BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Ordinal Strength of Logic-Enriched Type Theories -
Adams\, R (University of London)
DTSTART;TZID=Europe/London:20120327T110000
DTEND;TZID=Europe/London:20120327T113000
UID:TALK37189AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/37189
DESCRIPTION:Type theories are formal languages that can be rea
d 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 difficu
lt to relate type theories to the more orthodox sy
stems of first-order logic\, second-order logic\,
etc. \n\nLogic-enriched type theories (LTTs) may h
elp with this problem. An LTT is a hybrid system c
onsisting of a type theory (for defining mathemati
cal objects) and a separate logical component (for
reasoning about those objects). It is often possi
ble to translate between a type theory and an orth
odox logic using an LTT as an intermediate system\
, when finding a direct translation would be very
difficult. \n\nIn this talk\, I shall summarise th
e work so far on the proof theory of type theories
\, including Anton Setzer's work on ordinal streng
th. I shall show how LTTs allow results about type
theories to be applied to orthodox logics\, and v
ice versa. This will include a recently discovered
\, elementary proof of the conservativity of ACA0
over PA. I conclude by giving two new results: typ
e-theoretic analogues of the classic results that
P corresponds to first-order least fixed point log
ic\, and NP to second-order existential logic. \n\
n
LOCATION:Seminar Room 1\, Newton Institute
CONTACT:Mustapha Amrani
END:VEVENT
END:VCALENDAR