A BRICS Mini-Course
October 21, 26 and 28, 1999
Lectures by
Tatiana Yavorskaja (Sidon)
Moscow State University
The well-known Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic (BHK) gives the informal definition of intuitionistic truth in terms of provability. It treats the connectives as constructors that provide proofs for compound statements being given proofs of their components. The idea of describing BHK by means of modal logic of classical provability was suggested by Goedel in 1933. He formulated modal logic of informal provability (coinciding with S4) and defined intuitionistic logic inside S4 in the style of BHK semantics. However, the problem of finding the exact provability semantics for S4 itself was left open. In particular, Goedel pointed out that S4 does not agree with the straightforward interpretation of modality as the provability formula in Peano Arithmetic. Further studies of the modal logic complete under this interpretation led to the logic GL (see [5]) incompatible with S4.
In 1938 in one of his lectures (published in 1995) Goedel suggested to use the proof operator ``t is a proof of F'' instead of the provability operator ``F has a proof'' to formalize the intended semantics for intuitionistic logic. The complete axiom system of Logic of Proofs LP formulated in the format ``t is a proof of F'' was found by S. Artemov in [2]. Here t is the proof term constructed from atomic proofs by elementary computable operations corresponding to modus ponens, proof checker and nondeterministic choice. Logic of Proofs is shown to emulate the entire S4 by assigning proof terms to all occurrences of the modality in S4-derivation that converts it to a derivation in LP. This result allows to give the exact provability model for S4 and therefore intuitionistic logic. LP is also proved to be functional complete, that is the basic operations of LP suffice to realize all invariant operations on proofs admitting propositional description in arithmetic.
Logic of proofs may be considered as a generalization of combinatory logic to the extend when it is able to iterate type assignment. Through realization in LP modality and lambda-terms receive a uniform provability semantics.
Provability reading of S4-modality correspond to multi-conclusion proof systems. Logic of proofs for uni-conclusion proof predicates was described in [4].
The joint Logic of Proofs and Provability was that incorporates both formal arithmetical provability (Solovay, [5]) and proof predicate was found in [6]. In turns out that the presence of the modality requires two additional operations on proofs.
Logic of proofs LP can be considered as the explicit variant of modal logic S4. Explicit versions of other modal logics, in particular for S5, were studed by S. Artemov, E. Kazakov, D. Shapiro.
First order extensions of LP that admit quantifiers either on individual variables (S. Artemov, T. Yavorskaya) or on proofs (R. Yavorsky) are proved to be nonaxiomatizable.
2. S. Artemov, Explicit provability: the intended semantics for intuitionistic and modal logic, Tech. Rep. CFIS 98-10, Cornell University (1998).
3. S. Artemov, Uniform provability realization of intuitionistic logic, modality and lambda-terms, Electronic Notes in Theoretical Computer Science 23 (1999).
4. V. N. Krupski, Operational logic of proofs with functionality condition on proof predicate, Lecture notes in computer science 1234 (1997) 167-177.
5. R. M. Solovay, Provability interpretation of modal logic, Israel Journal of Mathematics 25 (1976) 287-304.
6. T. Sidon, Provability logic with operations on proofs, Lecture notes in computer science 1234 (1997) 342-353.
7. G. Boolos, The logic of provability (Cambrige University Press, Cambrige, 1993).