According to Brouwer, the truth in intuitionistic logic means provability. On this basis Heyting and Kolmogorov introduced what is now known as Brouwer-Heyting-Kolmogorov (BHK) semantics for intuitionistic logic and is generally recognized as the intended semantics for the latter. Since then, various mathematical models for intuitionistic logic have been found. However, despite many efforts the original BHK semantics of intuitionistic logic as logic of proofs did not have, until recently, an exact mathematical formulation.

Goedel 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, but made an important reduction which later became an integral part of the solution. In 1938 Goedel suggested using the original BHK format of proof-carrying formulas to build a provability model of S4. This Goedel's program was accomplished in a recently found Logic of Proofs (LP) which enjoys a natural provability semantics, is complete, and able to realize the whole of S4.

The Logic of Proofs is becoming a working tool in Computer Science addressing problems which lie outside the scope of the traditional logical machinery. In this talk 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, self-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 of knowledge to distinguish between given facts, like logical axioms on one hand and knowledge which can be only obtained after a long derivation process. The proof carrying formulas of LP naturally make this distinction.

For more information about the Penn Logic and Computation Seminar, please see the seminar web page.