Estonian Winter Schools in Computer Science
Eesti arvutiteaduse talvekoolid
Basic knowledge of undergraduate logic.
According to Brouwer, the truth in intuitionistic logic means provability. On this basis Heyting and Kolmogorov introduced an informal Brouwer-Heyting-Kolmogorov (BHK) semantics for intuitionistic logic. The ideas of BHK led to a discovery of computational semantics of intuitionistic logic, in particular, realizability semantics and Curry-Howard isomorphism of natural derivations and typed lambda-terms. However, despite many efforts the original semantics of intuitionistic logic as logic of proofs did not meet, until recently, an exact mathematical formulation.
Gödel in 1933 suggested a mechanism based on modal logic S4 connecting classical provability (represented as S4-modality) to intuitionistic logic. This did not solve the BHK problem, since S4 itself was left without an exact provability model. In 1938 Gödel suggested using the original BHK format of proof carrying formulas to build a provability model of S4. This Gödel's program was accomplished in 1995 when proof polynomials and the Logic of Proofs (LP) were discovered, shown to enjoy a natural provability semantics, and to be able of realizing all S4-modalities by proof polynomials. The Logic of Proofs became both an explicit counterpart of modal logic and a reflexive combinatory logic (reflexive lambda-calculus) thus providing a uniform mathematical model of knowledge and computability.
In this course we will discuss several applications of the Logic of Proofs. In the areas of lambda-calculi and typed theories, LP brings in a much richer system of types capable of iterating the type assignment, in particular, referential types. In the context of typed programming languages LP provides a theory of data types containing programs. In the area of knowledge representation LP allows us to approach classical logical omniscience problem, which addresses a failure of the traditional logic to distinguish between given facts, like logical axioms, and knowledge which can be only obtained after a long derivation process. The proof carrying formulas of LP naturally make this distinction. In foundations of formal verification the LP idea of explicit reflection gives a new mechanism of extending verification system which guarantees its provable stability.
Lectures 1-2: Explicit tradition in logic and its impact to Computer Science. Classical and intuitionistic proof systems. Operational reading of logical connectives. The problem of finding the Brouwer-Heyting-Kolmogorov (BHK) provability semantics for intuitionistic logic. Kripke semantics. Gentzen proof systems for classical and intuitionistic logics. Modal logic: time vs knowledge semantics. Basic modal systems: K,K4,S4,S5,GL. Kripke models for modal logic. Gentzen proof systems for modal logics. Completeness and Normalization Theorems. Gödel's embedding of intuitionistic logic to S4. The problem of the intended provability semantics for S4.
Lectures 3-4: Natural derivations in intuitionistic logic. Transformation of a Gentzen style proof into a Natural Derivation. Transformation of natural deduction trees into Gentzen style derivations. Abstract data types, examples. Simple types as implication only formulas. Set theoretical (functional) semantics of simple types. Simply typed lambda-calculus. Curry-Howard isomorphism of natural derivations and typed lambda-terms. Simply typed combinatory terms calculus a.k.a. the simply typed combinatory logic. Computational and provability meaning of combinators. Emulated lambda-abstraction and beta-reduction in combinatory logic.
Lectures 5-6: Proof Polynomials and proof-carrying formulas. Logic of Proofs, its provability semantics. Internalization Property. Logic of Proofs vs. Combinatory Logic, polymorphism. Logic of Proofs vs modal logic, realization theorem. Solution to Gödel's provability problem, two models of provability. Proof polynomials as BHK proofs. Reflexive combinatory logic, its computational semantics and provability semantics. Areas of applications.
Modified Thursday, Jan 01, 1970 at 2:00 EET+0200 by monika(at)cs.ioc.ee