### Ordinal Strength of Logic-Enriched Type Theories

Adams, R *(University of London)*

Tuesday 27 March 2012, 11:00-11:30

Seminar Room 1, Newton Institute

#### 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.

#### Presentation

#### Video

**The video for this talk should appear here if JavaScript is enabled.**

If it doesn't, something may have gone wrong with our embedded player.

We'll get it fixed as soon as possible.

## Comments

Start the discussion!