COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Ordinal Strength of Logic-Enriched Type Theories

## Ordinal Strength of Logic-Enriched Type TheoriesAdd to your list(s) Download to your calendar using vCal - Adams, R (University of London)
- Tuesday 27 March 2012, 11:00-11:30
- Seminar Room 1, Newton Institute.
If you have a question about this talk, please contact Mustapha Amrani. Semantics and Syntax: A Legacy of Alan Turing 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. This talk is part of the Isaac Newton Institute Seminar Series series. ## This talk is included in these lists:- All CMS events
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
- bld31
Note that ex-directory lists are not shown. |
## Other listsType the title of a new list here Current Issues in Assessment Cambridge-INET Institute, Faculty of Economics## Other talksCommunicating Your Research to the Wider World SciBar: Sleep, Dreams and Consciousness 'Nobody comes with an empty head': enterprise Hindutva and social media in urban India Optimising fresh produce quality monitoring and analysis Satellite Applications Catapult Quickfire Talks Developing a single-cell transcriptomic data analysis pipeline |