Forcing in Proof Theory
From MaRDI portal
Publication:4678943
DOI10.2178/bsl/1102022660zbMath1064.03034OpenAlexW1979476005MaRDI QIDQ4678943
Publication date: 24 May 2005
Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/293f2c5065bfa681a77237a8e6e0ec8083263478
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Proof theory in general (including proof-theoretic semantics) (03F03) Relative consistency and interpretations (03F25)
Related Items
Term extraction and Ramsey's theorem for pairs, Forcing for hat inductive definitions in arithmetic, Finitely axiomatized theories lack self‐comprehension, Forcing revisited, Constructive forcing, CPS translations and witness extraction in Interactive realizability, A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP, Validating Brouwer's continuity principle for numbers using named exceptions, Provably recursive functions of constructive and relatively constructive theories, Partially definable forcing and bounded arithmetic, On the correspondence between arithmetic theories and propositional proof systems – a survey, Prawitz, Proofs, and Meaning, A Kuroda-style \(j\)-translation, Ultrafilters in reverse mathematics
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
- On the scheme of induction for bounded arithmetic formulas
- Set theory. An introduction to independence proofs
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- A Boolean model of ultrafilters
- Algebraic proofs of cut elimination
- Transfer principles in nonstandard intuitionistic arithmetic
- Some points in formal topology.
- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- Some conservation results on weak König's lemma
- Saturated models of universal theories
- A model for intuitionistic non-standard arithmetic
- On the strength of Ramsey's theorem
- Formalizing forcing arguments in subsystems of second-order arithmetic
- Interpreting classical theories in constructive ones
- On the strength of Ramsey's theorem for pairs
- The Baire category theorem in weak subsystems of second-order arithmetic
- La logique des topos
- Forcing in intuitionistic systems without power-set
- The point of pointless topology
- Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik
- Relativizations of the $\mathcal{P} = ?\mathcal{NP}$ Question
- Internal set theory: A new approach to nonstandard analysis
- Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
- Forcing on bounded arithmetic II
- A feasible theory for analysis
- Constructive Sheaf Semantics
- Minimal invariant spaces in formal topology
- Minimal models of Heyting arithmetic
- IKP and friends
- Constructive topology and combinatorics
- A new method for establishing conservativity of classical systems over their intuitionistic version
- Free-variable axiomatic foundations of infinitesimal analysis: A fragment with finitary consistency proof
- An Effective Conservation Result for Nonstandard Arithmetic
- Eliminating definitions and Skolem functions in first-order logic
- Class groups of integral group rings
- Ramsey's theorem and recursion theory
- Intuitionistische Untersuchungen der formalistischen Logik
- The strength of Mac Lane set theory
- Dynamical method in algebra: Effective Nullstellensätze
