Proof Polynomials
Sergei Artemov
City University Graduate Center
New York
(sartemov@gc.cuny.edu)
Prerequisites:
Summary: The "Greats" (Brouwer, Kolmogorov, Goedel) raised in the 1930's a
complex of fundamental questions which we can now characterize as
determining the exact relation between deductions and computations.
One such fundamental relation, stemming from the consistency proofs,
has already become a cornerstone of Computer Science. This is
the Curry-Howard Isomorphism between typed lambda-terms and
intuitionistic deductions.
The Curry-Howard Isomorphism itself does not capture the self-referential
mechanisms available in formal systems and in programming languages.
A discovery of a natural system of self-referential proof terms,
which we call "proof polynomials", was essential in recent solution to
the famous open problem of Goedel (1933) concerning formalization of
provability. Proof polynomials considerably extend the Curry-Howard
Isomorphism and lead to a joint calculus of propositions and proofs
which unifies modal and epistemic logic with combinatory logic and
typed lambda-calculus. We will explain this solution, and why it is
likely to change our conception of the appropriate syntax and semantics
for lambda-calculus based programming languages, automated deduction
and formal verification, reasoning about knowledge, etc.
Course Outline: Lecture 1: Operational reading of logic, the intended Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic. Close relatives: Kleene realizability, typed lambda-calculus. Goedel's approach to BHK problem: provability calculus S4. Goedel's embedding of intuitionistic logic to S4. The problem of the intended provability semantics for S4.
Lecture 2: Normalization of derivations in modal logic.
Lecture 3: Proof polynomials and Logic of Proofs LP. Internalization
property as a generalization of the Curry-Howard isomorphism.
Lecture 4: Realization of S4 in LP. Solution to Goedel's provability
problem. Proof polynomials as Brouwer-Heyting-Kolmogorov proofs.
Lecture 5: Applications: knowledge with justifications and logical
omniscience problem, new foundations of formal verification, reflective lambda-calculus and its potential.
References: K.Goedel, "Eine Interpretation des intuitionistischen
Aussagenkalkuls", Ergebnisse Math. Colloq., Bd. 4 (1933), S. 39-40.
K. Goedel, "Vortrag bei Zilsel" (1938), in S. Feferman, ed. "Kurt
Goedel Collected Works. Volume III", Oxford University Press, 1995
S. Artemov, "Uniform provability realization of intuitionistic logic,
modality and lambda-terms", Electronic Notes on Theoretical Computer
Science v. 23, No. 1, 1999
S. Artemov, "Explicit provability and constructive semantics",
Bulletin of Symbolic Logic, volume 7, No.1, pp. 1-36, 2001
J.Alt and S.Artemov, "Reflective lambda-calculus",
In Springer Lecture Notes in Computer Science; v. 2183,
Proceedings of the Dagstuhl-Seminar on Proof Theory in Computer Science,
2001
Course Notes:
Explicit Provability and Constructive Semantics
Back to course listing.