Interpreting classical theories in constructive ones

DOI10.2307/2695075zbMath0981.03061OpenAlexW1975734325MaRDI QIDQ2710607

Jeremy Avigad

Publication date: 11 March 2002

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2695075

zbMATH Keywords

proof theoryKripke-Platek set theoryKripke semanticsbounded arithmeticaxiom of choiceconstructive theoriesclassical theoriesforcing relationdouble-negation interpretationFriedman-Dragalin translation

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Proof theory in general (including proof-theoretic semantics) (03F03) Relative consistency and interpretations (03F25)

Related Items (18)

A semantic approach to conservativity ⋮ Mathematical method and proof ⋮ Preservation theorems for bounded formulas ⋮ A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC ⋮ The strength of extensionality. II: Weak weak set theories without infinity ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ The axiom of choice and combinatory logic ⋮ Unnamed Item ⋮ Provably recursive functions of constructive and relatively constructive theories ⋮ Forcing in Proof Theory ⋮ A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\). ⋮ The metamathematics of ergodic theory ⋮ MARKOV’S PRINCIPLE AND SUBSYSTEMS OF INTUITIONISTIC ANALYSIS ⋮ Functional interpretation and inductive definitions ⋮ Functional interpretation of Aczel's constructive set theory ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ 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

Cites Work

• Unnamed Item
• Functional interpretations of feasibly constructive arithmetic
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• The strength of some Martin-Löf type theories
• A proof-theoretic characterization of the primitive recursive set functions
• The model-theoretic ordinal analysis of theories of predicative strength
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• A new method for establishing conservativity of classical systems over their intuitionistic version

This page was built for publication: Interpreting classical theories in constructive ones