scientific article

Publication date: 5 June 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

proof theory realizability Heyting algebra intuitionistic logic intuitionistic analysis intuitionistic arithmetic cut-elimination theorem algebraic models completeness theorems intuitionistic simple theory of types purely syntactical methods

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55) Proof theory and constructive mathematics (03Fxx) Proof theory and constructive mathematics (03F99)

Related Items (50)

A Note on Disjunction and Existence Properties in Predicate Extensions of Intuitionistic Logic—An Application of Jankov Formulas to Predicate Logics ⋮ Multiple Conclusion Linear Logic: Cut Elimination and More ⋮ Rudimentary Kripke models for the intuitionistic propositional calculus ⋮ Some weak fragments of HA and certain closure properties ⋮ Intersection types for explicit substitutions ⋮ Semantics for intuitionistic epistemic logics of shallow depths for game theory ⋮ The Došen square under construction: a tale of four modalities ⋮ Algebraic proofs of cut elimination ⋮ Conservativeness and Eliminability for Anti-Realistic Definitions ⋮ Image of Soviet and Russian logic in the West. Latter Half of the XXth Century ⋮ Simplifying proofs in Fitch-style natural deduction systems ⋮ A NOTE ON THE SEQUENT CALCULI ⋮ Three roads to complete lattices: orders, compatibility, polarity ⋮ QUANTIFIED MODAL LOGIC ON THE RATIONAL LINE ⋮ Interpolation in extensions of first-order logic ⋮ A simple sequent calculus for Angell's logic of analytic containment ⋮ Correspondence theory for modal Fairtlough-Mendler semantics of intuitionistic modal logic ⋮ Lewis meets Brouwer: constructive strict implication ⋮ A Lindström theorem for intuitionistic first-order logic ⋮ Contraction-free sequent calculi for intuitionistic logic ⋮ Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory ⋮ Natural deduction for bi-intuitionistic logic ⋮ Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic ⋮ B-frame duality ⋮ Cover systems for the modalities of linear logic ⋮ A Brauer's theorem and related results ⋮ Kripke sheaf completeness of some superintuitionistic predicate logics with a weakened constant domains principle ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ A semantic hierarchy for intuitionistic logic ⋮ Free choice sequences: a temporal interpretation compatible with acceptance of classical mathematics ⋮ A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic ⋮ Subtractive logic ⋮ Forcing in Proof Theory ⋮ In Memoriam: Albert G. Dragalin 1941–1998 ⋮ The creating subject, the Brouwer-Kripke schema, and infinite proofs ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ The metamathematics of ergodic theory ⋮ Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics ⋮ On Algebraisation of Superintuitionistic Predicate Logics ⋮ PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS ⋮ Absorbing the structural rules in the sequent calculus with additional atomic rules ⋮ Cut-free Gentzen calculus for multimodal CK ⋮ Irreflexive modality in the intuitionistic propositional logic and Novikov completeness ⋮ Markov's constructive analysis; a participant's view ⋮ Heyting-valued interpretations for constructive set theory ⋮ Structural cut elimination. I: Intuitionistic and classical logic ⋮ Saturated models of universal theories ⋮ A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.

This page was built for publication: