Seminar Room Goedel, Favoritenstrasse 9, ground floor, courtyard

Theories of truth over a combinatory algebra have high expressive strength in spite of the simplicity of their axioms. They allow straightforward interpretations of theories of arithmetic and fixed point theories. In this talk, the truth predicate will be used to obtain a natural implicit characterisation of polynomial time.

A theory T_PT of truth over combinatory logic of polynomial strength will be introduced in detail. T_PT has a flexible truth-induction axiom which yields polynomial strength without assuming polynomially growing functions. We describe the proof-theoretic techniques necessary to treat T_PT, and show that T_PT suggests the design of new safe/normal function algebras for polynomial time.