In this course we describe the area of justification logics and the main results obtained for them. Justification logics were introduced by S Artemov in 1995. Propositional justification logics are formulated in the extension of standard propositional language by special terms that denote evidence for the truth of formulas. Replacing these terms by the modality expressing existence of such evidence converts justification logic to some propositional modal logic. So, justification logics can be considered as an explicit analog of modal logics. We will describe justification logics corresponding to some well-known modal logics and the appropriate semantics for them. We will prove completeness with respect to this semantics and realization of the corresponding modal logics, that is, the fact that for a number of modal logics $L$ for any formula $F$ derivable in $L$ there exists the way to ascribe justification terms to occurrences of modalities in $F$ which converts $F$ into a theorem of the justification logic $J(L)$.

Then we pay more attention to the logic of proofs $LP$ (S.N. Artemov, 1995), which started an investigation in this area. We will prove that the modal analog of $LP$ is the modal logic $S4$ and describe translation of propositional intuitionistic logic in $LP$. Then we supply $LP$ with the arithmetical semantics in which propositional variables stand for arithmetical sentences and justification terms denote codes of arithmetical derivations. We will prove that $LP$ is sound and complete with respect to this semantics. Arithmetical completeness of $LP$ together with the realization results for $S4$ and intuitionistic logic enables us to describe arithmetical semantics for them.

Another point of our interest is first order justification logic, for which we describe language and semantics and prove realization theorems for the appropriate first order modal logics. Also we will discuss possible ways of arithmetical reading for first order justification logic.

Lecturer
Yavorskaya Tatiana Leonidovna

Organizations
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Steklov International Mathematical Center