Proof-theoretical analysis: Weak systems of functions and classes

conservation for arithmetic sentences cut elimination extensional type theory without universes Feferman style theory of functions and classes Heyting arithmetic intuitionistic logic Myhill-Friedman style set theory restricted induction transfinite induction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Review text

For several systems of Myhill-Friedman style set theory and Feferman style theory of functions and classes, analogs of recursive realizability provide conservation results for negative arithmetic formulas over more standard theories based on intuitionistic logic, viz. Heyting arithmetic HA, \(ID^-({\mathcal O})\), \((\Sigma^ 1_ 1-AC)^-\), where superscript minus means restricted induction. The author proves conservation for all arithmetic sentences. He uses cut elimination, modifications of realizability and known conservation results for theories obtained by adding to HA the schema of transfinite induction up to certain ordinals. The theory \(T_ 1\) is a set-theory with an axiom for exponentiation \(a^ b\), \(\Delta_ 0\)-comprehension, strong collection and restricted induction. \(T_ 2\) has the full induction schema, and \(T_ 3\) has also \(\epsilon\)-induction. The systems proved to be conservative over HA are \(T_ 1\), Feferman's \(EM_ 0\upharpoonright +J\) and Martin-Löf style \(ET_ 0\) (extensional type theory without universes). \(T_ 2\) and \(EM_ 0+J\) are conservative over \((\Sigma^ 1_ 1-AC)^-\), and \(T_ 3\) is conservative over \(ID^-({\mathcal O})\). Extensional type theory \(\cup_{n}ET_ n\) with \(\omega\) universes is conservative over \(HA+TI(\Gamma_ 0)\).

Recommendations

Cites work

Cited in

(19)

This page was built for publication: Proof-theoretical analysis: Weak systems of functions and classes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q911585)