Proof-theoretical analysis: Weak systems of functions and classes (Q911585): Difference between revisions

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)\).