Interpreting classical theories in constructive ones (Q2710607)

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.