Gödel's papers of 1933 and 1938 left open two problems concerning
- a semantics of proofs for the modal logic S4 and thus for the intuitionistic logic;
- the modal logic of the standard provability predicate Provable(x).
Problem (b) was solved in 1976 by Solovay who established the arithmetical
completeness of the Gödel-Löb modal logic GL with respect to the
provability semantics of □F.
Problem (a) found its solution in
1995 via the Logic of Proofs LP. These two models of provability
complement each other targeting their own areas of application.
S4/LP captures Brouwer-Heyting-Kolmogorov semantics for intuitionistic
logic, epistemic logic with justifications, typed lambda-calculus, modal
lambda-calculus. GL expresses the Second Incompleteness Theorem, Löb
Theorem and other profound provability principles. In this talk we
will discuss recent developments and open problems in this area.
|