Next: About this document
Logic of Proofs and Realizability
Sergei Artemov (Cornell Math Department)
PRL Seminar
Tuesday, April 22, 1997
Logic of Proofs (LP) incorporates proof terms directly into
the propositional language using new atomic formulas
``
'' with the intended reading ``
is a proof of 
''.
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
`` is a proof of '' is interpreted as a corresponding
arithmetical formula about Gödel codes of and .
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 
(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.