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.

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, MeyvdHoe95]) 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.

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 ([Göd33EMC]). 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