Proof theory. 2nd ed

Publication date: 1987

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

zbMATH Keywords

consistency Heyting algebras proof theory infinitary logic Peano arithmetic ordinal diagrams independence results ordinal notation fundamental sequences Borel determinacy ordinal analysis of subsystems of second-order arithmetic provably recursive functions of arithmetic

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Recursive ordinals and ordinal notations (03F15) Subsystems of classical logic (including intuitionistic logic) (03B20) Intuitionistic mathematics (03F55)

Related Items

, , AND REINHARDT’S PROGRAM, Dialogues and Proofs; Yankov’s Contribution to Proof Theory, A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH, A Conservation Result Concerning Bounded Theories and the Collection Axiom, Reducibilities Among Decision Problems for HNN Groups, Vector Addition Systems and Subsystems of Peano Arithmetic, Cut-Elimination and Proof Schemata, Herbrand analyses, Program Size Complexity of Correction Grammars in the Ershov Hierarchy, A NOTE ON THE SEQUENT CALCULI, THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY, Lifting proofs from countable to uncountable mathematics, LINEAR TIME IN HYPERSEQUENT FRAMEWORK, NONCLASSICAL TRUTH WITH CLASSICAL STRENGTH. A PROOF-THEORETIC ANALYSIS OF COMPOSITIONAL TRUTH OVER HYPE, The (Greatest) Fragment of Classical Logic that Respects the Variable-Sharing Principle (in the FMLA-FMLA Framework), Normalizing notations in the Ershov hierarchy, Glivenko sequent classes and constructive cut elimination in geometric logics, THE LARGE STRUCTURES OF GROTHENDIECK FOUNDED ON FINITE-ORDER ARITHMETIC, TWO-SORTED FREGE ARITHMETIC IS NOT CONSERVATIVE, The laws of thought and the laws of truth as two sides of one coin, Dialetheias and numbers distinct from themselves, Herbrand complexity and the epsilon calculus with equality, ON ZARDINI’S RULES FOR MULTIPLICATIVE QUANTIFICATION AS THE SOURCE OF CONTRA(DI)CTIONS, Cut Elimination for Extended Sequent Calculi, Notes on models of (partial) Kripke-Feferman truth, Type-theoretic approaches to ordinals, GENERALITY AND EXISTENCE 1: QUANTIFICATION AND FREE LOGIC, More on Systems of Truth and Predicative Comprehension, On the Set-Generic Multiverse, On Relating Theories: Proof-Theoretical Reduction, Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss, Improved witnessing and local improvement principles for second-order bounded arithmetic, Cut-elimination and redundancy-elimination by resolution, Elementary patterns of resemblance, An open formalism against incompleteness, Asymptotic cyclic expansion and bridge groups of formal proofs, A generalization of the second incompleteness theorem and some exceptions to it, Ackermann's substitution method (remixed), The Skolemization of existential quantifiers in intuitionistic logic, A new application for explanation-based generalisation within automated deduction, How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning, A Survey on Ordinal Notations Around the Bachmann–Howard Ordinal, Predicativity and Feferman, On Herbrand's theorem, PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent, Informational logic for automated reasoning, Structural proof theory for first-order weak Kleene logics, Controlling witnesses, … and so on: Schütte on Naming Ordinals, Cut-Elimination for SBL, Normalization Proof for Derivations in PA after P. Cohen, Geometric Rules in Infinitary Logic, THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY, EQUIVALENCES FOR TRUTH PREDICATES, THE PREHISTORY OF THE SUBSYSTEMS OF SECOND-ORDER ARITHMETIC, Monotone simulations of non-monotone proofs., Stratified least fixpoint logic, Proof theory of reflection, On elementary theories of ordinal notation systems based on reflection principles, An extension of the omega-rule, A normal form for logical derivations implying one for arithmetic derivations, Is cut-free logic fit for unrestricted abstraction?, A constructive logic behind the catch and throw mechanism, Dependent choice, `quote' and the clock, A sequent calculus for urn logic, The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Gentzen's consistency proof without heightlines, Sequent calculi for the propositional logic of HYPE, Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \), Generalizing theorems in real closed fields, Understanding uniformity in Feferman's explicit mathematics, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\), Higher-order logic and disquotational truth, Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones, Some remarks on lengths of propositional proofs, Dispensing with the continuum, Derivatives of normal functions and \(\omega \)-models, Infinite versions of some problems from finite complexity theory, Ordinal notation systems corresponding to Friedman's linearized well-partial-orders with gap-condition, The machinery of consistency proofs, Passive induction and a solution to a Paris-Wilkie open question, The problem of \(\Pi_{2}\)-cut-introduction, The paradox of the knower revisited, Interpolation in extensions of first-order logic, Interpolation methods for Dunn logics and their extensions, Algorithmic introduction of quantified cuts, A sequent calculus for a negative free logic, A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem., Proof theory for theories of ordinals. I: Recursively Mahlo ordinals, A proof theory for the logic of provability in true arithmetic, Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms, Defeasible inheritance on cyclic networks, Proof theory and mathematical meaning of paraconsistent C-systems, Sequent calculi for Visser's propositional logics, On the compressibility of finite languages and formal proofs, Axioms and models of linear logic, Classes and truths in set theory, How to assign ordinal numbers to combinatory terms with polymorphic types, Effective cut-elimination for a fragment of modal mu-calculus, Upper bounds on positional Paris-Harrington games, The undecidability of \(k\)-provability, A note on Gentzen's ordinal assignment, The contraction rule and decision problems for logics without structural rules, Logics of intuitionistic Kripke-Platek set theory, Intuitionistic fixed point theories over set theories, Sequent calculi for intuitionistic Gödel-Löb logic, Contraction-elimination for implicational logics, On the strength of König's duality theorem for infinite bipartite graphs, A simple logical matrix and sequent calculus for Parry's logic of analytic implication, Free logics are cut-free, Functional interpretations of feasibly constructive arithmetic, Universal algebra in higher types, Subsystems of true arithmetic and hierarchies of functions, Proofs and countermodels in non-classical logics, Fixed points in Peano arithmetic with ordinals, Hypersequent and display calculi -- a unified perspective, Determinate logic and the axiom of choice, Resolution is cut-free, Herbrand's theorem and term induction, LK, LJ, dual intuitionistic logic, and quantum logic, An ordinal analysis for theories of self-referential truth, Paraconsistent informational logic, On the form of witness terms, A proof-theoretical investigation of global intuitionistic (fuzzy) logic, Corrected upper bounds for free-cut elimination, Proof theory and ordinal analysis, Abstract deduction and inferential models for type theory, Notation systems for infinitary derivations, Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees, Robust multiplicity with (transfinitely) vanishing naiveté, The Hydra battle and Cichon's principle, A proof-theoretic study of the correspondence of hybrid logic and classical logic, Analogy calculus, Patterns of resemblance of order 2, A note on the unprovability of consistency in formal theories of truth, Describing proofs by short tautologies, Proof-theoretic strengths of the well-ordering principles, Full operational set theory with unbounded existential quantification and power set, Patterns of resemblance and Bachmann-Howard fixed points, The foundation of a generic theorem prover, Mass problems associated with effectively closed sets, Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II, Extended normal form theorems for logical proofs from axioms, Well-ordering proofs for Martin-Löf type theory, Some results on cut-elimination, provable well-orderings, induction and reflection, Enhancing induction in a contraction free logic with unrestricted abstraction: from \(\mathbf{Z}\) to \(\mathbf{Z}_2\), Cut normal forms and proof complexity, On Takeuti's early view of the concept of set, ``Gaisi Takeuti's finitist standpoint and its mathematical embodiment, Streams and strings in formal proofs., The finitistic consistency of Heck's predicative Fregean system, Systems of explicit mathematics with non-constructive \(\mu\)-operator. I, Syntactical results on the arithmetical completeness of modal logic, Sequent-calculi for metainferential logics