BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Ordinal Strength of Logic-Enriched Type Theories - Adams\, R (Univ
 ersity of London)
DTSTART:20120327T100000Z
DTEND:20120327T103000Z
UID:TALK37189@talks.cam.ac.uk
CONTACT:Mustapha Amrani
DESCRIPTION:Type theories are formal languages that can be read as either 
 a programming language or a system of logic\, via the propositions-as-type
 s or proofs-as-programs paradigm. Their syntax and metatheory is quite dif
 ferent in character to that of "orthodox logics" (the familiar first-order
  logics\, second-order logics\, etc). So far\, it has been difficult to re
 late type theories to the more orthodox systems of first-order logic\, sec
 ond-order logic\, etc. \n\nLogic-enriched type theories (LTTs) may help wi
 th this problem. An LTT is a hybrid system consisting of a type theory (fo
 r defining mathematical objects) and a separate logical component (for rea
 soning about those objects). It is often possible to translate between a t
 ype theory and an orthodox logic using an LTT as an intermediate system\, 
 when finding a direct translation would be very difficult. \n\nIn this tal
 k\, 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 LTT
 s 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 fir
 st-order least fixed point logic\, and NP to second-order existential logi
 c. \n\n
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR