PRL Seminars

Logic of Proofs (LP) incorporates proof terms directly into the propositional language using new atomic formulas "t:F" with the intended reading "t is a proof of F." Three basic operations on proofs are postulated: "application," "proof checker" (they appeared in the Gödel Second Incompleteness theorem), and "choice." The language of LP admits a natural semantics, where "t is a proof of F" is interpreted as a corresponding arithmetical formula about Gödel codes of t and F. A compact complete axiom system for LP has been found. Logic of Proofs provides a basic framework for a formalization of reasonings about proofs and it answers some "old" questions in logic. In particular, LP gives an intended semantics for the Gödel provability logic S4(open since 1933).

In this talk we demonstrate how to build realizations of the intuitionistic logic and lambda calculus in LP. Unlike Kleene recursive realizability, proof realizability provides a fair semantics for the intuitionistic logic.