Abstract

Type theories are formal languages that can be read as either a programming language or a system of logic, via the propositions-as-types or proofs-as-programs paradigm. Their syntax and metatheory is quite different in character to that of “orthodox logics” (the familiar first-order logics, second-order logics, etc). So far, it has been difficult to relate type theories to the more orthodox systems of first-order logic, second-order logic, etc.

Logic-enriched type theories (LTTs) may help with this problem. An LTT is a hybrid system consisting of a type theory (for defining mathematical objects) and a separate logical component (for reasoning about those objects). It is often possible to translate between a type theory and an orthodox logic using an LTT as an intermediate system, when finding a direct translation would be very difficult.

In this talk, I shall summarise the work so far on the proof theory of type theories, including Anton Setzer’s work on ordinal strength. I shall show how LTTs allow results about type theories to be applied to orthodox logics, and vice versa. This will include a recently discovered, elementary proof of the conservativity of ACA0 over PA. I conclude by giving two new results: type-theoretic analogues of the classic results that P corresponds to first-order least fixed point logic, and NP to second-order existential logic.