Proof theory

zbMath0354.02027MaRDI QIDQ5905909

Publication date: 1975

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Proof theory and constructive mathematics (03F99)

Related Items (93)

Proof theory for minimal quantum logic. I ⋮ Discretely ordered modules as a first-order extension of the cutting planes proof system ⋮ Basic logic: reflection, symmetry, visibility ⋮ A normal form theorem for first order formulas and its application to Gaifman's splitting theorem ⋮ Logics without the contraction rule ⋮ Syntactical investigations into $BI$ logic and $BB^ \prime I$ logic ⋮ A finite analog to the Löwenheim-Skolem theorem ⋮ Relevant entailment—semantics and formal systems ⋮ Analytic rules for mereology ⋮ Elementary descent recursion and proof theory ⋮ A cut elimination theorem for stationary logic ⋮ A semantics for $\lambda $Prolog ⋮ Satisfaction relations for proper classes: Applications in logic and set theory ⋮ The role of parameters in bar rule and bar induction ⋮ The calculus of constructions ⋮ Note on a proof of the extended Kirby-Paris theorem on labelled finite trees ⋮ Herbrand style proof procedures for modal logic ⋮ Lower bounds to the size of constant-depth propositional proofs ⋮ Global quantification in Zermelo-Fraenkel set theory ⋮ European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988 ⋮ On the number of steps in proofs ⋮ A note on full intuitionistic linear logic ⋮ A cut-free calculus for second-order Gödel logic ⋮ Representing any-time and program-iteration by infinitary conjunction ⋮ Paraconsistency, paracompleteness, Gentzen systems, and trivalent semantics ⋮ A small reflection principle for bounded arithmetic ⋮ Preservation theorem and relativization theorem for cofinal extensions ⋮ Contribution to the study of the natural number object in elementary topoi ⋮ Kripke completeness of bi-intuitionistic multilattice logic and its connexive variant ⋮ MODEL THEORY AND PROOF THEORY OF THE GLOBAL REFLECTION PRINCIPLE ⋮ Grzegorcyk's hierarchy and IepΣ₁ ⋮ The Π21$\Pi ^1_2$ consequences of a theory ⋮ Unnamed Item ⋮ On the polynomial-space completeness of intuitionistic propositional logic ⋮ On Theses Without Iterated Modalities of Modal Logics Between C1 and S5. Part 1 ⋮ Completeness and cut-elimination theorems for trilattice logics ⋮ Proof-theoretical analysis: Weak systems of functions and classes ⋮ Non-elementary speed-ups in proof length by different variants of classical analytic calculi ⋮ On quasitautologies ⋮ Taking out LK parts from a proof in Peano arithmetic ⋮ A restricted fragment of the Lambek calculus with iteration and intersection operations ⋮ A new reduction sequence for arithmetic ⋮ A constructive investigation of satisfiability ⋮ A binary modal logic for the intersection types of lambda-calculus. ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic ⋮ Invariant computations for analytic projective geometry ⋮ Bounded arithmetic and the polynomial hierarchy ⋮ Well-Partial Orderings and their Maximal Order Types ⋮ Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa ⋮ A note on definable Skolem functions ⋮ Primitive recursive selection functions for existential assertions over abstract algebras ⋮ Syntactical truth predicates for second order arithmetic ⋮ Explicit Provability and Constructive Semantics ⋮ The Skolemization of prenex formulas in intermediate logics ⋮ Modal translations in substructural logics ⋮ Some properties of ordinal diagrams ⋮ 2-sequent calculus: A proof theory of modalities ⋮ Constructive logics. I: A tutorial on proof systems and typed $\lambda$- calculi ⋮ An approach to infinitary temporal proof theory ⋮ Cut-elimination: syntax and semantics ⋮ A complete infinitary logic ⋮ Ambiguous classes in $\mu$-calculi hierarchies ⋮ An elimination theorem of uniqueness conditions in the intuitionistic predicate calculus ⋮ A simple proof of Parsons' theorem ⋮ Hauptsatz for higher-order modal logic ⋮ Consistency statements and iterations of computable functions in $\mathrm{I}\Sigma_1$ and PRA ⋮ Sequent forms of Herbrand theorem and their applications ⋮ A version of the ∑1-reflection principle for CFA provable in PRA ⋮ Integrating classical and intuitionistic type theory ⋮ A cut-free sequential system for the propositional modal logic of finite chains ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ Interpolation theorems for intuitionistic predicate logic ⋮ Completeness of type assignment systems with intersection, union, and type quantifiers ⋮ A constructive semantics for non‐deducibility ⋮ Compact and ϖ-compact formulas in 51-151-151-1 ⋮ Continuous valuation and logic ⋮ Schematic Cut Elimination and the Ordered Pigeonhole Principle ⋮ Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic ⋮ Bounded linear-time temporal logic: a proof-theoretic investigation ⋮ Some pitfalls of LK-to-LJ translations and how to avoid them ⋮ Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle ⋮ On some proof theoretical properties of the modal logic GL ⋮ Well-ordering Principles, ω-models and $$ \varPi_{1}^{1} $$-comprehension ⋮ An effectively given initial semigroup ⋮ On generalized quantifiers in arithmetic ⋮ On the consistency of an impredicative subsystem of Quine's NF ⋮ European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991 ⋮ Full intuitionistic linear logic ⋮ A uniform tableau method for intuitionistic modal logics. I ⋮ Simple consequence relations ⋮ Probabilized Sequent Calculus and Natural Deduction System for Classical Logic ⋮ Equality and lyndon's interpolation theorem

This page was built for publication: Proof theory