Interpreting classical theories in constructive ones
In this article a general method for interpreting classical theories in constructive ones is introduced, which generalizes the Friedman-Dragalin translation, but allows interpreting as well classical axiom systems for which that translation fails. It was extracted from methods used by \textit{W. Buchholz} [``The \(\Omega_{\mu+1}\)-rule, in: \textit{W. Buchholz, S. Feferman, W. Pohlers} and \textit{W. Sieg}, Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, 188-233 (1981; Zbl 0489.03022)] and by \textit{T. Coquand} and \textit{M. Hofmann} [``A new method for establishing conservativity of classical systems over their intuitionistic version, Math. Struct. Comput. Sci. 9, No.~4, 323-333 (1999; Zbl 0935.03069)]. The basic idea is to formulate a Kripke model of one theory in a second one, which amounts to defining \(p \Vdash \varphi\) for formulas \(\varphi\) of the first theory and nodes \(p\) of the Kripke model as formulas in the second theory. However \(\bot\) is just treated as an arbitrary relation symbol, but with the restriction, that ex falsum quodlibet should hold w.r.t. this translation. Then, usually via an intermediate theory (involving Markov's principle or a classical intensional version of the original classical one) interpretations of classical in intuitionistic theories are introduced. The article gives a series of examples of interpretations of intuitionistic theories into classical ones. The equivalences of the intuitionistic and of the classical theories are always well known, but the proofs are simplified by using the new technique. It is used to establish the following: 1) Classical \(\text{I}\Sigma_n\) (\(n \geq 1\)) is conservative over its intuitionistic counterpart for \(\Pi_2\) formulae; 2) PA is conservative over HA for \(\Pi_2\)-formulae; 3) \(S_2^1\) is conservative over its constructive counterpart for \(\forall \Sigma_1^b\)-formulae; 4) \(S_2\) is conservative over its constructive counterpart for \(\forall \Sigma_1^b\)-formulae; 5) if classical \(\text{KP} \restriction\) (Kripke-Platek set theory with foundation restricted to \(\Sigma_1\)-formulae) proves \(\forall x.\exists y.\varphi(x,y)\) for a \(\Delta_0\) formula \(\varphi\), then its intensional intuitionistic counterpart proves \(\forall x.\exists w. \neg \forall y \in w.\neg \varphi^{\ast N}(x,y)\), where \(\varphi^{\ast N}\) is the result of applying a standard interpretation of extensional in intensional theories and double negation translation to \(\varphi\); 6) the same result as 5), but for the theories KP (as KP but with full foundation), \(\text{KP}\omega\) (KP with natural numbers) and \(\text{KP}\omega \restriction\) holds; 7) classical KPu (KP with natural numbers as urelements) is conservative over its intuitionistic intensional counterpart for arithmetic \(\Pi_2\)-formulae; 8) if \(\Sigma^1_1\text{-AC}_0 + (\Sigma^1_1\)-induction\()\) (\(\Sigma^1_1\)-axiom of choice with \(\Sigma^1_1\)-induction) proves \(\forall X \exists Y.\varphi(X,Y)\) for arithmetic \(\varphi\), then the corresponding intuitionistic theory proves \(\exists W.\forall X.\exists Y \in W. \varphi^N(X,Y)\) for the double negation translation \(\varphi^N\) of \(\varphi\); 9) the same result as 8) but for \(\Sigma^1_1\text{-AC}\) (the same theory as in 8) but with full induction) holds.NEWLINENEWLINENEWLINEThe article is written in a nice, precise style and a pleasure to read.
- A semantic approach to conservativity
- scientific article; zbMATH DE number 6307929
- A new method for establishing conservativity of classical systems over their intuitionistic version
- Provably recursive functions of constructive and relatively constructive theories
- A generalization of a conservativity theorem for classical versus intuitionistic arithmetic
- A new method for establishing conservativity of classical systems over their intuitionistic version
- A proof-theoretic characterization of the primitive recursive set functions
- Functional interpretations of feasibly constructive arithmetic
- scientific article; zbMATH DE number 4039890 (Why is no real title available?)
- The consistency of classical set theory relative to a set theory with intu1tionistic logic
- The model-theoretic ordinal analysis of theories of predicative strength
- The strength of some Martin-Löf type theories
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- The metamathematics of ergodic theory
- Functional interpretation of Aczel's constructive set theory
- Saturated models of universal theories
- A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- A semantic approach to conservativity
- A translation characterizing the constructive content of classical theories
- Functional interpretation and inductive definitions
- scientific article; zbMATH DE number 1303441 (Why is no real title available?)
- The axiom of choice and combinatory logic
- Forcing in Proof Theory
- A new method for establishing conservativity of classical systems over their intuitionistic version
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
- Markov's principle and subsystems of intuitionistic analysis
- Integrating classical and intuitionistic type theory
- The strength of extensionality. II: Weak weak set theories without infinity
- A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).
- On the unprovability of circuit size bounds in intuitionistic \(\mathsf{S}^1_2\)
- Very large set axioms over constructive set theories
- Mathematical method and proof
- Preservation theorems for bounded formulas
- Provably recursive functions of constructive and relatively constructive theories
This page was built for publication: Interpreting classical theories in constructive ones
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2710607)
