Logic Talk
Computer Science Department

Time: 2:30-3:30
Date : Tuesday 10/26/2004
Room: AKW 400

Completeness and Cut-Elimination in the
Intuitionistic Theory of Types.

James Lipton (Wesleyan University)

In 1954 Takeuti conjectured that cut-elimination holds for the simple theory of types. For over a decade it was the leading open problem in proof theory, because the impredicative character of the logic obstructs traditional approaches using induction on formulas.

A semantic proof was given for (different formulations of) classical second and higher-order logic by Takahashi, Tait, and Andrews in the late 1960's and early 70's, and the related proof of strong normalization for system F was given by Girard in 1970. A constructive proof for the second order intuitionistic theory of species was given by Dragalin in the mid-1980's.

We now show cut-elimation holds for the Miller-Church formulation of the intuitionistic theory of types, extending techniques of Takahashi, and Andrews and tableau machinery of Smullyan, Hintikka, Nerode and Shore. The benefit of generalizing Andrews' approach is that one obtains a stronger result: completeness and cut-elimination are shown to follow from Smullyan's so-called abstract consistency properties, and one is able to show how to extend atomic assignments in this impredicative system, to all formulas.

We strengthen the notion of Hintikka sets in a way that defines tableau-provability for our type theory. Since our proof is semantic, it also defines a model theory and yields a completeness theorem. Our work thus supplies the first declarative semantics for the logic underlying the lambda-Prolog programming language.

We will discuss these results and applications to the model theory of Lambda-prolog.

Host: Carsten Schuermann. If you would like to talk to Jim, please let me know.