The proof theory of Frege structures

Reinhard Kahle

(University of Tuebingen, Germany)

Aczel introduced Frege structures as a semantical concept to define sets by use of a partial truth predicate. Beeson discovered that they can be syntactically defined as a theory of truth over applicative theories.

Applicative theories - the first-order part of Feferman's theories of explicit mathematics - essentially comprise combinatory logic and axiomatically defined natural numbers. They provide a very useful account to theoretical computer science, particularly, they are well-suited for the study of functional programming.

We will discuss Frege structures as an alternative to explicit mathematics to introduce types. We show the expressive power of Frege structures and discuss their position in the landscape of proof theory.
Wednesday 2nd February 2000, 15:00
Board Room
Department of Computer Science