Justification Logic Bibliography

Bounds for the computational complexity of major justification logics were found in papers by Buss, N. Krupski, Kuznets, and Milnikel: logics J, J4, JT, LP and JD, were established to be Σ₂^p-complete. A corresponding lower bound is also known for JD4, the system that includes the consistency axiom and positive introspection. However, no upper bound has been established so far for this logic. Here, the missing upper bound for the complexity of JD4 is established through an alternating algorithm. It is shown that using Fitting models of only two worlds is adequate to describe JD4; this helps to produce an effective tableau procedure and essentially is what distinguishes the new algorithm from existing ones.

Bounds for the computational complexity of major justification logics were found in papers by Buss, N. Krupski, Kuznets, and Milnikel: logics J, J4, JT, LP and JD, were established to be Σ₂^p-complete. A corresponding lower bound is also known for JD4, the system that includes the consistency axiom and positive introspection. However, no upper bound has been established so far for this logic. Here, the missing upper bound for the complexity of JD4 is established through an alternating algorithm. It is shown that using Fitting models of only two worlds is adequate to describe JD4; this helps to produce an effective tableau procedure and essentially is what distinguishes the new algorithm from existing ones.

Keywords: Justification Logic, Computational Complexity, Satisfiability

We introduce a general purpose typed λ-calculus λ^∞ which contains intuitionistic logic, is capable of internalizing its own derivations as λ-terms and yet enjoys strong normalization with respect to a natural reduction system. In particular, λ^∞ subsumes the typed λ-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into λ-terms is a simple instance of the internalization property of λ^∞. The standard semantics of λ^∞ is given by a proof system with proof checking capacities. The system λ^∞ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.

What is public information in a multi-agent logic of knowledge such as T_n, S4_n or S5_n? Traditionally this notion has been captured by common knowledge, which is an epistemic operator Cφ given roughly as ∧_n=0^∞ Eⁿφ where Eφ= K₁φ∧K₂φ∧...∧K_nφ (everyone knows φ) and K_i is an individual agent's knowledge operator. In common knowledge systems T_n^C, S4_n^C, and S5_n^C, C depends directly on the agents' logic ([FagHalMosVar95]). A stronger notion of public information is introduced in [Art04TR] with the new epistemic operator J. This provides evidence-based common knowledge for which J φ (φ is justified) asserts that there is access to a proof of φ. Evidence-based systems are more flexible than their C counterparts as the logic for J can be chosen independently from that of the agents. The paper [Art04TR] considers evidence-based systems T_n^J, S4_n^J, and S5_n^J obtained from the base logics T_n, S4_n, and S5_n by adding a copy of S4 for J and a connection principle Jφ → K_iφ, i = 1, ..., n.

In this paper we compare common knowledge and justified knowledge in a canonical situation of the base logic S4 and specify an exact logic principle that distinguishes them. Let I.A. stand for the “Induction Axiom”

φ∧ J(φ ∧ Eφ) → Jφ.

Theorem. S4_n^C ≡ (S4_n^J + I.A.)^*, where ^* is replacing J by C.
This theorem provides an alternative formulation for S4_n^C.

Three formal approaches to public knowledge are “any fool” knowledge by McCarthy (1970), Common Knowledge by Halpern and Moses (1990), and Justified Knowledge by Artemov (2004). We compare them to mathematically address the observation that the light-weight systems of Justified Knowledge and `any fool knows' suffice to solve standard epistemic puzzles for which heavier solutions based on Common Knowledge are offered by standard textbooks. Specifically we show that epistemic systems with Common Knowledge modality C are conservative with respect to Justified Knowledge systems on formulas χ ∧ Cφ → ψ, where χ, φ, and ψ are C-free. We then notice that formalization of standard epistemic puzzles can be made in the aforementioned form, hence each time there is a solution within a Common Knowledge system, there is a solution in the corresponding Justified Knowledge system.

What is public information in a multi-agent logic of knowledge such as T_n, S4_n or S5_n? Traditionally this notion has been captured by common knowledge, which is an epistemic operator Cφ given roughly as ∧_n=0^∞ Eⁿφ where Eφ= K₁φ∧K₂φ∧⋅⋅⋅∧K_nφ (everyone knows φ) and K_is are individual agent's knowledge operators. In common knowledge systems T_n^C, S4_n^C, and S5_n^C, C depends directly on the agents' logic ([FagHalMosVar95]).

A stronger notion of public information is introduced in [Art04TR] with the new epistemic operator J. This provides evidence-based common knowledge for which J φ (φ is justified) asserts that there is access to a proof of φ. Evidence-based systems are more flexible than their C counterparts as the logic for J can be chosen independently from that of the agents. The paper [Art04TR] considers evidence-based systems T_n^J, S4_n^J, and S5_n^J obtained from the base logics T_n, S4_n, and S5_n by adding a copy of S4 for J and a connection principle Jφ → K_iφ, i = 1, ..., n.

In this paper we compare common knowledge and justified knowledge in a canonical situation of the base logic S4 and specify an exact logic principle that distinguishes them. Let I.A. stand for the “Induction Axiom”

φ∧ J(φ → Eφ) → Jφ.

Theorem. S4_n^C ≡ (S4_n^J + I.A.)^*, where ^* is replacing J by C.
This theorem provides an alternative formulation for S4_n^C.

A multi-agent epistemic logic S4_n^CJ is defined which encompasses both traditional Common Knowledge C (cf. [FagHalMosVar95, MeyvanderHoe95]) and Justified Knowledge J [Art06TCS]. Justified Common Knowledge, introduced by Artemov [Art06TCS], is a more general approach to the concept of common knowledge which has been shown to have better proof-theoretic and complexity behavior. The notion of justified knowledge grew from the studies of the Logic of Proofs [Art01BSL]. The discovery of the justified common knowledge J brought under consideration a whole variety of common knowledge operators for a given set of agents.

Here we introduce the logic S4_n^CJ, which is formalized as a normal modal logic of n agents each represented by an S4 modality K_i for i = 1, 2, ..., n. The two types of common knowledge are also S4 modalities and satisfy the connection axiom for all i : Jφ → K_iφ and Cφ → K_iφ. In addition, there is an induction axiom for C alone: [φ ∧ C(φ → Eφ)] → Cφ. In S4_n^CJ the modality C is the conventional common knowledge operator whereas J represents any common knowledge operator. In particular, Jφ → Cφ is provable, hence C is provably the weakest of common knowledge operators.

We show that S4_n^CJ is sound and complete for a class of epistemic Kripke models. As a result, we also have that S4_n^CJ has the finite model property and is decidable. S4_n^CJ is conservative over both S4_n^C and S4_n^J, the analogous systems with a single common knowledge modality, C or J respectively. This then offers a convenient testbed for analyzing different approaches to the common knowledge phenomenon (cf. [Ant06TR]).

We consider the relative strengths of three formal approaches to public knowledge: “any fool” knowledge by McCarthy (1970), Common Knowledge by Halpern and Moses (1990), and Justified Knowledge by Artemov (2004). Specifically, we show that epistemic systems with the Common Knowledge modality C are conservative with respect to Justified Knowledge systems on formulas χ ∧ Cφ → ψ, where χ, φ, and ψ are C-free.

Keywords: justified knowledge, common knowledge, Artemov, conservative

The Knower Paradox demonstrates that any theory T which 1) extends Robinson arithmetic Q, 2) includes a predicate K(x) intended to formalize the formula with Godel number x is known by agent i, and 3) contains certain elementary epistemic principles involving K(x) is inconsistent. In [DeaKur09FEW] Dean and Kurokawa show that the Knower can be proved in the Quantified Logic of Proofs (QLP) formulated by Mel Fitting in [Fit08APAL] – extending work presented by Artemov in [Art01BSL]. Dean and Kurokawa argue that QLP is more expressive than most modal logics and that this permits to identify more clearly the epistemic principles used in the proof of the Knower. They also argue that the proof seems to require the use of a suspect principle – the Uniform Barcan Formula (UBF). So, they propose to resolve the paradox by abandoning UBF. In this note we offer three independent proofs of the Knower in QLP that do not require the use of UBF. So, it seems that the resolution of the paradox proposed by Dean and Kurokawa is not a viable option. We conclude with some observations about possible resolutions of the paradox compatible with our results.

In this paper individual proofs are integrated into provability logic. Systems of axioms for a logic with operators “A is provable” and “p is a proof of A” are introduced, provided with Kripke semantics and decision procedure. Completeness theorems with respect to the arithmetical interpretation are proved.

Answers to two old questions are given in this paper.
1. Modal logic S4, which was informally specified by Gödel in 1933 as a logic for provability, meets its exact provability interpretation.
2. Brouwer - Heyting - Kolmogorov realizing operations (1931-32) for intuitionistic logic Int also get exact interpretation as corresponding propositional operations on proofs; both S4 and Int turn out to be complete with respect to this proof realization.

These results are based on operational reading of S4, where a modality is split into three operations. The logic of proofs with these operations is shown to be arithmetically complete with respect to the intended provability semantics and sufficient to realize every operation on proofs admitting propositional specification in arithmetic.

Logic of Proofs (LP) has been introduced in [Art95TR] as a collection of all valid formulas in the propositional language with labeled logical connectives [[t]](⋅) where t is a proof term with the intended reading of [[t]]F as “t is a proof of F”. LP is supplied with a natural axiom system, completeness and decidability theorems. LP may express some constructions of logic which have been formulated or/and interpreted in an informal metalanguage involving the notion of proof, e.g. the intuitionistic logic and its Brauwer-Heyting-Kolmogorov semantics, classical modal logic S4, etc (cf. [Art95TR]). In the current paper we demonstrate how the intuitionistic propositional logic Int can be directily realized into the Logic of Proofs. It is shown, that the proof realizability gives a fair semantics for Int.

The Logic of Proofs (LP) introduced in [Art95TR] provides a basic framework for the formalization of reasoning about proofs. It incorporates proof terms into the propositional language, using labeled logical operators “t : ” with the intended reading of t:F being “t is a proof of F”. LP is supplied with an exact provability semantics in Peano Arithmetic, a simple axiom system, and completeness and decidability theorems. LP naturally expresses a number of constructions of logic involving the notion of proof, which have previously been formulated and/or interpreted in an informal metalanguage, e.g. modal logic, Intuitionistic logic with its Brouwer-Heyting-Kolmogorov semantics, etc. ([Art95TR], [Art96TR]). In the current paper we demonstrate how the typed λ-calculus and the modal λ-calculus can be realized in the Logic of Proofs.

In 1933 Gödel introduced an axiomatic system, currently known as S4, for a logic of an absolute provability, i.e. not depending on the formalism chosen ([Goed33]). The problem of finding a fair provability model for S4 was left open. The famous formal provability predicate which first appeared in the Gödel Incompleteness Theorem does not do this job: the logic of formal provability is not compatible with S4. As was discovered in [Art95TR], this defect of the formal provability predicate can be bypassed by replacing hidden quantifiers over proofs by proof polynomials in a certain finite basis. The resulting Logic of Proofs enjoys a natural arithmetical semantics and provides an intended provability model for S4, thus answering a question left open by Gödel in 1933. Proof polynomials give an intended semantics for some other constructions based on the concept of provability, including intuitionistic logic with its Brouwer-Heyting- Kolmogorov interpretation, λ-calculus and modal λ-calculus. In the current paper we demonstrate how the intuitionistic propositional logic Int can be directly realized by proof polynomials. It is shown that Int is complete with respect to this proof realizability.

In 1933 Gödel introduced a modal logic of provability (S4) and left open the problem of a formal provability semantics for this logic. We give a complete solution to this problem. We find a sound and complete axiom system for the logic (LP) with atomic propositions for explicit proofs “t is a proof of F”, and construct an exact realization of S4 in LP . In LP the reflection principle is valid, which circumvents some of the restrictions imposed on the provability operator by Gödel's second incompleteness theorem.

LP formalizes the Kolmogorov calculus of problems and proves the Kolmogorov conjecture (1932) that intuitionistic logic coincides with the classical calculus of problems. LP has revealed the relationship between proofs and types, and subsumes the λ-calculus, modal λ-calculus and combinatory logic.

The intended meaning of intuitionistic logic is given by the Brouwer-Heyting-Kolmogorov (BHK) semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The natural problem of formalizing the BHK semantics and establishing the completeness of propositional intuitionistic logic Int with respect to this semantics remained open until recently. This question turned out to be a part of the more general problem of the intended semantics for Gödel's modal logic of provability S4 with the atoms “F is provable” which was open since 1933. In this paper we present complete solutions to both of these problems.

We find the logic of explicit provability (LP) with the atoms “t is a proof of F” and establish that every theorem of S4 admits a reading in LP as the statement about explicit provability. This provides the adequate provability semantics for S4 along the lines of a suggestion made by Gödel in 1938. The explicit provability reading of Gödel's embedding of Int into S4 gives the desired formalization of the BHK semantics: Int is shown to be complete with respect to this semantics. In addition, LP has revealed the relationship between proofs and types, and subsumes the λ-calculus, modal λ-calculus and combinatory logic.

The basic properties of soundness, extensibility, and stability required from a verification system V taken in full yield the necessity of having a reflection rule in every such V. However, the reflection rule based on the Gödel provability predicate (implicit provability predicate) leads to a “reflection tower” of theories which cannot be formally verified.

The paper introduces an explicit reflection mechanism which can be verified inside the system. This circumvents the reflection tower and provides a strict justification for the verification process. On the practical side, the paper gives specific recommendations concerning the verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.

In 1933 Gödel introduced a modal logic of provability (S4) and left open the problem of a formal provability semantics for this logic. Since then numerous attempts have been made to give an adequate provability semantics to Gödel's provability logic with only partial success. In this paper we give the complete solution to this problem in the Logic of Proofs (LP). LP implements Gödel's suggestion (1938) of replacing formulas “F is provable” by the propositions for explicit proofs “t is a proof of F” (t:F). LP admits the reflection of explicit proofs t:F → F thus circumventing restrictions imposed on the provability operator by Gödel's second incompleteness theorem. LP formalizes the Kolmogorov calculus of problems and proves the Kolmogorov conjecture that intuitionistic logic coincides with the classical calculus of problems.

Explicit modal logic was first sketched by Gödel in [Goed38CW] as the logic with the atoms “t is a proof of F”. The complete axiomatization of the Logic of Proofs LP was found in [Art95TR] (see also [Art02CSLI],[Art98TRb],[JapdeJon98HPT]). In this paper we establish a sort of a functional completeness property of proof polynomials which constitute the system of proof terms in LP. Proof polynomials are built from variables and constants by three operations on proofs: “⋅” (application), “!” (proof checker), and “+” (choice). Here constants stand for canonical proofs of “simple facts”, namely instances of propositional axioms and axioms of LP in a given proof system. We show that every operation on proofs that (i) can be specified in a propositional modal language and (ii) is invariant with respect to the choice of a proof system is realized by a proof polynomial.

The traditional Curry-Howard isomorphism given a derivation of F from assumptions Γ in intuitionistic modal logic constructs the λ-term t(x) such that the sequent x:Γ ⇒ t(x):F is derivable in the corresponding calculus of typed modal λ-terms. Technically speaking this isomorphism is a realization by λ-terms of the outermost modalities in some (not all) derivable modal sequents []Γ ⇒ []F.

In this talk we describe a system of λ-terms (in the combinatory terms form) LPi sufficient for a uniform realization of all modalities (not just the outermost ones) in any derivable modal sequent. The expressive power of LPi surpasses the one of the usual modal λ-calculus. LPi also extends the natural provability semantics of Curry-Howard terms under which t:F can be interpreted as “t is a proof of F in a given sufficiently rich system, e.g. Heyting Arithmetic HA”.

The intended meaning of intuitionistic logic is explained by the Brouwer-Heyting-Kolmogorov (BHK) provability semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The problem of finding an adequate formalization of the provability semantics and establishing the completeness of the intuitionistic logic Int was first raised by Gödel in 1933. This question turned out to be a part of the more general problem of the intended realization for Gödel's modal logic of provability S4 which was open since 1933. In this tutorial talk we present a provability realization of Int and S4 that solves both of these problems. We describe the logic of explicit provability (LP) with the atoms “t is a proof of F” and establish that every theorem of S4 admits a reading in LP as the statement about operations on proofs. Moreover, both S4 and Int are shown to be complete with respect to this realization. In addition, LP subsumes the λ-calculus, modal λ-calculus, combinatory logic and provides a uniform provability realization of modality and λ-terms.

We show that the stability requirement for a verification system yields the necessity of some sort of a reflection mechanism. However, the traditional reflection rule based on the Gödel implicit provability predicate leads to a “reflection tower” of theories which cannot be formally verified. We found natural lower and upper bounds on a metatheory capable of establishing stability of a given verification system. The paper also introduces an explicit reflection mechanism which can be verified internally. This circumvents the reflection tower and provides a theoretical justification for the verification process. On the practical side, the paper gives specific recommendations concerning verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.

In 1933 Gödel introduced an axiomatic system, currently known as S4, for a logic of an absolute provability, i.e. not depending on the formalism chosen [Goed33]). The problem of finding a fair provability model for S4 was left open. The famous formal provability predicate which first appeared in the Gödel Incompleteness Theorem does not do this job: the logic of formal provability is not compatible with S4. As was discovered in [Art95TR], this defect of the formal provability predicate can be bypassed by replacing hidden quantifiers over proofs by proof polynomials in a certain finite basis. The resulting Logic of Proofs enjoys a natural arithmetical semantics and provides an intended provability model for S4, thus answering a question left open by Gödel in 1933. Proof polynomials give an intended semantics for some other constructions based on the concept of provability, including intuitionistic logic with its Brouwer-Heyting- Kolmogorov interpretation, lambda-calculus and modal lambda-calculus. In the current paper we demonstrate how the intuitionistic propositional logic Int can be directly realized by proof polynomials. It is shown, that Int is complete with respect to this proof realizability.

Explicit modal logic was first sketched by Gödel in [Goed38CW] as the logic with the atoms “t is a proof of F”. The complete axiomatization of the Logic of Proofs LP was found in [Art95TR] (see also [Art02CSLI],[Art98TRb],[JapdeJon98HPT]). In this paper we establish a sort of a functional completeness property of proof polynomials which constitute the system of proof terms in LP. Proof polynomials are built from variables and constants by three operations on proofs: “⋅” (application), “!” (proof checker), and “+” (choice). Here constants stand for canonical proofs of “simple facts”, namely instances of propositional axioms and axioms of LP in a given proof system. We show that every operation on proofs that (i) can be specified in a propositional modal language and (ii) is invariant with respect to the choice of a proof system is realized by a proof polynomial.

In 1933 Gödel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projectiof of LP. This also achieves Gödel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which resisted formalization since early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.

Gödel's Incompleteness theorem and his papers of 1933 and 1938 led to two essentially different models for provability, each having its own areas of applications.

A. Loeb's modal logic L of formal provability (also known as GL, G, PRL, K4.W) where the “non-reflexive” Loeb principle is present. Within this model proofs are represented implicitly by existential quantifiers. The highlights of this model are the propositional formalization of the Second Incompleteness Theorem and Loeb's theorem, De Jongh-Sambin fixed point theorem, and the Solovay completeness theorem. The logic L finds applications in traditional proof theory.

B. Gödel's modal logic for provability (also known as S4) and its counterpart logic of proofs LP with the reflection principle “provable F implies F”. Within his model proofs are represented explicitly by combinatory style terms. This model has reached out to such areas as constructive semantics, logics of knowledge, combinatory logic and lambda-calculus, automated deduction and formal verification, and typed programming languages.

The models A and B are compatible because they are both based on the same Gödel provability predicate.

It is shown that the modal logic S4, simple λ-calculus and modal λ-calculus admit a realization in a very simple propositional logical system LP, which has an exact provability semantics. In LP both modality and λ-terms become objects of the same nature, namely, proof polynomials. The provability interpretation of modal λ-terms presented here may be regarded as a system-independent generalization of the Curry-Howard isomorphism of proofs and λ-terms.

We will speak about three traditions in Logic:

- Classical, usually associated with Frege, Hilbert, Gödel, Tarski, and others;

- Intuitionistic, founded by Brouwer, Heyting, Kolmogorov, Gödel, Kleene, and others;

- Explicit, which we trace back to Skolem, Curry, Gödel, Church, and others.

The classical tradition in logic based on quantifiers ∀ and ∃ essentially reflected the 19th century mathematician's way of representing dependencies between entities. A sentence ∀x∃yA(x,y), though specifying a certain relation between x and y, did not mean that the latter is a function of the former, let alone a computable one. The Intuitionistic approach provided a principal shift toward the effective functional reading of the mathematician's quantifiers. A new, non-Tarskian semantics had been suggested by Kleene: realizability that revealed a computational content of logical derivations. In a decent intuitionstic system, a proof of ∀x∃yA(x,y) yields a program f that computes y=f(x).

Explicit tradition makes the ultimate step by using representative systems of functions instead of quantifiers from the very beginning. Since the work of Skolem, 1920, it has been known that the classical logic can be adequately recast in this way. Church in 1936 showed that even the very basic system of function definition and function application is capable of emulating any computable procedure. However, despite this impressive start, the explicit tradition remained a Cinderella of the mathematical logic for decades. Now things have changed: due to its very explicitness, this third tradition became the one most closely connected with Computer Science.

In this talk we will show how switching from quantifiers to explicit functional language helps problem solving in both theoretical logic and its applications. A discovery of a natural system of self-referential proof terms, proof polynomials, was essential in the solution to an open problem of Gödel concerning formalization of provability. Proof polynomials considerably extend the Curry-Howard isomorphism and lead to a joint calculus of propositions and proofs which unifies several previously unrelated areas. It changes our conception of the appropriate syntax and semantics for reasoning about knowledge, functional programming languages, formalized deduction and verification.

The Logic of Proofs LP introduced by the author may be regarded as a basic formal system for reasoning about propositions and proofs. LP comes from Gödel's calculus of provability, also known as modal logic S4 to which P. S. Novikov devoted the well-known monograph Constructive Mathematical Logic from the Point of View of the Classical One. LP gives an exact mathematical answer to the question of the provability semantics of S4 raised by Gödel. This paper gives a comparison of the expressive powers of LP, the typed λ-calculus, and the modal λ-calculus. It is shown that a small (namely, Horn) fragment of LP is sufficient for a natural embedding of the typed λ-calculus. It is also shown that LP models the modal λ-calculus.

In this paper we introduce a new type of knowledge operator, called evidence-based knowledge, intended to capture the constructive core of common knowledge. An evidence-based knowledge system is obtained by augmenting a multi-agent logic of knowledge with a system of evidence assertions t:φ (“t is an evidence for φ”) based on the following plausible assumptions: 1) each axiom has evidence; 3) evidence is checkable; 3) any evidence implies individual knowledge for each agent. Normally, the following monotonicity property is also assumed: 4) any piece of evidence is compatible with any other evidence. We show that the evidence-based knowledge operator is a stronger version of the common knowledge operator. Evidence-based knowledge is free of logical omniscience, model-independent, and has natural motivation. Furthermore, evidence-based knowledge can be presented by normal multi-modal logics, which are in the scope of well-developed machinery applicable to modal logic: epistemic models, normalized proofs, automated proof search, etc.

Intuitionistic mathematics was created by Brouwer on the basis of constructive reasoning, where the existence of a proof was the criterion for truth. Kolmogorov and Gödel proposed interpreting intuitionistic logic on the basis of classical notions of a problem's solution and of provability. In 1933 Gödel made the first substantial step toward the building of such an interpretation. Despite much progress in the understanding of intuitionism, this task was not complete before the author's 1995 paper [Art95TR]. This survey will cover the results of the past decade obtained within this framework.

In this paper we introduce the justified knowledge operator J with the intended meaning of Jφ as `there is a justification for φ.' Though justified knowledge appears here in a case study of common knowledge systems, a similar approach is applicable in more general situations. First we consider evidence-based common knowledge systems obtained by augmenting a multi-agent logic of knowledge with a system of evidence assertions t:φ, reflecting the notion `t is an evidence for φ,' such that evidence is respected by all agents. Justified common knowledge is obtained by collapsing all evidence terms into one modality J. We show that in standard situations, when the base epistemic systems are T, S4, and S5, the resulting justified common knowledge systems are normal modal logics, which places them within the scope of well-developed machinery applicable to modal logic: Kripke-style epistemic models, normalized proofs, automated proof search, etc. In the aforementioned situations, the intended semantics of justified knowledge is supported by a realization theorem stating that for any valid fact about justified knowledge, one could recover its constructive meaning by realizing all occurrences of justified knowledge modalities Jφ by appropriate evidence terms t:φ.

Keywords: epistemic logic, common knowledge, justification, logic of proofs

The Logic of Proofs LP captures the invariant propositional properties of proof predicates t is a proof of F with a set of operations on proofs sufficient for realizing the whole modal logic S4 and hence the intuitionistic logic IPC. Some intuitive properties of proofs, however, are not invariant and hence not present in LP. For example, the choice function `+' in LP, which is specified by the condition s:F ∨ t:F → (s+t):F, is not necessarily symmetric. In this paper, we introduce an extension of the Logic of Proofs, SLP, which incorporates natural properties of the standard proof predicate in Peano Arithmetic:

t is a code of a derivation containing F,

including the symmetry of Choice. We show that SLP produces Brouwer-Heyting-Kolmogorov proofs with a rich structure, which can be useful for applications in epistemic logic and other areas.

We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem.

As a case study, we formalize Gettier examples in Justification Logic and reveal hidden assumptions and redundancies in Gettier reasoning. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic.

The Logic of Proofs LP captures the invariant propositional properties of proof predicates t is a proof of F with a set of operations on proofs sufficient for realizing the whole modal logic S4 and hence the intuitionistic logic IPC. Some intuitive properties of proofs, however, are not invariant and hence not present in LP. For example, the choice function `+' in LP, which is specified by the condition s:F ∨ t:F → (s+t):F, is not necessarily symmetric. In this paper, we introduce an extension of the Logic of Proofs, SLP, which incorporates natural properties of the standard proof predicate in Peano Arithmetic:

t is a code of a derivation containing F,

including the symmetry of Choice. We show that SLP produces Brouwer-Heyting-Kolmogorov proofs with a rich structure, which can be useful for applications in epistemic logic and other areas.

We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic.

As a case study, we offer a resolution of the Goldman-Kripke `Red Barn' paradox and analyze Russell's `prime minister example' in Justification Logic. Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and redundancies in Gettier's reasoning.

In this paper, we will sketch the basic system of Justification Logic, which is a general logical framework for reasoning about epistemic justification. Justification Logic renders a new, evidence-based foundation for epistemic logic. As a case study, we compare formalizations of the Kripke `Red Barn' scenario in modal epistemic logic and Justification Logic and show here that the latter provides a deeper analysis. In particular, we argue that modal language fails to fully represent the epistemic closure principle whereas Justification Logic provides its adequate formalization.

We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic.

As a case study, we offer a resolution of the Goldman-Kripke `Red Barn' paradox and analyze Russell's `prime minister example' in Justification Logic. Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and redundancies in Gettier's reasoning.

In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts. We consider as basic an example which features two justifications for a true statement, one which is correct and one which is not. We formalize this example in a system of Justification Logic with two knowers: the object agent and the observer, and we show that whereas the object agent does not logically distinguish between factive and non-factive justifications, such distinctions can be attained at the observer level by analyzing the structure of evidence terms. Basic logic properties of the corresponding two-agent Justification Logic system have been established, which include Kripke-Fitting completeness.

We also argue that a similar evidence-tracking approach can be applied to analyzing paraconsistent systems.

In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts. We consider as basic an example which features two justifications for a true statement, one which is correct and one which is not. We formalize this example in a system of Justification Logic with two knowers: the object agent and the observer, and we show that whereas the object agent does not logically distinguish between factive and non-factive justifications, such distinctions can be attained at the observer level by analyzing the structure of evidence terms. Basic logic properties of the corresponding two-agent Justification Logic system have been established, which include Kripke-Fitting completeness. We also argue that a similar evidence-tracking approach can be applied to analyzing paraconsistent systems.

Keywords: justification, epistemic logic, evidence

Of Plato's tripartite analysis of knowledge, justified true belief, the traditional modal approach to epistemology leaves justification out of the picture. Justification Logic augments epistemic logic by assertions t:F that read

t is a justification for F

hence incorporating all three of Plato's criteria. Justification Logic absorbs basic principles that originate from both mainstream epistemology and the mathematical theory of proofs. A general Correspondence Theorem shows that behind each epistemic modal logic lies a robust system of justifications. This renders an evidence-based foundation for formal epistemology.

Justification Logic provides an axiomatic description of justifications and delegates the question of their nature to semantics. In this note, we address the conceptual issue of the logical type of justifications: we argue that justifications in the logical setting are naturally interpreted as sets of formulas which leads to a class of epistemic models that we call modular models. We show that Fitting models for Justification Logic naturally encode modular models and can be regarded as convenient pre-models of the former.

Justification Logic provides an axiomatic description of justifications and delegates the question of their nature to semantics. In this note, we address the conceptual issue of the logical type of justifications: we argue that justifications in the logical setting are naturally interpreted as sets of formulas which leads to a class of epistemic models that we call modular models. We show that Fitting models for Justification Logic naturally encode modular models and can be regarded as convenient pre-models of the former.

Keywords: Justification Logic, Kripke models, Fitting models

We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion []A is replaced by [[s]]A whose intended reading is “s is a proof of A”. A term calculus for this formulation yields a typed lambda calculus λ^I that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, λ^I internalises its own computations. Confluence and strong normalisation of λ^I is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.

We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion []A is replaced by [[s]]A whose intended reading is “s is a proof of A”. A term calculus for this formulation yields a typed lambda calculus λ^I that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, λ^I internalises its own computations. Confluence and strong normalisation of λ^I is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.

The logic of proofs is the modal provability logic enriched by new operators (labeled modalities) for individual proofs. In the current paper we add to the logic of proofs also new labeled modalities which stand for the complexity of proofs. The Kripke style completeness, decidability, and arithmetical completeness theorems are obtained. The complexity logics introduced here correspond to two major classes of complexity measures: decidable and recursively enumerable ones; the completeness theorems relate either of these logics to the entire class of the relevant complexity measures.

The famous de Jongh's theorem of 1970 stated that the intuitionistic logic captured all the logical formulas which have all arithmetical instances derivable in the Heyting Arithmetic HA. In this note we extend de Jongh's arithmetical completeness property from IPC to the basic intuitionistic logic of proofs, which allows proof assertion statements of the sort x is a proof of F. The logic of proofs seems to provide an appropriate language of describing admissible rules in HA.

The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

The Reflective Combinatory Logic RCL [Art04RMS] is an extension of the Typed Combinatory Logic CL_→ which admits typing judgments of the form “t is a term of type F” inside types via an additional type constructor t:F. Unlike the case of the Intuitionistic Type Theory [Mar98] where a similar type constructor is also available, the type t:F in RCL is inhabited by nontrivial terms that store a complete information about the typing judgment.

In the definition of RCL the following two judgments have been introduced by simultaneous induction: “F is a well-formed formula (or type)” and “F is derivable from F₁,...,F_n”. The intended meaning of the latter is “type F is inhabited provided all types F_i are”. In this talk we give an equivalent cut-free sequent formulation for RCL and establish complexity bounds for the decision problems concerning these judgements.

Theorem 1. The well-formedness property for RCL is decidable in polynomial time. The derivability in RCL is decidable and PSPACE-complete.

We introduce reference structures – a basic logical model of a computer memory organization capable to store and utilize information about its addresses. The corresponding labeled modal logics are axiomatized and supplied with the completeness and decidability theorems. A labeled modal formula can be regarded as a description of a certain reference structure; the satisfiability algorithm gives a method of building and optimizing reference structures satisfying a given formula.

We introduce reference structures – a basic logical model of a computer memory organization capable to store and utilize information about its addresses. The corresponding labeled modal logics are axiomatized and supplied with the completeness and decidability theorems. A labeled modal formula can be regarded as a description of a certain reference structure; the satisfiability algorithm gives a method of building and optimizing reference structures satisfying a given formula.

We introduce reference structures – a basic mathematical model of a data organization capable to store and utilize information about its addresses. A propositional labeled modal language is used as a specification and programming language for reference structures; the satisfiability algorithm for modal language gives a method of building and optimizing reference structures satisfying a given formula. Corresponding labeled modal logics are presented, supplied with cut free axiomatizations, completeness and decidability theorems are proved. Initialization of typed variables in some programming languages is presented as an example of a reference structure building.

We introduce reference structures – a basic mathematical model of a data organization capable to store and utilize information about its addresses. A propositional labeled modal language is used as a specification and programming language for reference structures; the satisfiability algorithm for modal language gives a method of building and optimizing reference structures satisfying a given formula. Corresponding labeled modal logics are presented, supplied with cut free axiomatizations, completeness and decidability theorems are proved. Initialization of typed variables in some programming languages is presented as an example of a reference structure building.

The Hintikka-style modal logic approach to knowledge has a well-known defect of logical omniscience, i.e., an unrealistic feature that an agent knows all logical consequences of her assumptions. In this paper we suggest the following Logical Omniscience Test (LOT): an epistemic system E is not logically omniscient if for any valid in E knowledge assertion A of type `F is known' there is a proof of F in E, the complexity of which is bounded by some polynomial in the length of A. We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions). We also apply LOT to Justification Logic, which along with the usual knowledge operator K<sub>i</sub>(F) (`agent i knows F') contain evidence assertions t:F (`t is a justification for F'). In Justification Logic, the evidence part is an appropriate extension of the Logic of Proofs LP, which guarantees that the collection of evidence terms t is rich enough to match modal logic. We show that justification logic systems are logically omniscient w.r.t. the usual knowledge and are not logically omniscient w.r.t. the evidence-based knowledge.

The Hintikka-style modal logic approach to knowledge contains a well-known defect of logical omniscience, i.e., the unrealistic feature that an agent knows all logical consequences of her assumptions. In this paper, we suggest the following Logical Omniscience Test (LOT): an epistemic system E is not logically omniscient if for any valid in E knowledge assertion A of type `F is known,' there is a proof of F in E, the complexity of which is bounded by some polynomial in the length of A. We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions). We also apply LOT to evidence-based knowledge systems, which, along with the usual knowledge operator K<sub>i</sub>(F) (`agent i knows F'), contain evidence assertions t:F (`t is a justification for F'). In evidence-based systems, the evidence part is an appropriate extension of the Logic of Proofs LP, which guarantees that the collection of evidence terms t is rich enough to match modal logic. We show that evidence-based knowledge systems are logically omniscient w.r.t. the usual knowledge and are not logically omniscient w.r.t. evidence-based knowledge.

The logical omniscience feature assumes that an epistemic agent knows all logical consequences of her assumptions. This paper offers a general theoretical framework that views logical omniscience as a computational complexity problem. We suggest the following approach: we assume that the knowledge of an agent is represented by an epistemic logical system E; we call such an agent not logically omniscient if for any valid knowledge assertion A of type F is known, a proof of F in E can be found in polynomial time in the size of A. We show that agents represented by major modal logics of knowledge and belief are logically omniscient, whereas agents represented by justification logic systems are not logically omniscient with respect to t is a justification for F.

An issue of a logic of knowledge with justifications has been discussed since the early 1990s. Such a logic along with the usual knowledge operator []F “F is known” should contain assertions t:F “t is an evidence of F”. In this paper we build two systems of logic of knowledge with justifications: LPS4, which is an extension of the basic epistemic logic S4 by an appropriate calculus of evidences corresponding to the logic of proofs LP together with the principle that justification implies knowledge, and LPS4^–, which is LPS4 augmented by the mixed implicit/explicit negative introspection principle. We offer a provability semantics for LPS4 and LPS4^– where the epistemic modality []F is interpreted as “F is true and provable” and the evidence assertions t:F as “t is a proof of F”. We find Kripke semantics and establish a number of fundamental properties of LPS4 and LPS4^–. On the way to those systems we find the minimal joint logic of proofs and formal provability, LPGL, complete with respect to the standard provability semantics.

An issue of an epistemic logic with justification has been discussed since the early 1990s. Such a logic, along with the usual knowledge operator []F (F is known), should contain assertions t:F (t is a justification for F), which gives a more nuanced and realistic model of knowledge. In this paper, we build two systems of epistemic logic with justification: the minimal one—S4LP—which is an extension of the basic epistemic logic S4 by an appropriate calculus of justification corresponding to the logic of proofs LP, and S4LPN—which is S4LP augmented by the explicit negative introspection principle ¬(t:F) → []¬(t:F). Epistemic semantics for both systems are suggested. Completeness and specific properties of S4LP and S4LPN, reflecting the explicit character of those systems, are established.

The true belief components of Plato's tripartite definition of knowledge as justified true belief are represented in formal epistemology by modal logic and its possible worlds semantics. At the same time, the justification component of Plato's definition did not have a formal representation. This paper introduces the notion of justification into formal epistemology. Epistemic logic with justification, along with the usual knowledge operator []F (F is known), contains assertions t:F (t is a justification for F). We suggest an epistemic semantics which augments Kripke models with a natural Fitting-style treatment of justification assertions t:F. Completeness and some new specific properties of basic systems of epistemic logic with justification are established.

Plato's tripartite definition of knowledge as justified true belief (JTB) is generally regarded as a set of necessary conditions for the possession of knowledge. The true belief components the JTB definition are represented in formal epistemology by modal logic and its possible worlds semantics. At the same time, the justification component of Plato's definition did not have a formal representation. This paper introduces the notion of justification into formal epistemology. Epistemic logic with justification, along with the usual knowledge operator []F (F is known), contains assertions t:F (t is a justification for F). We study two basic systems, S4LP and S4LPN, of epistemic logic with justification and show completeness with respect to natural epistemic semantics, which augments Kripke models with a natural Fitting-style treatment of justification assertions t:F. Some new specific properties of epistemic logic with justification are established.

Keywords: epistemic lgoic, logic of proofs, justification, knowledge

The Justification Logic is a family of logical systems obtained from epistemic logics by adding new type of formulas t:F which reads as t is a justification for F. The major epistemic modal logic S4 has a well-known Tarski topological interpretation which interprets []F as the interior of F (a topological equivalent of the `knowable part of F'). In this paper we extend the Tarski topological interpretation from epistemic modal logics to justification logics which have both: knowledge assertions []F and justification assertions t:F. This topological semantics interprets modality as the interior, terms t represent tests, and a justification assertion t:F represents a part of F which is accessible for test t. We establish a number of soundness and completeness results with respect to Kripke topology and the real line topology for S4-based systems of Justification Logic.

Keywords: Justification Logic, Logic of Proofs, modal logic, topological semantics, Tarski

Justification Logic is a family of epistemic logical systems obtained from modal logics of knowledge by adding a new type of formula t:F , which is read t is a justification for F. The principal epistemic modal logic S4 includes Tarski's well-known topological interpretation, according to which the modality []X is read the Interior of X in a topological space (the topological equivalent of the `knowable part of X'). In this paper, we extend Tarski's topological interpretation from S4 to Justification Logic systems with both modality and justification assertions. The topological semantics interprets t:X as a reachable subset of X (the topological equivalent of `test t confirms X'). We establish a number of soundness and completeness results with respect to Kripke topology and the real topology for S4-based systems of Justification Logic.

Keywords: modal logic, Justification Logic, topological semantics, Tarski

Propositional Provability Logic was axiomatized in [Sol76]. This logic describes the behaviour of the arithmetical operator “y is provable”. The aim of the current paper is to provide propositional axiomatizations of the predicate “x is a proof of y” by means of modal logic, with the intention of meeting some of the needs of computer science.

This report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems PF and PFM in the Basic Logic of Proofs. An appropriate axiom system PU in a language with operators “x is a proof of y” is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms.

Propositional Provability Logic was axiomatized in [Sol76]. This logic describes the behaviour of the arithmetical operator “y is provable”. The aim of the current paper is to provide propositional axiomatizations of the predicate “x is a proof of y” by means of modal logic, with the intention of meeting some of the needs of computer science.

We discuss the logics of the operators “p is a proof of A” and “p is a proof containing A” for the standard Gödel proof predicate in Peano Arithmetic. Decidabillty and arithmetical completeness of these logics are proved. We use the same semantics as for the Provability Logic where the operator “A is provable” is studied.

The Logic of Proofs LP solved long standing Gödel's problem concerning his provability calculus (cf. [Art01BSL]]). It also opened new lines of research in proof theory, modal logic, typed programming languages, knowledge representation, etc. The propositional logic of proofs is decidable and admits a complete axiomatization. In this paper we show that the first order logic of proofs is not recursively axiomatizable.

Keywords: logic of proofs, provability, recursive axiomatizability

The propositional logic of proofs LP revealed an explicit provability reading of modal logic S4 which provided an indented provability semantics for the propositional intuitionistic logic IPC and led to a new area, Justification Logic. In this paper, we find the first-order logic of proofs FOLP capable of realizing first-order modal logic S4 and, therefore, the first-order intuitionistic logic HPC. FOLP enjoys a natural provability interpretation; this provides a semantics of explicit proofs for first-order S4 and HPC compliant with Brouwer-Heyting-Kolmogorov requirements. FOLP opens the door to a general theory of first-order justification.

Justification Logic (JL) is a refinement of modal logic that has recently been proposed for explaining well-known paradoxes arising in the formalization of Epistemic Logic. Assertions of knowledge and belief are accompanied by justifications: the formula [[t]]A states that t is “reason” for knowing/believing A. We study the computational interpretation of JL via the Curry-de Bruijn-Howard isomorphism in which the modality [[t]]A is interpreted as: t is a type derivation justifying the validity of A. The resulting lambda calculus is such that its terms are aware of the reduction sequence that gave rise to them. This serves as a basis for understanding systems, many of which belong to the security domain, in which computation is history-aware.

In the first part of the paper we discuss some conceptual problems related to the notion of proof. In the second part we survey five major open problems in Provability Logic as well as possible directions for future research in this area.

We explore an intuitionistic fragment of Artëmov's Logic of Proofs as a type system for a programming language for mobile units. Such units consist of both a code and certificate component. Dubbed the Certifying Mobile Calculus, our language caters for both code and certificate development in a unified theory. In the same way that mobile code is constructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system additionally ensures correct certificate construction out of certificate components. We present proofs of type safety and strong normalistion for a run-time system based on an abstract machine.

We explore an intuitionistic fragment of Artëmov's Logic of Proofs as a type system for a programming language for mobile units. Such units consist of both a code and certificate component. Dubbed the Certifying Mobile Calculus, our language caters for both code and certificate development in a unified theory. In the same way that mobile code is constructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system additionally ensures correct certificate construction out of certificate components. We present proofs of type safety and strong normalistion for a run-time system based on an abstract machine.

The epistemic meaning of modality suggests that a modal formula []A → []B implicitely specifies a function f(x) such that if x is a justification of A then f(x) is a justification for B. S. Artemov in [Art95TR], [Art01BSL] made this consideration formal by introducing a system of proof polynomials necessary and sufficient for realizing modalities in every S4-derivation. Proof polynomials subsume typed λ-calculus by allowing types depending on terms. The Curry-Howard semantics of λ-terms as operations on proofs has also been extended to proof polynimials, which answered a long standing question about the intended provability meaning of S4. Artemov's Logic of Proofs LP that desicribes all identities on proof polynomials may be regarded as an explicit counterpart of S4.
In this paper we find explicit counterparts of the modal logics K, K4, T, D and D4. Realizing terms for all these logics are proper subclasses of proof polynomials. The corresponding explicit modal logics are subsystems of LP. The realization methods are based on the Artemov's realization algorithm.

The Logic of Proofs (LP) was introduced by S. N. Artemov. It is a system in the propositional language with additional sort of objects – proof terms, and an extra atomic propositions [t]F with intended reading “t is a proof of F”. LP is an explicit counterpart of modal logic S4, since S4 is the exact term-forgetting projection of LP. In the present paper we build sequent system corresponding to fragment of LP sufficient to realize S4. Using its format we build explicit counterparts of modal logics K, K4, D, D4 and T. Also we define versions of this systems for which the intended interpretation of terms is proof tactics, computable procedures able to find proofs of some formulas, having formula as input.

Artemov's logic of proofs LP is a complete calculus of propositions and proofs, which is now becoming a foundation for the evidence-based approach to reasoning about knowledge. Additional atoms in LP have form t:F, read as “t is a proof of F” (or, more generally, as “t is an evidence for F”) for an appropriate system of terms t called proof polynomials. In this paper, we answer two well-known questions in this area. One of the main features of LP is its ability to realize modalities in any S4-derivation by proof polynomials thus revealing a statement about explicit evidences encoded in that derivation. We show that the original Artemov's algorithm of building such realizations can produce proof polynomials of exponential length in the size of the initial S4-derivation. We modify the realization algorithm to produce proof polynomials of at most quadratic length. We also found a modal formula, any realization of which necessarily requires self-referential constants of type c:A(c). This demonstrates that the evidence-based reasoning encoded by the modal logic S4 is inherently self-referential.

Artemov's logic of proofs LP is a complete calculus of propositions and proofs, which is now becoming a foundation for the evidence-based approach to reasoning about knowledge. Additional atoms in LP have form t:F, read as “t is a proof of F” (or, more generally, as “t is an evidence for F”) for an appropriate system of terms t called proof polynomials. In this paper, we answer two well-known questions in this area. One of the main features of LP is its ability to realize modalities in any S4-derivation by proof polynomials thus revealing a statement about explicit evidences encoded in that derivation. We show that the original Artemov's algorithm of building such realizations can produce proof polynomials of exponential length in the size of the initial S4-derivation. We modify the realization algorithm to produce proof polynomials of at most quadratic length. We also found a modal formula, any realization of which necessarily requires self-referential constants of type c:A(c). This demonstrates that the evidence-based reasoning encoded by the modal logic S4 is inherently self-referential.

Keywords: logic of proofs, self-reference, modal logic

Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms d, t, b, 4, and 5 with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for KB5 and S5 by showing that the positive introspection operator is superfluous.

Keywords: justification logic, modal logic, realization theorem, nested sequents, positive introspection

We consider the logic of justified common knowledge S4_n^J introduced in [Art04TR]. This system captures the notion of justified common knowledge, which is free of some of the deficiencies of the usual common knowledge operator, and yet sufficient for analysis of epistemic problems where common knowledge has been traditionally applied. In particular, S4_n^J enjoys cut-elimination, which opens a possibility for an automatic proof search in logic of common knowledge. In this paper, we present an implementation that automatically builds cut-free proofs in S4_n^J. Our work is based on the existing matrix-based prover for intuitionistic logic [SchLorKreNog01].

An efficient proof assistant uses a wide range of decision procedures, including automatic verification of validity of arithmetical formulas with linear terms. Since the final product of a proof assistant is a formalized and verified proof, it prompts an additional task of building proofs of formulas, which validity is established by such a decision procedure.

We present an implementation of several decision procedures for arithmetical formulas with linear terms in the MetaPRL proof assistant in a way that provides formal proofs of formulas found valid by those procedures.

We also present an implementation of a theorem prover for the logic of justified common knowledge S4_n^J introduced in [Art04TR]. This system captures the notion of justified common knowledge, which is free of some of the deficiencies of the usual common knowledge operator, and is yet sufficient for the analysis of epistemic problems where common knowledge has been traditionally applied. In particular, S4_n^J enjoys cut-elimination, which introduces the possibility of automatic proof search in the logic of common knowledge. Our implementation automatically builds cut-free sequent proofs in S4_n^J. This prover is based on the existing matrix-based prover for intuitionistic logic [SchLorKreNog01].

Justification Logic is a framework for reasoning about evidence and justification. Public Announcement Logic is a framework for reasoning about belief changes caused by public announcements. This paper develops JPAL, a dynamic justification logic of public announcements that corresponds to the modal theory of public announcements due to Gerbrandy and Groeneveld. JPAL allows us to reason about evidence brought about by and changed by Gerbrandy–Groeneveld-style public announcements.

Keywords: justification logic, dynamic epistemic logic, public announcements, belief revision

It is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems.

Keywords: justification logics, common knowledge, proof theory

Justification logics are epistemic logics that explicitly include justifications for the agents' knowledge. We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripke-style semantics that is similar to Fitting's semantics for the Logic of Proofs LP. We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics. We demonstrate that our logic is a conservative extension of Yavorskaya's minimal bimodal explicit evidence logic, which is a two-agent version of LP. We discuss the relationship of our logic to the multi-agent modal logic S4 with common knowledge. Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.

Justification logics are epistemic logics that explicitly include justifications for the agents' knowledge. We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripke-style semantics that is similar to Fitting's semantics for the Logic of Proofs LP. We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics. We demonstrate that our logic is a conservative extension of Yavorskaya's minimal bimodal explicit evidence logic, which is a two-agent version of LP. We discuss the relationship of our logic to the multi-agent modal logic S4 with common knowledge. Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.

Keywords: justification logic, epistemic modal logic, multi-agent systems, common knowledge

Justification logic is an epistemic framework that provides a way to express explicit justifications for the agent's belief. In this paper, we present OPAL, a dynamic justification logic that includes term operators to reflect public announcements on the level of justifications. We create dynamic epistemic semantics for OPAL. We also elaborate on the relationship of dynamic justification logics to Gerbrandy–Groeneveld's PAL by providing a partial realization theorem.

Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound.

Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are Π^p₂-hard, reproving and generalizing an earlier result by Milnikel.

Keywords: justification logic; logic of proofs; computational complexity; Π^p₂-completeness; Derivability problem

Classical logic of proofs LP naturally extends propositional calculus to the language enriched with formulas meaning t is a proof of formula F. Intuitionistic logic of proofs iLP introduced by Artemov and Iemhoff was conjectured to be complete with respect to intuitionistic arithmetic HA. The article presents a proof of this conjecture.

Keywords: logic of proofs, intuitionistic arithmetic, admissible rules

The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis that all truths are knowable entails the implausible conclusion that all truths are known. The notoriety of this argument owes to the negative light it appears to cast on the view that there can be no verification-transcendent truths. We argue that it is overly simplistic to formalize the views of contemporary verificationists like Dummett, Prawitz or Martin-Löf using the sort of propositional modal operators which are employed in the original derivation of the Paradox. Instead we propose that the central tenet of verificationism is most accurately formulated as follows: if φ is true, then there exists a proof of φ. Building on the work of Artemov [Art01BSL], a system of explicit modal logic with proof quantifiers is introduced to reason about such statements. When the original reasoning of the Paradox is developed in this setting, we reach not a contradiction, but rather the conclusion that there must exist non-constructed proofs. This outcome is evaluated relative to the controversy between Dummett and Prawitz about proof existence and bivalence.

Keywords: Knowability Paradox, Fitch, verificationism, intuitionistic logic, BHK interpretation, existence predicate, logic of proofs, potential proof, bivalence

The Knower Paradox demonstrates that any theory T which 1) extends Robinson arithmetic Q, 2) includes a predicate K(x) intended to formalize “the formula with godel number x is known by agent i,” and 3) contains certain elementary epistemic principles involving K(x) is inconsistent. The purpose of this paper is to show how this paradox may be redeveloped within a system of quantified explicit modal logic in the tradition of Artemov [Art01BSL] and Fitting [Fit04TRb], [Fit05APAL] which we argue allows for a more faithful formulation of some of the epistemic principles on which it is based. Along the way, we isolate a principle – the so-called Uniform Barcan Formula [UBF] – which we show is required to derive an explicit counterpart of the axiom U (i.e. K(⌈K(⌈φ⌉) → φ⌉)) which was used in the original formulation of the Paradox. We argue that since there are independent epistemic reasons to be suspicious of UBF, the paradox may be resolved by abandoning this principle (and thereby U as well).

The Knower Paradox demonstrates that any theory T which 1) extends Robinson arithmetic Q, 2) includes a predicate K(x) intended to formalize “the formula with godel number x is known by agent i,” and 3) contains certain elementary epistemic principles involving K(x) is inconsistent. The purpose of this paper is to show how this paradox may be redeveloped within a system of quantified explicit modal logic in the tradition of Artemov [Art01BSL] and Fitting [Fit04TRb], [Fit05APAL] which we argue allows for a more faithful formulation of some of the epistemic principles on which it is based. Along the way, we isolate a principle – the so-called Uniform Barcan Formula [UBF] – which we show is required to derive an explicit counterpart of the axiom U (i.e. K(⌈K(⌈φ⌉) → φ⌉)) which was used in the original formulation of the Paradox. We argue that since there are independent epistemic reasons to be suspicious of UBF, the paradox may be resolved by abandoning this principle (and thereby U as well).

The logic of proofs (LP) was proposed as Gödel's missed link between Intuitionistic and S4-proofs, but so far the tableau-based methods proposed for LP have not explored this closeness with S4 and contain rules whose analycity is not immediately evident. We study possible formulations of analytic tableau proof methods for LP that preserve the subformula property. Two sound and complete tableau decision methods of increasing degree of analycity are proposed, KELP and preKELP. The latter is particularly inspired on S4-proofs. The crucial role of proof constants in the structure of LP-proofs methods is analysed. In particular, a method for the abduction of proof constant specifications in strongly analytic preKELP proofs is presented; abduction heuristics and the complexity of the method are discussed.

Keywords: Logic of proofs, tableaux, KE tableaux

An axiomatic formulation of a logic called LPS4 appears in [ArtNog04TR]. Here that logic is proved sound and complete with respect to the weak semantics of [Fit05APAL]. Also a tableau system for LPS4 is introduced, and also proved sound and complete with respect to the semantics, thus establishing both cut elimination and equivalence with the axiomatic formulation.

An extension, QLP, of the propositional logic of explicit proofs, LP, is created, allowing quantification over proofs. The resulting logic is given an axiomatization, a Kripke-style semantics, and soundness and completeness are shown. It is shown that S4 embeds into the logic, when we translate the necessity operator using a quantifier: there exists an explicit proof. And it is shown that the propositional part of QLP is exactly LP. No connection with arithmetic provability is made.

A new semantics is presented for the logic of proofs (LP), ([Art95TR], [Art01BSL]) based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.

A well-known problem with Hintikka-style logics of knowledge is that of logical omniscience. One knows too much. This breaks down into two subproblems: one knows all tautologies, and one's knowledge is closed under consequence. A way of addressing the second of these is to move from knowledge simpliciter, to knowledge for a reason. Then, as consequences become `further away' from one's basic knowledge, reasons for them become more complex, thus providing a kind of resource measurement.

One kind of reason is a formal proof. Sergei Artemov has introduced a logic of explicit proofs, LP. I present a semantics for this, based on the idea that it is a logic of knowledge with explicit reasons. A number of fundamental facts about LP can be established using this semantics. But it is equally important to realize that it provides a natural logic of more general applicability than its original provenance, arithmetic provability.

Gödel suggested the creation of a propositional logic of explicit proofs, and recently this suggestion was carried out by Artemov, to produce the logic LP. This logic can, in fact, be looked at more generally as a logic of explicit evidence. A major result about LP is the Realization Theorem, that says any theorem of S4 can be converted into a theorem of LP by some replacement of necessitation symbols with explicit proof terms. Thus the necessitation operator of S4 can be seen as a kind of implicit existential quantifier: there exists explicit evidence such that.... I introduce quantification over evidence into LP, and show that the connection between S4 necessitation and the existential quantifier is an explicit one. The extension of LP with quantifiers is called QLP. I will sketch its semantics and axiomatization.

A propositional logic of explicit proofs, LP, was introduced in [Art01BSL], completing a project begun long ago by Gödel, [Goed38CW]. LP can be looked at more generally as a logic of explicit evidence, something currently being investigated. The Realization Theorem for LP says that any theorem of S4 can be converted into a theorem of LP by some replacement of necessitation symbols with explicit proof terms. Thus [] of S4 is a kind of implicit existential quantifier: there exists a proof term (explicit evidence) such that.... Here, quantification over evidence is added to LP, and it is shown that the connection between S4 necessitation and the existential quantifier is direct. The extension of LP with quantifiers is called QLP. A semantics and an axiom system for QLP are given, soundness and completeness are established, and several results are proved relating QLP to LP and to S4.

Keywords: logic of knowledge, modal logic, Kripke semantics, LP

The replacement theorem for classical and normal modal logics is a fundamental tool. It says that if A and B have been proved equivalent, occurrences of A in a formula may be replaced with occurrences of B to produce a formula equivalent to the original one. This theorem does not hold for LP, Logic of Proofs. A replacement for replacement is not simple to formulate. In this note I have provided one, along with some machinery for working with LP realizations that may prove useful for other things as well.

Suppose X is a theorem of S4, and a realization for X has been constructed. If X' is a substitution instance of X, it is also a theorem of S4, and so is realizable, but the only available algorithm for producing a realization of X', so far, has been to apply a general realization algorithm to a cut-free proof of X'. In effect we start over and the realization of X plays no role. It is the purpose of this report to present an algorithm for realizing substitution instances of a realizable formula that is, we believe, more efficient than a simple appeal to a general realization algorithm itself.

LP can be seen as a logic of knowledge with justifications. Artemov's Realization Theorem says justifications can be extracted from validities in the Hintikka-style logic of knowledge S4, where they are not explicitly present. We provide tools for reasoning about justifications directly. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. The results are algorithmic in nature—semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov's Realization Theorem itself.

Several justification logics have evolved, starting with the logic LP, [Art01BSL]. These can be thought of as explicit versions of modal logics, or logics of knowledge or belief in which the unanalyzed necessity operator has been replaced with a family of explicit justification terms. Modal logics come in various strengths. For their corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, extensions are actually conservative. Our method of proof is very simple, and general enough to also handle several justification logics not directly corresponding to modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open.

The logic S4LP combines the modal logic S4 with the justification logic LP. This is the case both axiomatically and semantically, though of course the real story is in the details. We introduce a simple restriction on the behavior of constants in S4LP, a restriction that has no effect on the LP sublogic. With this assumed, some very powerful derived rules are established. Then these are used to show we have completeness relative to a semantics having what we call the local realizability property. This means that at each world of such a model, for each formula true at that world there is a realization also true at that world, where a realization is the result of replacing all modal operators with explicit justification terms. This is part of a attempt to understand the deeper aspects of Artemov's Realization Theorem, though it is not yet clear just how the results obtained here relate to that theorem.

Several justification logics have evolved, starting with the logic LP, [Art01BSL]. These can be thought of as explicit versions of modal logics, or logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. Modal logics come in various strengths. For their corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open.

A propositional logic of explicit proofs, LP, was introduced in [Art01BSL], completing a project begun long ago by Gödel, [Goed38CW]. LP can be looked at in a more general way, as a logic of explicit evidence, and there have been several papers along these lines. A major result about LP is the Realization Theorem, that says any theorem of S4 can be converted into a theorem of LP by some replacement of necessitation symbols with explicit proof terms. Thus the necessitation operator of S4 can be seen as a kind of implicit existential quantifier: there exists a proof term (explicit evidence) such that.... In this paper, quantification over evidence is introduced into LP, and it is shown that the connection between S4 necessitation and the existential quantifier becomes an explicit one. The extension of LP with quantifiers is called QLP. A semantics and an axiom system for QLP are given, soundness and completeness are established, and several results are proved relating QLP to LP and to S4.

Keywords: logic of proofs, justification logic, logic of knowledge, modal logic, realization theorem

The logic S4LP combines the modal logic S4 with the justification logic LP, both axiomatically and semantically. We introduce a simple restriction on the behavior of constants in S4LP, having no effect on the LP sublogic. Under this restriction some powerful derived rules are established. Then these are used to show completeness relative to a semantics having what we call the local realizability property: at each world and for each formula true at that world there is a realization also true at that world, where a realization is the result of replacing all modal operators with explicit justification terms. This is part of a project to understand the deeper aspects of Artemov's Realization Theorem.

Several justification logics have been created, starting with the logic LP, ([Art01BSL]). These can be thought of as explicit versions of modal logics, or of logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. We begin by sketching the basics of justification logics and their relations with modal logics. Then we move to new material. Modal logics come in various strengths. For their corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open.

Keywords: logic, modal logic, logic of knowledge, justification logic, conservativity

This is an expository paper in which the basic ideas of a family of Justification Logics are presented. Justification Logics evolved from a logic called LP, introduced by Sergei Artemov [Art95TR], [Art01BSL], which formed the central part of a project to provide an arithmetic semantics for propositional intuitionistic logic. The project was successful, but there was a considerable bonus: LP came to be understood as a logic of knowledge with explicit justifications and, as such, was capable of addressing in a natural way long-standing problems of logical omniscience. Since then,LP has become one member of a family of related logics, all logics of knowledge with explicit knowledge terms. In this paper the original problem of intuitionistic foundations is discussed only briefly. We concentrate entirely on issues of reasoning about knowledge.

Keywords: logic of knowledge, justification logic, modal logic

LP can be seen as a logic of knowledge with justifications. See [Art08RSL] for a recent comprehensive survey of justification logics generally. Artemov's Realization Theorem says justifications can be extracted from validities in the more conventional Hintikka-style logic of knowledge S4, in which they are not explicitly present. Justifications, however, are far from unique. There are many ways of realizing each theorem of S4 in the logic LP. If the machinery of justifications is to be applied to artificial intelligence, or better yet, to everyday reasoning, we will need to work with whatever justifications we may have at hand—one version may not be interchangeable with another, even though they realize the same S4 formula. In this paper we begin the process of providing tools for reasoning about justifications directly. The tools are somewhat complex, but in retrospect this should not be surprising. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. (The second of these is actually weaker than just stated, but this is not the place for a detailed formulation.) The results are algorithmic in nature—semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov's Realization Theorem itself. This paper is a much extended version of [Fit07LFCS].

Keywords: logic of proofs, justification logic, logic of knowledge, modal logic, realization theorem

Hybrid logics internalize their own semantics. Members of the newer family of justification logics internalize their own proof methodology. It is an appealing goal to combine these two ideas into a single system, and in this paper we make a start. We present a hybrid/justification version of the modal logic T. We give a semantics, a proof theory, and prove a completeness theorem. In addition, we prove a Realization Theorem, something that plays a central role for justification logics generally. Since justification logics are newer and less well known than hybrid logics, we sketch their background, and give pointers to their range of applicability. We conclude with suggestions for future research. Indeed, the main goal of this paper is to encourage others to continue the investigation begun here.

Keywords: hybrid logic, justification logic, logic of proofs, nominals

In [ArtTYav11TR] an elegant formulation of the first-order logic of proofs was given, FOLP. That report also proved an arithmetic completeness theorem, and a realization theorem for the logic. In this report we provide a possible-world semantics for FOLP, based on the propositional semantics of [Fit05APAL]. Motivation and intuition for the logic itself can be found in [ArtTYav11TR], and are not discussed here. We also give an Mkrtychev semantics for FOLP. This report was essentially completed June 10, 2011.

Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants of each other, roughly in the same way that Gentzen sequent calculi and tableaus are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators.

Keywords: modal logic; tableau; sequent; prefixed tableau; nested sequent

In this paper, we will introduce justification counterparts for some distributed knowledge systems. Our justified systems have explicit knowledge operators of the form [[t]]_i F and [[t]]_D F, which are interpreted respectively as “t is a justification that agent i accepts for F”, and “t is a justification that all agents implicitly accept for F”. We then present Kripke style models, called pseudo-Fitting, and prove the completeness theorem. Finally, using labelled sequent calculus of distributed knowledge systems and the fully explanatory property of pseudo-Fitting models, we establish the realization theorem.

Epistemic logics with justification, S4LP and S4LPN, are combinations of the modal epistemic logic S4 and the Logic of Proofs LP, with some connecting principles. These logics together with the modal knowledge operator []F (F is known), contain infinitely many operators of the form t:F (t is a justification for F), where t is a term. Regarding the Realization Theorem of S4, LP is the justification counterpart of S4, in the sense that, every theorem of S4 can be transformed into a theorem of LP (by replacing all occurrences of [] by suitable terms), and vise versa. In this article, we first introduce a new cut-free sequent calculus LP^G_L for LP, and then extend it to obtain a cut-free sequent calculus for S4LP and a cut-free hypersequent calculus for S4LPN. All cut elimination theorems are proved syntactically. Moreover, these sequent systems enjoy a weak subformula property. Then, we show that theorems of S4LP can be realized in LP and theorems of S4LPN can be realized in JS5 (the justification counterpart of modal logic S5). Consequently, we prove that S4LP and S4LPN are conservative extensions of LP.

Keywords: logic of proofs, realization theorem, sequent calculus, hypersequent calculus, cut elimination, subformula property

The logic of proofs is known to be complete for the semantics of proofs in PA. In this paper we present a refinement of this theorem, we will show that we can assure that all the operations on proofs can be realized by feasible, that is PTIME-computable, functions. In particular we will show that the logic of proofs is complete for the semantics of proofs in Buss' bounded arithmetic S₂¹.

In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly the intersection of S4 and GL and equals the fragment that can be realized by proof-terms of LP. Additionally we show that the problem of determining which implicit provability assertions in a given modal formula can be made explicit is decidable. In the final sections of this paper we establish the disjunction property for GLA and give an axiomatization for the intersection of GL and S4.

The logic of proofs is known to be complete for the semantics of proofs in Peano Arithmetic PA. In this paper we present a refinement of this theorem, we will show that we can assure that all the operations on proofs can be realized by feasible, that is PTIME-computable, functions. In particular we will show that the logic of proofs is complete for the semantics of proofs in Buss' bounded arithmetic S₂¹. In view of recent applications of the Logic of Proofs in epistemology this result shows that explicit knowledge in the propositional framework can be made computationally feasible.

This paper studies a particular interpretation of propositional modal logic into propositional modal logic. Under an epistemic reading of the modality this interpretation can be understood as taking knowledge to be true belief. All normal modal logics of belief that under this definition of knowledge give rise to S5 as the logic of knowledge are determined. And all the normal modal logics of belief that give rise to S4w5 as the logic of knowledge are determined. Among the latter KD45 shows up as a maximal such logic.

In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly the intersection of S4 and GL and equals the fragment that can be realized by proof-terms of LP. In the final section of this paper we establish the disjunction property for GLA and give an axiomatization for the intersection of GL and S4.

This paper presents a semantics for the logic of proofs LP in which all the operations on proofs are realized by feasibly computable functions. More precisely, we will show that the completeness of LP for the semantics of proofs of Peano Arithmetic extends to the semantics of proofs in Buss' bounded arithmetic S₂¹. In view of applications in epistemology of LP in particular and justification logics in general this result shows that explicit knowledge in the propositional framework can be made computationally feasible.

Keywords: logic of proofs, bounded arithmetic

We establish the bi-modal forgetful projection of the Logic of Proofs and Formal Provability GLA. That is to say, we present a normal bi-modal provability logic with modalities [] and [×] whose theorems are precisely those formulas for which the implicit provability assertions represented by the [×] modality can be realized by explicit proof terms.

Keywords: justification logic, provability logic, realization theorem

We examine four approaches for dealing with the logical omniscience problem and their potential applicability: the syntactic approach, awareness, algorithmic knowledge, and impossible possible worlds. Although in some settings these approaches are equi-expressive and can capture all epistemic states, in other settings of interest they are not. In particular, adding probabilities to the language allows for finer distinctions between different approaches.

The basic logic of proofs consists of the propositional schemes that are valid about the proof predicate Prf(x, y). It is a logic in the language of propositional logic extended by expressions t:A, where t is an atom and A a formula, that are interpreted as “t is a proof of A”. We will present an arithmetical completeness theorem for the basic intuitionistic logic of proofs, that is a completeness theorem w.r.t. Heyting Arithmetic. This result disproves the conjecture that the intuitionistic logic of proofs consists of intuitionistic logic extended by the characteristic axioms of the classical logic of proofs and the law of excluded middle for expressions t:A. We will briefly comment on the extension of the result to the case in which functions on proof terms are allowed. This is joint work with Sergei Artemov.

Artemov's system LP captures all propositional invariant properties of a proof predicate “x proves y” ([Art95TR], [Art01BSL]). Kuznets in [Kuz00CSL] showed that the satisfiability problem for LP belongs to the class Π₂^p of the polynomial hierarchy. No nontrivial lower complexity bound for LP is known. We describe quite expressive syntactical fragment of LP which belongs to NP. It is rLP_{∧ ,∨} – the set of all theorems of LP which are monotone boolean combinations of quasiatomic formulas (facts of sort “t proves F”).

A new decision algorithm for this fragment is proposed. It is based on a new simple independent formalization for rLP (the reflected fragment of LP) and involves the corresponding proof search procedure. Essentially rLP contains all the theorems of LP supplied with additional information about their proofs. We show that in many respects rLP is simpler than LP itself. This gives the complexity bound (NP) for rLP. In addition we prove a suitable variant of the disjunctive property which extends this bound to rLP_{∧ ,∨}.

Keywords: proof theory, explicit modal logic, logic of proofs, proof polynomials, symbolic models, disjunctive property, complexity

We study the syntax of Artemov's Reflective Combinatory Logic RCL_→. We provide the explicit definition of types for RCL_→ and prove that every well-formed term has a unique type. We establish that the typability testing and detailed type restoration can be done in polynomial time and that the derivability relation for RCL_→ is decidable and PSPACE-complete. These results also formalize the intended semantics of the type t:F in RCL_→. Terms RCL_→ store the complete information about the judgment “t is a term of type F”, and this information can be extracted by the type restoration algorithm.

Artemov's propositional logic of proofs LP captures all invariant properties of proof predicates “t is a proof of F” which are represented in LP as formulas t:F. Kuznets in [Kuz00CSL] showed that the satisfiability problem for LP belongs to the class Π₂^p of the polynomial hierarchy. In this paper we consider the reflected logic of proofs, rLP, consisting of formulas t:F derivable in LP. The system rLP is as expressible as LP itself, since every F derivable in LP is represented in rLP by t:F for an appropriate proof term t. We prove a better upper bound (NP) for the decision procedure in rLP. In addition we prove the disjunctive property for the original logic of proofs LP, thus answering a well-known question in this area.

Keywords: logic of proofs, proof polynomials, symbolic models, disjunctive property, complexity

We study Artemov's Reflective Combinatory Logic RCL_→. We provide the explicit definition of types for RCL_→ and prove that every well-formed term has a unique type. We establish that the typability testing and detailed type restoration can be done in polynomial time and that the derivability relation for RCL_→ is decidable and PSPACE-complete. These results also formalize the intended semantics of the type t:F in RCL_→. Terms RCL_→ store the complete information about the judgment “t is a term of type F”, and this information can be extracted by the type restoration algorithm.

Keywords: proof theory, reflective combinatory logic, well-formed formula, typing, derivability, complexity, cut elimination

The extended operational (term-labeled modal) language is used to give the axiomatic description for functional proof predicate supplied with effective operations on proofs induced by modus ponens and necessitation rules. An additional operation is involved which restores a statement from its proof. The arithmetical completeness and decidability theorems are proved. The cut-elimination property for Gentzen style reformulation of corresponding logic is established.

The logic of single-conclusion (functional) proofs (FLP) is introduced. It combines the verification property of proofs with the single valuedness of proof predicate and describes the operations on proofs induced by modus ponens rule and proof checking. It is proved that FLP is decidable, sound and complete with respect to arithmetical proof interpretations based on single-valued proof predicates. The application to arithmetical inference rules specification and PA-admissibility testing is considered. We show that the provability in FLP gives the complete admissibility test for the rules which can be specified by schemes in FLP-language. The test is supplied with the ground proof extraction algorithm which eliminates the admissible rules from a PA-proof by utilizing the information from the corresponding FLP-proofs.

Keywords: logic of proofs, explicit modal logic, single-conclusion proof predicate, proof term, inference rule specification, admissible rule

We propose an extension of the propositional proof logic language by the second-order variables denoting the reference constructors (like `the formula which is proven by x'). The proof logic in this weak second-order language is axiomatized via the calculus FLP_ref, the (Functional) Logic of Proofs with References. It is supplied with the formal arithmetical semantics: we prove that FLP_ref is sound with respect to arithmetical interpretations and is a conservative extension of propositional single-conclusion proof logic FLP. Finally, we demonstrate how the language of FLP_ref can be used as a scheme language for arithmetic and provide the corresponding proof conversion method.

Keywords: proof theory, explicit modal logic, single conclusion logic of proofs, proof term, reference, unification

We introduce an extension of the propositional logic of single-conclusion proofs by the second-order variables denoting the reference constructors of the type “the formula which is proved by x.” The resulting Logic of Proofs with References, FLP_ref, is shown to be decidable, and to enjoy soundness and completeness with respect to the intended provability semantics. We show that FLP_ref provides a complete test of admissibility of inference rules in a sound extension of arithmetic. This paper may be regarded as a contribution to the theory of automated reasoning systems.

Keywords: proof theory, explicit modal logic, single conclusion logic of proofs, proof term, reference, unification, admissible inference rule

Symbolic semantics for logics of proofs based on Mkrtychev models covers the the case of multi-conclusion proof logics. We propose symbolic models for single-conclusion proof logics (FLP and its extensions). The corresponding soundness and completeness theorems are proven. The developed symbolic model technique is used to establish the consistency of contexts required for proof internalization. In particular, we construct an extension of FLP that enjoys the strong proof internalization property with empty context.

In this paper we define symbolic models for Single-Conclusion Logics of Proofs. We prove the soundness and completeness of these logics with respect to the corresponding classes of symbolic models. We apply the semantic methods developed in this paper to justify the use of terms of single-conclusion logic of proofs as notation for derivations in this logic.

Keywords: formal derivation, proof predicate, single-conclusion logic of proofs, Mkrtychev models, internalization property

Justification Logic is a new generation of epistemic logics which along with the traditional modal knowledge/belief operators also consider justification assertions `t  is a justification for F.' In this paper, we introduce a prefixed tableau system for one of the major logics of this kind S4LPN, which combines the logic of proofs (LP) and epistemic logic S4 with an explicit negative introspection principle ¬t:F → []¬t:F. We show that the prefixed tableau system for S4LPN is sound and complete with respect to Fitting-style semantics. We also introduce a hypersequent calculus HS4LPN and show that HS4LPN is complete as far as we confine ourselves to a case where only a single formula is to be proven. We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus. This completeness result gives us a semantic proof of cut-admissibility for S4LPN under the aforementioned restriction.

Justification logic is a new generation of epistemic logics which along with the traditional modal knowledge/belief operators also consider justification assertions `t is a justification for F.' In this paper, we introduce a prefixed tableau system for one of the major logics of this kind S4LPN, which combines the Logic of Proofs (LP) and epistemic logic S4 with an explicit negative introspection principle ¬t:F →[]¬t:F. We show that the prefixed tableau system for S4LPN is sound and complete with respect to Fitting-style semantics. We also introduce a hypersequent calculus HS4LPN and show that HS4LPN is complete. We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus. This completeness result gives us a semantic proof of cut-admissibility for S4LPN. We conclude the paper by discussing a subsystems of S4LPN, namely S4LP.

Keywords: hypersequents, tableaux, justification logic, modal logic

In linear logic, a formula !A with the modality ! means that A can be duplicated as many times as we like. We can paraphrase this as `A holds with an empty resource'. Then it is natural to generalize formulas with modalities to the form s:A with a term s, of which meaning is that A holds if there is a resource s. Terms are interpreted as elements of a well-ordered set; ! is interpreted as the least element. In this paper, we present an extended system of linear logic with such formulas s:A as `linear logic with explicit resources'. We show some basic properties of the logic: the soundness and completeness theorems with respect to a denotational semantics (Phase semantics), the cut-elimination theorem (normalization theorem). In addition, we consider the fragment containing no ! and prove the faithful embeddability of (ordinary) linear logic in the fragment.

Explicit modal logic was introduced by S. Artemov. Whereas the traditional modal logic uses atoms []F with a possible semantics “F is provable”, the explicit modal logic deals with atoms of form t:F, where t is a proof polynomial denoting a specific proof of a formula F. Artemov found the explicit modal logic LP in this new format and built an algorithm that recovers explicit proof polynomials corresponding to modalities in every derivation in K. Gödel's modal provability calculus S4. In this paper we study the complexity of LP as well as the complexity of explicit counterparts of the modal logics K, D, T, K4, D4 found by V. Brezhnev. The main result: the satisfiability problem for each of these explicit modal logics belongs to the class Σ₂^p of the polynomial hierarchy. Similar problem for the original modal logics is known to be PSPACE-complete. Therefore, explicit modal logics have much better upper complexity bounds than the original modal logics.

Logic of Proofs LP introduced by Artemov gave an exact intended semantics for Gödel's logic of provability S4 [Art95TR], [Art01BSL]. This Logic of Proofs considers statements of the form t:F where a proof term t (called proof polynomial) denotes a proof for F. Proof polynomials are built from variables and proof constants c which stand for proofs of axioms of the theory. Logic of Proofs has a natural arithmetical semantics where t:F is interpreted as a formal arithmetical statement “t is a proof of F in PA.” Proof constants are specified by accepting as postulates constant specifications CS which are sets of formulas of sort {c₁:A₁, c₂:A₂, ...} where c_i is a proof constant and A_i an axiom. A theory LP_CS is a theory with constant specification CS. Logic LP₀ corresponding to the empty CS was shown to be decidable in [Art95TR]. Mkrtychev in [Mkr97LFCS] has shown that if CS contains only a finite number of axiom schemes for each constant then LP_CS is decidable. We show that those results do not extend to all decidable constant specifications.

Theorem 1. There is a decidable constant specification CS such that the logic LP_CS is undecidable.

Moreover, it can be shown that even a decidable constant specification involving only one constant already may lead to an undecidable theory LP_CS.

Logic of Proofs LP introduced by Artemov gave an exact intended semantics for Gödel's logic of provability S4 (see [Art01BSL]). This Logic of Proofs considers statements of the form t:F, where a proof term t (called proof polynomial) denotes a proof for F. Logic of Proofs has a natural arithmetical semantics where t:F is interpreted as a formal arithmetical statement “t is a proof of F in PA.” We show that the smallest proof polynomial that proves F can serve as a measure of how long is the shortest Hilbert-style proof of t:F.

Theorem 1. Let t be the smallest term such that LP |- t:F. Let L₁ be the shortest Hilbert-style derivation of t:F in LP. Then

dag(t) ≤ |L_1| ≤ 3|t|,

where |t| is the size of the syntactic tree of term t, dag(t) is the size of the syntactic direct acyclic graph (dag) of term t, and |L₁| is the number of formulas in derivation L₁.

We further extend this result to Hilbert-style proofs of propositional tautologies:

Theorem 2. Let F be a propositional tautology. Let t be the smallest term such that LP |- t:F. Let t' be the dag-smallest term such that LP |- t':F. Let L₂ be the shortest Hilbert-style propositional derivation of F. Then

dag(t') ≤ |L_2| = O(|t|).

One of the applications of modal logic is provability logic with []F read as `formula F is provable (in a theory T).' Another application is epistemology logic where []F is understood as `formula F is known (by an agent a).' Recently developed logic LP (see [Art01BSL]) provides an explicit version for both applications. Using t:F to mean `F is provable and t represents its proof' in provability case or `F is known and t justifies this knowledge' in epistemology case allows for a finer grained discussion. It was shown ([Art01BSL]) that LP is an explicit counterpart of modal logic S4, which can be viewed both as an informal provability logic and a logic of knowledge.

In principle, one can imagine a proof or a justification that refers to itself. For example, it would make sense to reserve one uniform justification for all circular reasoning instances; such a justification, in particular, would apply to every circular reasoning about this very justification. The language of modal logic is too poor to capture this notion of self-referentiality. Its explicit counterpart, on the contrary, can distinguish between self-referential and non-self-referential justifications.

We tried to answer the following question: Is self-referentiality crucial for the provability/knowledge encompassed by modal logic S4? The following theorem affirms that it is.

Theorem 1. Some theorems of S4 require self-referential proofs to be given an explicit realization in LP, e.g., ¬[]¬(S → []S).

A system of evidence-based knowledge S4LP was recently proposed by Artemov and Nogina. It combines epistemic modal operator with explicit evidence represented by evidence terms similar to those of Artemov's Logic of Proofs. This logic S4LP and its generalizations promise a new approach to common-knowledge and to the logical omniscience problem. In this paper, we show that this logic is PSPACE-complete. Thus adding explicit evidence to S4 does not seem to increase the complexity of the logic.

The problem of the identity criteria for proofs can be traced to Hilbert and Prawitz. One of the approaches, which uses the concept of generality of proofs, was suggested in 1968 by Lambek. Following his ideas, we propose a language and a logic to represent Hilbert-style proofs for classical propositional logic by adapting the Logic of Proofs (LP) introduced by Artemov in 1994. We prove that proof polynomials, the objects representing Hilbert derivations in LP, are sufficient to realize all propositional derivations, with or without hypotheses. We also show that proof polynomials respect the ideas of generality and provide an algorithm for determining whether two given proof polynomials represent the same proof. These results naturally extend similar properties of combinatory logic demonstrated by Hindley. The language of LP allows us to formally capture more structure of Hilbert-style proofs. In particular, we show how the well-known phenomenon of proof composition in classical logic manifests itself in the case of Hilbert proofs.

Justification Logic is an emerging field that studies provability, knowledge, and belief via explicit proofs or justifications that are part of the language. There exist many justification logics closely related to modal epistemic logics of knowledge and belief. Instead of modality [] in pure justification logics, or in addition to modality [] in hybrid logics, which has an existential epistemic reading `there exists a proof of F,' all justification logics use constructs t:F, where a justification term t represents a blueprint of a Hilbert-style proof of F. The first justification logic, LP, introduced by Sergei Artemov, was shown to be a justification counterpart of modal logic S4 and serves as a missing link between S4 and Peano arithmetic, thereby solving a long-standing problem of provability semantics for S4 and Int.

The machinery of explicit justifications can be used to analyze well-known epistemic paradoxes, e.g. Gettier's examples of justified true belief that can hardly be considered knowledge, and to find new approaches to the concept of common knowledge. Yet another possible application is the Logical Omniscience Problem, which reflects an undesirable property of knowledge as described by modality when an agent knows all the logical consequences of his/her knowledge. The language of justification logic opens new ways to tackle this problem.

This thesis focuses on quantitative analysis of justification logics. We explore their decidability and complexity of Validity Problem for them. A closer analysis of the realization phenomenon in general and of one procedure in particular enables us to deduce interesting corollaries about self-referentiality for several modal logics. A framework for proving decidability of various justification logics is developed by generalizing the Finite Model Property. Limitations of the method are demonstrated through an example of an undecidable justification logic. We study reflected fragments of justification logics and provide them with an axiomatization and a decision procedure whose complexity (the upper bound) turns out to be uniform for all justification logics, both pure and hybrid. For many justification logics, we also present lower and upper complexity bounds.

The principal result of Justification Logic is the Realization Theorem, which states that behind major epistemic modal logics there are corresponding systems of evidence/justification terms sufficient for reading all provable knowledge assertions as statements about justifications. A knowledge/belief modality is self-referential if there are modal sentences that cannot be realized without using self-referential evidence of type “t is a proof of A(t).” Building on an earlier result that S4 and its justification counterpart LP describe knowledge that is self-referential, we show that the same is true for K4, D4, and T with their justification counterparts whereas for K and D self-referentiality can be avoided. Therefore, no single modal axiom from the standard axiomatizations of these logics is responsible for self-referentiality.

Logics J, JD, JT, J4, JD4, and LP are explicit counterparts of modal epistemic logics K, D, T, K4, D4, and S4 respectively (see [Bre00TR], [Art07TRb] for more details). An upper bound of Σ₂^p for the satisfiability problem in these justification logics was announced in [Kuz00CSL]. The algorithm was essentially a propositional tableau procedure (though not presented as such) followed by a check on possible contradictions among justifications. The former part is traditionally NP while the latter was shown to be co-NP, thus yielding Σ₂^p as the total complexity.

Recently an omission was found in the proof for two of the six logics: JD and JD4. Restoring the upper bound for JD called for the use of prefixed tableaux. Below we provide the tableau-style formulation of the first part of the original algorithm for J, JT, J4, and LP as well as a new tableau algorithm for JD that help establish the Σ₂^p upper bound for satisfiability problems in all these 5 logics (note the integer prefixes used for JD).

J, J4     (T s:G)/(T *(s,G))    (F s:G)/(F *(s,G))

JT, LP     (T s:G)/(T G and T *(s,G))     (F s:G)/(F *(s,G) | F G)

JD     (n T s:G)/(n T *(s,G) and n+1 T G)     (n F s:G)/(n F *(s,G))

Whether the same bound holds for JD4 remains at this point an open problem.

This paper is devoted to the study of self-referential proofs and/or justifications, i.e., valid proofs that prove statements about these same proofs. The goal is to investigate whether such self-referential justifications are present in the reasoning described by standard modal epistemic logics such as S4. We argue that the modal language by itself is too coarse to capture this concept of self-referentiality and that the language of justification logic can serve as an adequate refinement. We consider well-known modal logics of knowledge/belief and show, using explicit justifications, that S4, D4, K4, and T with their respective justification counterparts LP, JD4, J4, and JT describe knowledge that is self-referential in some strong sense. We also demonstrate that self-referentiality can be avoided for K and D.

In order to prove the former result, we develop a machinery of minimal evidence functions used to effectively build models for justification logics. We observe that the calculus used to construct the minimal functions axiomatizes the reflected fragments of justification logics. We also discuss difficulties that result from an introduction of negative introspection.

Keywords: self-referentiality, justification logic, epistemic modal logic, Logic of Proofs

The Logic of Proofs LP, introduced by Artemov, encodes the same reasoning as the modal logic S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application ⋅, positive introspection !, and sum +) are sufficient to mimic provability concealed in S4 modality. While the first two operations go back to Gödel, the exact role of + remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.

A generalization of the Curry-Howard-Lambek isomorphism for Cartesian closed categories and typed lambda calculi is given for the LP categories with weak natural numbers object, which correspond to the positive conjunction fragment of the intuitionistic Logic of Proofs LP of Artemov, and LP-typed lambda calculi with natural numbers type.

We exploit the Justification Logic capabilities of reasoning about justifications, comparing pieces of evidence, and measuring the complexity of justifications in the context of argumentative agents. Not knowing all of the implications of their knowledge base, agents use justified arguments for reflection and guidance.

The logic of proofs was introduced by Artemov in order to analize the formalization of the concept of proof rather than the concept of provability. In this context, some operations on proofs play a very important role. In this paper, we investigate some very natural operations, paying attention not only to positive information, but also to negative information (i.e. information saying that something cannot be a proof). We give a formalization for a fragment of such a logic of proofs, and we prove that our fragment is complete and decidable.

Keywords: provability logic, logic of proofs, proof theory

In modal nonmonotonic logics, lack of proof of a formula φ is sufficient to conclude ¬[]φ. We will make use of explicit modal operators from Artemov's Logic of Proofs [Art01BSL] to establish non-provability of formulas in S4. Our eventual goal is to incorporate the these into sequent proofs for S4 skeptical consequence.

The Logic of Proofs realizes the modalities from traditional modal logics with proof polynomials, so an expression []F becomes t:F where t is a proof polynomial representing a proof of or evidence for F. The pioneering work on explicating the modal logic S4 is due to S. Artemov and was extended to several subsystems by V. Brezhnev. In 2000, R. Kuznets presented a Π₂^p algorithm for deducibility in these logics; in the present paper we will show that the deducibility problem is Π₂^p-complete. (The analogous problem for traditional modal logics is PSPACE-complete.) Both Kuznets's work and the present results make assumptions on the values of proof constants.

Keywords: Logic of Proofs, logic of belief, complexity

In [Fit08ISAIM], Fitting showed that the standard hierarchy of logics of justified knowledge is conservative (e.g. a logic with positive introspection operator ! is conservative over the logic without !). We do the same with most logics of justified belief, but taking a semantic approach rather than Fitting's syntactic one. A brief example shows that conservativity does not hold for logics of justified consistent belief.

In [Fit08ISAIM], Fitting showed that the standard hierarchy of logics of justified knowledge is conservative (e.g. a logic with positive introspection operator ! is conservative over the logic without !). We do the same with most logics of justified belief, showing both conservation of sequent proofs and extensibility of models. A brief example shows that conservativity does not hold for logics of justified consistent belief.

Keywords: justification logic, epistemic logic, logic of belief, proof theory

The operational logic of proofs LP was introduced by S. Artemov [Art95TR] as an operational version of S4. In this paper, we define a model for LP and prove the corresponding completeness theorem. Using this model, we prove the decidability of a variant of LP axiomatized by a finite set of schemes.

Logics with the strong provability operator “... is true and provable” together with the proof operators “p is a proof of ...” are axiomatized. Kripke-style completeness, decidability and arithmetical completeness of these logics are established.

Logics with the modal operator “... is true and provable” together with the modal proof operator “p is a proof of ...” are axiomatized. Kripke-style completeness, decidability and arithmetical completeness of these logics are established.

Keywords: provability, modal logic, Kripke model, arithmetical completeness, decidability

Joint logics of proofs and provability were studied in [Art94APAL] and [TYav01APAL]. The latter found an arithmetically complete logic which contained both the provability logic GL ([Boo93]) and the logic of proofs LP ([Art01BSL]) in their joint language augmented by some additional operations. A recent application in the logic of knowledge [ArtNog05TR] prompted a question of a complete axiomatization of the logic of proofs and provability in the original language of GL and LP.

In the current note we find such an axiomatization, GLA, consisting of axioms and rules of GL and LP together with axioms t:P → []P, ¬t:P → []¬t:P, t:[]P → P, and the reflection rule |-[]P ⇒ |-P. GLA has been supplied with a corresponding Kripke-style semantics and shown to be complete with respect to the intended arithmetical provability interpretation.

The logic of proofs and provability GLA [Nog06LC] is an arithmetically complete system that combines the provability logic GL and Artemov's Logic of Proofs LP (cf. [Art07MLH]) in their joint language. GLA has become a prototype of epistemic logics with justification [Art07MLH], [ArtNog05TARK], [ArtNog05JLC]. In addition to axioms and rules of LP and GL, GLA has axioms t:φ→ []φ, ¬t:φ→ []¬t:φ, t:[]φ→ φ, and a rule |-[]φ ⇒ |-φ.

In this paper we establish the completeness of GLA with respect to epistemic semantics. An epistemic model for GLA is a Fitting – Artemov model (cf. Def. 2 of [Art06TCS]) with
- a reverse well-founded transitive frame (W,<)
- an equivalence relation ≡ on W as an evidence accessibility relation such that < ⊆≡
- a possible evidence function ([Art06TCS], [Fit05APAL]) E satisfying the stability property:

E(u, t) = E(v, t) whenever u ≡ v.

Strong provability F is true and provable in Peano Arithmetic is known ([Boo93]) to be propositionally axiomatized by Grzegorczyk's logic Grz, which postulates are classical logic axioms and rules, [](F → G) → ([]F → []G), []F → [][]F, []F → F, []([](F →[]F) → F) →F, and Rule of Necessitation: |-F ⇒ |-[]F. Artemov's Logic of Proofs LP ([Art01BSL]) axiomatizes proof operators t is a proof of F in Peano Arithmetic. The postulates of LP are the ones of the classical propositional logic, t:(F → G) → (s:F → (t⋅s):G), t:F → F, t:F → !t:(t:F), s:F → (s+t):F and t:F → (s+t):F, and the rule of inferring c:A whenever A is an axiom and c is a proof constant.

Joint logics of proofs and provability have been studied in a variety of languages ([Art94APAL], [Nog94TR], [Nog06LC], [Nog07ASL], [TYav01APAL]). In this paper we found the arithmetically complete logic of strong provability and explcit proofs GrzA in the joint language of Grz and LP. GrzA consists of axioms and rules of Grz and LP together with axioms t:P → []P and ¬t:P → []¬t:P. We show that GrzA is complete with respect to the arithmetical provability interpretation, supplied with a corresponding Fitting epistemic semantics and enjoys some sort of a finite model property, which also yields the decidability of GrzA for any given finite specification of constants.

Artemov introduced the Logic of Proofs (LP) as a logic of explicit proofs. We can also offer an epistemic reading of this formula: “t is a possible justification of φ”. Motivated, in part, by this epistemic reading, Fitting introduced a Kripke style semantics for LP in [Fit05APAL]. In this note, we prove soundness and completeness of some axiom systems which are not covered in [Fit05APAL].

Artemov introduced the Logic of Proofs (LP) as a logic of explicit proofs. We can also offer an epistemic reading of this formula: “t is a possible justification of φ”. Motivated, in part, by this epistemic reading, Fitting introduced a Kripke style semantics for LP in [Fit05APAL]. In this note, we prove soundness and completeness of some axiom systems which are not covered in [Fit05APAL].

Two difficult issues for the logic of knowledge have been logical omniscience and common knowledge. Our existing logics of knowledge based on Kripke structures seem to justify logical omniscience, but we know that in real life it does not exist. Also, common knowledge appears to be needed for certain real life procedures to work. But it seems quite implausible that it actually exists in real people.

We suggest two procedure based semantics for knowledge which seem to take care of both these issues in a relatively realistic way.

What this suggests is that if we really want to understand knowledge, then existing customs and plans must play a greater role than we are used to assigning them.

The logic of proofs is an interesting and important logic recently introduced by Artemov [Art02CSLI]. There exist two systems of the logic of proofs: one that cas a classical base Lp, and one that has an intuitionistic base Ilp. From a Gentzen-style point of view, we can formulate two similar sequent calculi for the two systems Lp and Ilp, respectively (see [Art02CSLI]). Although simple and cut-free, these two sequent calculi present several and analogous disadvantages: they do not satisfy the subformula property, their contraction rules are not admissible, and their logical rules fail to be symmetric. Therefore we can claim that at the proof theoretical level both the intuitionistic and the classical logic of proofs need to be improved. In this paper we aim at dealing with this task.

The Logic of Proofs, LP, is an explicit provability logic due to Artemov. The introduction of LP answered a long-standing question concerning the intended semantics of Gödel's provability calculus and provability semantics for intuitionistic logic. The explicit nature of LP and its ability to naturally represent both modal logic and typed λ-calculi, especially in light of the Curry-Howard Isomorphism, makes its applicability to Computer Science a primary focus of research in this area. In the present paper, I develop a tableau system for LP and give a semantic proof of cut elimination.

This paper presents a game semantics for LP, Artemov's Logic of Proofs. The language of LP extends that of propositional logic by adding formula-labeling terms, permitting us to take a term t and an LP formula A and form the new formula t:A. We define a game semantics for this logic that interprets terms as winning strategies on the formulas they label, so t:A may be read as “t is a winning strategy on A.” LP may thus be seen as a logic containing in-language descriptions of winning strategies on its own formulas.

We apply our semantics to show how winnable instances of certain extensive games with perfect information may be embedded into LP. This allows us to use LP to derive a winning strategy on the embedding, from which we can extract a winning strategy on the original, non-embedded game. As a concrete illustration of this method, we compute a winning strategy for a winnable instance of the well-known game Nim.

Fitting has described LP, Artemov's Logic of Proofs, as a logic of explicit knowledge. To say that knowledge is explicit means that something is known for a specific reason, as opposed to the Hintikka notion of knowledge, which is best described as knowability. LP introduces symbols for reasons along with natural operations to combine and manipulate them. What results is a joint calculus of reasons and formulas, achieved by admitting new formulas of the form t:φ, which may be understood as “φ for reason t.”

An evaluation game is a zero-sum game between two players with perfect information. Given a model for a logical theory, the game is played on the parse tree of a formula, but the rules of play are rigged so that the Verifier player has a winning strategy exactly when the formula holds in the model. Interpreting a specific winning strategy for Verifier as a reason why Verifier can always win an evaluation game on an LP formula in some LP model, we study the connection between reasons in logics of explicit knowledge and winning strategies in evaluation games.

This paper introduces a game-theoretic semantics for LP, Artemov's Logic of Proofs, taking the viewpoint that LP is a logic of explicit strategies on propositional verification games. To demonstrate the utility of this viewpoint, we define an embedding of the well-known game of Nim into the propositional verification game, which allows us to extract a winning strategy on a winnable Nim instance by internalizing the proof in LP of the formalized version of that instance.

Keywords: Logic of Proofs, game-theoretic semantics, GTS

Explicit modal logics contain modal-like terms that label formulas in a way that mimics deduction in the system. These logics have certain proof-theoretic advantages over the usual modal logics, perhaps the most important of which is conventional cut-elimination.

The present paper studies tableau proof systems for two explicit modal logics, LP and S4LP. Using a certain method to prove the correctness of these systems, we obtain a semantic proof of cut-elimination for these logics.

This paper introduces a notion of bisimulation for Artemov's logics of evidence-based knowledge. Bisimulation allows us to study the effect of dynamic epistemic operations on language expressivity. It is shown that public announcements, a basic dynamic epistemic operation, add expressivity to the language of evidenced-based knowledge. It is also shown that public announcements are definable in the language of evidence-based knowledge augmented with an evidence admissibility relation.

Justification Logic is the study of a family of logics used to reason about justified true belief. Dynamic Epistemic Logic is the study of a family of logics obtained by adding various kinds of communication to the language of multi-modal logic, yielding languages for reasoning about communication and true belief. This paper is a first-step in merging these two areas, in that it brings the most basic kind of communication studied in Dynamic Epistemic Logic—the public announcement—over to Justification Logic. This gives us a language for reasoning about public announcements and justified true belief.

After giving an overview of Justification Logic, the paper introduces a notion of bisimulation for Justification Logic. Bisimulation allows us to study the affect on language expressivity when we add various kinds of communication to the language. Among a number of expressivity results, we show that adding public announcements to the language of Justification Logic strictly increases language expressivity. This stands in contrast to the Plaza-Gerbrandy Theorem, which states that adding public announcements to multi-modal logic does not increase language expressivity. This leads us to extend the language of Justification Logic in order to provide a Plaza-Gerbrandy analog of multi-modal logic that we can use to reason about justified true belief.

Justification Logic is the study of a family of logics used to reason about justified true belief. Dynamic Epistemic Logic is the study of logics used to reason about communication and true belief. This dissertation is a first step in merging these two areas, in that it defines theories for a joint language in which we may reason about communication alongside justified true belief.

After some preliminary matters, we go through a comprehensive survey of Dynamic Epistemic Logic, which primes us for the work at the end of the text. We then move into the core work of the dissertation, where we introduce a number of extensions of existing languages and theories of Justification Logic. Our extensions are all based on the work of Sergei Artemov, who extended the language of propositional logic by the addition of formula-labeling terms. This extension allows us to take a term t and a formula φ and form the new formula t:φ. The terms have a derivation-compatible structure that allows us to view terms as evidence verifying the truth of the formulas they label, which provides us with a means for reasoning about justified true belief.

We look at extensions of these theories that allow us to reason about evidence admissibility: the new formula t>>φ lets us express that t is admissible as evidence for φ, by which we mean that t may be taken into account when considering the truth of φ, though t need not conclusively validate φ. A further extension adds a unary modal operator [] that we use to reason about alternative evidence possibilities.

Nominaled extensions of the latter languages allow us to express a notion of dynamic evidence introduction, whereby we may introduce a term t as admissible as evidence for φ. These extensions lead us to the final chapter of the text, where we combine our various systems of Justification Logic with the framework of Dynamic Epistemic Logic. Such joint theories contribute to the ongoing work aiming to provide a better foundational account of the reasoning of computational social agents.

This paper presents a logic combining Dynamic Epistemic Logic, a framework for reasoning about multi-agent communication, with a new multi-agent version of Justification Logic, a framework for reasoning about evidence and justification. This novel combination incorporates a new kind of multi-agent evidence elimination that cleanly meshes with the multi-agent communications from Dynamic Epistemic Logic, resulting in a system for reasoning about multi-agent communication and evidence elimination for groups of interacting rational agents.

This paper presents a game semantics for LP, Artemov's Logic of Proofs. The language of LP extends that of propositional logic by adding formula-labeling terms, permitting us to take a term t and an LP formula A and form the new formula t:A. We define a game semantics for this logic that interprets terms as winning strategies on the formulas they label, so t:A may be read as “t is a winning strategy on A.” LP may thus be seen as a logic containing in-language descriptions of winning strategies on its own formulas.

We apply our semantics to show how winnable instances of certain extensive games with perfect information may be embedded into LP. This allows us to use LP to derive a winning strategy on the embedding, from which we can extract a winning strategy on the original, non-embedded game. As a concrete illustration of this method, we compute a winning strategy for a winnable instance of the well-known game Nim.

Keywords: Logic of Proofs, game semantics, Justification Logic

Justification Logic is a framework for reasoning about evidence and justification in multi-agent systems. Most accounts of Justification Logic are essentially static, in that the (justified) beliefs of agents are immutable. In this article, we add public communication, a dynamic operation of belief change studied in the area of Dynamic Epistemic Logic, to the language of Justification Logic. Introducing notions of bisimulation for the languages of Justification Logic with and without public communication, we catalogue the expressive relationships that exist between almost all of the well-known static fragments of Justification Logic and then determine whether the addition of public communication affects the various expressive relationships existing between these fragments.

Keywords: justification logic, bisimulation, public announcements, expressivity

Logics of evidence-based knowledge was proposed by S. Artemov (see [Art04TR]). It is multi-agent logic of knowledge enriched by evidence assertions of the form t:φ where t is an evidence term. Knowledge of every agent is axiomatized by a modal logic L (L is T or S4 or S5), evidence-based knowledge operator is described by the logic of proofs LP (see [Art01BSL]). The resulting systems L_nLP are provided with Kripke-style semantics. The corresponding completeness theorems are proven. For L = T, S4 it is shown that forgetful projection which replace all evidences by a uniform modality J coincides with L_nS4. We introduce the multi-agent logic of evidence-based knowledge S4_nLP(S5) in which the evidence component corresponds to S5-modality. In order to do this we extend the language of S4_nLP by new unary operation of negative checker “?”.

Axioms and rules of S4_nLP(S5) are those of S4_nLP plus a new axiom describing negative checker:

¬[[t]]φ→ [[?t]]¬[[t]]φ.

For this logic we define Kripke-style models and prove the completeness theorem. A model is a structure M = (W,R₁,...,R_n,R,ε,||-) where W ≠∅ is a set of states, R_i, R are reflexive transitive accessibility relations on W. An evidence function ε is a mapping from states and evidence terms to sets of formulas. It is monotonous (uRv implies ε(u, t) ⊆ε(v, t)) and respects operations on evidence terms. ||- is a validity relation between states and sentence variables. The validity of formulas is defined in the usual way with the only new clause: u ||- [[t]]φ iff φ∈ε(u, t). We require that φ∈ε(u, t) implies v ||- φ for all v ∈W with uRv.

Theorem. S4_nLP(S5) |-φ iff φ holds in all S4_nLP(S5)-models.

We introduce a logic of evidence-based knowledge S5_nLP(S5) in which the evidence part is based on logic of proofs with negative checker LP(S5). The later is obtained from the Logic of proofs LP by adding a new unary operation of negative checker `?' and the corresponding axiom. We define Kripke-style models for S5_nLP(S5) and prove the completeness with respect to this semantics. We also define the logic of justified knowledge for S5_nLP(S5).

Keywords: Logic of proofs, logic of evidence-based knowledge, epistemic modal logic S5, logic of proofs with negative checker

We introduce the logic of proofs whose modal counterpart is the modal logic S5. The language of Logic of Proofs LP is extended by a new unary operation of negative checker “?”. We define Kripke-style models for the resulting logic in the style of Fitting models and prove the corresponding Completeness theorem. The main result is the Realization theorem for the modal logic S5.

We introduce a logic of evidence-based knowledge S5_nLP(S5) in which the evidence part is based on Logic of proofs with negative checker LP(S5). The later is obtained from the Logic of proofs LP (S. Artemov, 1995) by adding a new unary operation of negative checker “?” and the corresponding axiom. We define Fitting-Kripke-style models for S5_nLP(S5) and prove the completeness of S5_nLP(S5) with respect to this class of models with various restrictions on accessibility relation for the evidence part. We present the list of axioms for the logic S5_nLP(S5)^C with additional modality for common knowledge and prove that this logic is the conservative extension of S5_nLP(S5).

The substitution operation in logic of proofs is axiomatized. For the system constructed, symbolic semantics is introduced and a completeness theorem is proved.

Keywords: logic of proofs, axiomatics of substitution, symbolic semantic, symbolic model, finitely generated reflexive model, tableau of labels, semantic tableau, internalization

The paper presents a purely relational semantics for the basic justification logic J. Soundness and completeness results are obtained be demonstrating a close connection of the purely relational semantics with Mkrtychev interpretations. We prove that for every Mkrtychev interpretation there is an equivalent purely relational model and vice versa. Then we sketch a dynamic epistemic interpretation of the purely relational semantics. The paper concludes by pointing out the most interesting problems and topics for further study.

Reflexive combinatory logic RCL was introduced by S. Artemov as an extension of typed combinatory logic CL_→ capable to internalize its own derivations of typing judgments. It was designed as a basic theoretical prototype of functional programming languages extended by this kind of self-referential capacity. However, its operational aspects remained to be clarified.

We study reductions for reflexive combinatory logic and prove strong normalization and confluence properties.

We present a natural axiomatization for propositional logic with modal operator for formal provability (Solovay, [Sol76]) and labeled modalities for individual proofs with operations over them (Artemov, [Art95TR]). For this purpose the language is extended by two new operations. The obtained system MLP naturally includes both Solovay's provability logic GL and Artemov's operational modal logic LP. All finite extensions of the basic system MLP₀ are proved to be decidable and arithmetically complete. It is shown that LP realizes all operations over proofs admitting description in the modal propositional language.

Keywords: propositional provability logics, operations over proofs, logics of proofs

We present a natural axiomatization for propositional logic with a modal operator for formal provability (Solovay, [Sol76]) and labeled modalities for individual proofs with operations on them (Artemov, [Art95TR]). For this purpose, the language has to be extended by two new operations. The obtained system MLP naturally includes both Solovay's provability logic GL and Artemov's operational modal logic LP. We prove that the system MLP is decidable and arithmetically complete. We also show that MLP realizes all operations on proofs admitting description in the modal propositional language.

This report describes syntactical models for the Basic Logic of Proofs, which are closely related to canonical models. For each system of this class of logics soundness and completeness are proved. Moreover, some principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.

Propositional Provability Logic was axiomatized by R. M. Solovay in 1976. This modal logic describes the behavior of the arithmetical operator “A is provable”. The aim of these investigations is to provide propositional axiomatizations of the predicates “p is a proof of A”, “p is a proof which contains A” and “p is a program which computes A” using the same semantics.

The presented systems, called the Basic Logic of Proofs, are first proved to be sound and complete with respect to arithmetical interpretations. Decidability is a consequence of a semantical cut elimination theorem. Moreover, appropriate syntactical models for the Basic Logic of Proofs are defined, which are closely related to canonical models. Finally, some general principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.

The Basic Logic of Proofs provides prepositional axiomatizations of the predicate “p is a proof of A” using the same semantics as the Provability Logic GL. In this paper syntactical models for the Basic Logic of Proofs are described, which are closely related to canonical models. For each system of this class of logics soundness and completeness are proved. Moreover, some principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.

Internalization is a key property of justification logics. It states that justfication logics internalize their own notion of proof which is essential for the proof of the realization theorem. The aim of this note is to show how to make use of internalization to track where an agent's knowledge comes from and how to apply this to the problem of data privacy.

Keywords: justification logic, internalization, knowledge tracking, data privacy

Recently, Tsukada et al. propose to use multi-agent epistemic logic for a taxonomy of information-hiding/disclosure properties, in particular properties used in authentication protocols. We follow their proposal and introduce a new multi-agent justification logic for protocol analysis and verification. We show our logic at work analyzing a non-repudiation protocol due to Zhou and Gollmann. Based on this example, we then discuss the expressive power of the logic as well as possible further extensions.

Keywords: protocol verification, justification logic, authentication, non-repudiation

Artemov's Logic of Proof, LP, is an explicit proof counterpart of S4. Their formal connection is built through the realization theorem, that every S4 theorem can be converted to an LP theorem by substituting proof terms for provability modals. Instead of the realization of theorems, what is concerned in this paper is the realization of proofs. We will show that only a subclass of S4 proofs, called non-circular proofs, can be realized as LP proofs in this way. Furthermore, we introduce a numerical version of LP, called S4^Δ, to constructively prove that every S4 theorem has a non-circular proof. These results provide a new algorithmic proof of the realization theorem.

Knowledge's acquisition happens in time. However, this feature is not reflected in the standard epistemic logics, e.g. S4 with its possible world semantics suggested by Hintikka in [1], and hence their applications are limited. In this paper we adapt these normal modal logics to increase their expressive power such that not only is what is known modeled but also when it is known is recorded. We supplement each world with an awareness function which is an augmentation of Fagin-Halpern's to keep track of the time when each formula is to be derived. This provides a new response to the logical omniscience problem. Our work originates from the tradition of study of Justification Logic, also known as Logic of Proofs, LP, introduced by Artemov ([Art08RSL],[Art95TR],[Art01BSL]). We will give the axiom systems of the models built here, accompanied with soundness and completeness results.

It is well known that Modal Epistemic logic (MEL) suffers from the problem of logical omniscience. In this paper, we will argue that in order to solve the problem, the temporal dimension of knowledge has to be revealed and following this analysis, we present a general epistemic framework, timed Modal Epistemic Logic (tMEL), modified from MEL, such that the time at which a formula is known by an agent based on his reasoning procedure is explicitly stated. With the help of the additional temporal devices, we are able to determine what is actually known by the agent within a reasonable time of reasoning. The discussions will focus on tS4, the tMEL counterpart of S4, but the method can be uniformly generalized to the study of other tMEL logics. Both the semantics and axiomatic proof systems will be provided, accompanied by soundness and completeness results, and other technical features of tMEL are also examined. This work originates from the study of Justification Logic, which shapes many aspects of this paper, and is also a direct response to the request to utilize the use of awareness functions such that time can be added to the picture. A generalized awareness function is employed in the semantics to trace when a formula is deduced.

In this paper a complete proper subclass of Hilbert style S4 proofs, called non-circular, will be determined. This study originates from the investigation of formal connection between S4, as Logic of Provability and Logic of Knowledge, and Artemov's Logic of Proof, LP, which later developed into Logic of Justification. One of the main theorems concerning LP is the realization theorem, which states that S4 theorems are precisely the formulas which can be converted to LP theorems with proper justificational objects substituting for modal knowledge operators. We extend the theorem by showing that on the proof level, non-circular proofs are exactly the class of S4 proofs which can be realized to LP proofs. The procedure which leads to the result also provides an alternative algorithm to achieve the realization theorem, and in the course of the discussions, a numerical version of LP, called S4_Δ, is introduced, which is worth studying for its own sake.

The idea of describing the intended Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic by means of the modal logic of classical provability was suggested by Gödel. He introduced the modal logic of provability S4 and defined intuitionistic logic inside S4. However, the problem of finding the provability interpretation for S4 itself was left open. In particular, the studies of the modal logic complete under the straightforward interpretation of the modality [] as the provability formula in arithmetic led to the logic GL (see [Sol76]) incompatible with S4.

The above problems were solved in [Art95TR], where Artemov found the complete axiom system for the logic of proofs LP in the format “t is a proof of F” and showed that LP was sufficient to emulate the whole S4. Proof terms in LP are constructed by three elementary operations on proofs.

Our goal was to develop the joint logic that incorporates both the modality “F is provable” and the proof operator “t is a proof of F”.

We find the natural axiomatization MLP of the minimal complete system that includes both GL and LP. The presence of [] in the language of MLP requires two new elementary operations on proofs. We show that MLP suffices to realize all operations on proofs admitting description in the modal propositional language. We also find the complete answer to the question of what versions of the interpolation property hold in LP.

Propositional logic of proofs was introduced and studed by S. Artemov in [Art95TR]. He incorporated the proof predicate “t is a proof of F” denoted by t : F in the propositional language and found the complete axiom system for the logic of proofs LP. Proofs are represented by proof terms constructed by three elementary operations on proofs that realize application, (positive) proof checking and nondeterministic choice. Artemov proved that LP is sufficient to realize the modality of the whole Gödel's provability logic S4 (see [Goed33]) and thus provided S4 with the intended provability reading.

We describe logic of proofs extended by the additional storage predicate [t]F with the informal reading “t knows about F”. In the intended semantics t is a reference for a text containing the information (knowledge) F. Some of the texts represent proofs. This fact is denoted by t : F. Proofs contain only valid information that is reflected via the reflexivity principle t : F ∧ [t]G → G. The presence of the storage predicate allows us to specify operations on proofs depending on the formula arguments. For example, negative proof checking that verifies whether t is a proof of F and if no then returnes the proof of ¬(t : F) depends on both t and F. In our language we can replace F by the reference for t : F

[a](t : F) ∧ ¬(t : F) → check(a) : (¬t : F).

We present the complete axiom system for the logic of proof and storage predicates LPS. The obtained system is sufficient to realize S4 in such a way that the constructed realization makes sense for the arbitrary proof predicate.

In the paper the joint Logic of Proofs and Provability LPP is presented that incorporates both the modality [] for provability ([Sol76]) and the proof operator [[t]]F representing the proof predicate “t is a proof of F” ([Art95TR]). The obtained system LPP naturally includes both the modal logic of provability GL and Artemov's Logic of Proofs LP. The presence of the modality [] requires two new operations on proofs that together with operations of LP allow to realize all the invariant operations on proofs admitting description in the modal propositional language. Logic LPP is proved to be decidable and complete with the intended provability semantics.

Keywords: provability logic, logic of proofs, operations on proofs

Logic of proofs LP was introduced by S. Artemov in [Art01BSL]. It is formulated in the propositional language extended by atoms of the form [t]F which represent the proof predicate “t is a proof of a formula F”. Proofs are denoted by proof terms constructed by three elementary operations on proofs (namely, application, (positive) proof checking and nondeterministic choice). In [Art01BSL] LP is proved to be complete with respect to the intended semantics.

We extend the language of the logic of proofs by the additional labelling predicate x : F with the informal reading “x is a label for a formula F”. A typical example of a labelling predicate is the relation “x is a code of a finite set of formulas containing F”. Labelling predicate allows to specify operations on proofs depending on the formula argument. For example, we can specify an operation for the proof of disjunction

[t]A ∧ x : B → [disj(t,x)](A ∨ B)

and negative proof checker

¬[t]F ∧ x : F → [check^–(t,x)](¬[t]F).

Different choices of operations on proofs and labels result in different logics. We have proved that for a wide class of operations the corresponding logics are complete with respect to the intended arithmetical semantics. Also, we study some natural examples of such logics.

Logic of proofs LP introduced by S. Artemov in 1995 describes properties of proof predicate `t is a proof of F' in the propositional language extended by atoms of the form [[t]]F. Proof are represented by terms constructed by three elementary recursive operations on proofs. In order to make the language more expressive we introduce the additional storage predicate with the intended interpretation `x is a label for F'. It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments. In this paper we study operations on proofs and labels that can be specified in the extended language. First, we give a formal definition of an operation on proofs and labels. Then, for an arbitrary finite set of operations F the logic LPS(F) is defined. We provide LPS(F) with symbolic semantics and arithmetical semantics. The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.

Logic of proofs LP introduced by S. Artemov in 1995 describes properties of proof predicate “t is a proof of F” in the propositional language extended by atoms of the form [[t]]F. Proof are represented by terms constructed by three elementary recursive operations on proofs.

In order to make the language more expressive we introduce the additional storage predicate with the intended interpretation “x is a label for F”. It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments.

In this paper we study operations on proofs and labels that can be specified in the extended language. First, we give a formal definition of an operation on proofs and labels. Then, for an arbitrary finite set of operations F the logic LPS(F) is defined. We provide LPS(F) with symbolic semantics and arithmetical semantics.

The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.

We develop a framework in which operations on proofs can be specified and studied. Proofs are treated as structures built from atomic proofs and references by means of computable operations.

Our approach extends the ideas of Logic of Proofs (Artemov, 1995, [Art01BSL]) in which the proof predicate `t is a proof of F' is incorporated into the propositional language. We introduce an additional storage predicate `x is a label for F' (Yavorskaya, 2005, [TYav05JLC]).

In this article which is essentially a continuation of Yavorskaya's work, we study a natural example of a logic with operations on proofs and labels. This logic LPS^* is decidable and complete with respect to its intended semantics. LPS^* is capable to internalize its own proofs, and operations of LPS^* suffice to realize all operations specified in the language with proofs and labels.

Keywords: logic of proofs, justification logic, modal logic, provability logic

Logic of proofs LP, introduced by S. Artemov, originally designed for describing properties of formal proofs, now became a basis for the theory of knowledge with justification. So far, in epistemic systems with justification the corresponding “evidence part”, even for multi-agent systems, consisted of a single explicit evidence logic. In this paper we introduce logics describing two interacting explicit evidence systems. We find an appropriate formalization of the intended semantics and prove the completeness of these logics with respect to both symbolic and arithmetical models. Also, we find the forgetful projections for the logics with two proof predicates which are extensions of the bimodal logic S4².

Logic of proofs LP, introduced by S. Artemov, originally designed for describing properties of formal proofs, now became a basis for the theory of knowledge with justification (cf. [Art04TR]). So far, in epistemic systems with justification the corresponding “evidence part”, even for multi-agent systems, consisted of a single explicit evidence logic. In this paper we introduce logics describing two interacting explicit evidence systems. We find an appropriate formalization of the intended semantics and prove the completeness of these logics with respect to both symbolic and arithmetical models. Also, we find the forgetful projections for the two-agent justification logics which are extensions of the bimodal logic S4².

Keywords: justification logic, explicit evidence, logic of proofs, multi-modal logic, epistemic logic

Logic of proofs LP was introduced by S. Artemov in [Art99JANCL], [Art01BSL]. It describes properties of the proof predicate “t is a proof of F” formalized by the formula [[t]]F. Proofs are represented by terms constructed by three elementary recursive operations on proofs. In this paper we extend the language of the logic of proofs by the additional storage predicate x F with the intended interpretation “x is a label for F”. The storage predicate can play the role of syntax encoding, so it is useful for specification of operations on proofs, especially those that require formula arguments. We give a definition of a specification of an operation on proofs and introduce logics that describe such operations. For a large class of operations we prove the completeness of these logics with respect to the intended semantics. We also study the logic describing the operation of substitution.

Keywords: logic of proofs, justification logic, provability logic

In [Art98TRb] S. Artemov introduced the logic of proofs LP describing provability in an arbitrary system. In this paper we present the logic LPM of the standard multiple conclusion proof predicate in Peano Arithmetic with the negative introspection operation. We establish the completeness of LPM with respect to the intended arithmetical semantics. Two useful artificial semantics for LPM were also found. The first one is an extension of the usual boolean truth tables, whereas the second one deals with so-called protocolling extension of a theory. For both cases the completeness theorem has been established. In the last section we consider first order version of the logic LPM. Arithmetical completeness of this logic is established too.

Keywords: logic of proofs, semantics, protocolling extensions of theories

The language qLP of the provability logic with quantifiers on proofs contains propositional letters, proof variables, boolean connectives, quantifiers over the proof variables and binary proof operator x : F (“x is a proof of the formula F”) introduced by S. Artemov in [Art94APAL].

This language naturally extends the language of the logic of proofs considered in [Art94APAL]. The operational properties of provability studied in [Art98TRb] could be expressed in this language by the corresponding quantified sentences:

∀x ∀y ∃z (x : (A → B) → (y : A → z : B)),

∀x ∃y (x : A → y : (x : A)), etc.

Also, this language may be considered as an extension of the propositional modal language, since the modal provability operator []A could be expressed by the formula ∃x (x : A).

An arithmetical interpretation * assigns arithmetical sentences to propositional variables, commutes with boolean connectives and quantifiers and (x : A)^* = Prf(x, ⌈A^*⌉). (We suppose that the set of proof variables coincides with the set of individual variables in arithmetic.)

Given an arithmetical theory T and a class of proof predicates K we define the logic qLP_K(T) as the set of all formulas in the language qLP, which are provable in T under every arithmetical interpretation * based on proof predicates from K.

We present recent results concerning the decidability and arithmetical complexity of the corresponding logics for different T and K. It turned out that for many natural classes K the logic qLP_K(PA) is Π₂⁰-hard. For the case of the Gödel proof predicate decidable fragments were found.

We study here extensions of the Artemov's logic of proofs in the language with quantifiers on proof variables. Since the provability operator []A could be expressed in this language by the formula ∃u[u]A, the corresponding logic naturally extends the well-known modal provability logic GL. Besides, the presence of quantifiers on proofs allows us to study some properties of provability not covered by the propositional logics.

In this paper we study the arithmetical complexity of the provability logic with quantifiers on proofs qLP_K(T) for a given arithmetical theory T and a class K of proof predicates.

In the last section we define Kripke style semantics for the logics corresponding to the standard Gödel proof predicate and its multiple conclusion version.

Keywords: provability logic, first-order logic of proofs

In this paper we consider first order extensions for the modal provability logic GL and the operational logic of proofs LP. It is proved that if consider the case of so-called binding provability operator then a natural first order extension QGL^b of the logic GL turns out to be arithmetically complete. The same holds for the first order logic of proofs QLP^b.

For the first order modal logic of provability QGL^b we also establish completeness with respect to Kripke style semantics.

Keywords: provability logic, logic of proofs, first order extensions, arithmetical completeness, Kripke semantics

We consider a fragment of provability logic with quantifiers on proofs that consists of formulas with no occurrences of quantifiers in the scope of the proof predicate. By definition, a logic qL is the set of formulas that are true in the standard model of arithmetic under every interpretation based on the standard Gödel proof predicate. We describe Kripke-style semantics for the logic qL and prove the corresponding completeness theorem. For the case of injective arithmetical interpretations, the decidability is proved.

Kripke-style semantics is suggested for the provability logic with quantifiers on proofs corresponding to the standard Gödel proof predicate. It is proved that the set of valid formulas is decidable. The arithmetical completeness is still an open issue.

Keywords: provability logic, logic of proofs, Kripke semantics, decidability

Kripke-style semantics is suggested for the provability logic with quantifiers on proofs corresponding to the standard Gödel proof predicate. It is proved that the set of valid formulas is decidable. The arithmetical completeness is still an open issue.

By terms-allowed-in-types capacity, the Logic of Proofs LP includes formulas of the form t : φ(t), which have self-referential meanings. In this paper, “prehistoric phenomena” in a Gentzen-style formulation of modal logic S4 are defined. A special phenomenon, i.e., “left prehistoric loop”, is then shown to be necessary for self-referentiality in S4-LP realization.

By terms-allowed-in-types capacity, the Logic of Proofs LP enjoys a system of advanced combinatory terms, while including types of the form t:φ(t), which have self-referential meanings. This paper suggests a research on possible S4 measures of self-referentiality introduced by this capacity. Specifically, we define “prehistoric phenomena” in G3s, a Gentzen-style formulation of modal logic S4. A special phenomenon, namely, “left prehistoric loop”, is then shown to be necessary for self-referentiality in realizations of S4 theorems in LP.