consistencyproof theoryPeano arithmeticHeyting algebrasinfinitary logicindependence resultsordinal notationfundamental sequencesordinal diagramsBorel determinacyordinal analysis of subsystems of second-order arithmeticprovably recursive functions of arithmetic
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Recursive ordinals and ordinal notations (03F15) Intuitionistic mathematics (03F55)
Recommendations
Cited in
(only showing first 100 items - show all)- Monotone simulations of non-monotone proofs.
- Well-ordering proofs for Martin-Löf type theory
- Resolution is cut-free
- The machinery of consistency proofs
- The foundation of a generic theorem prover
- Streams and strings in formal proofs.
- Intuitionistic fixed point theories over set theories
- How to assign ordinal numbers to combinatory terms with polymorphic types
- The paradox of the knower revisited
- PROOF-THEORETIC ANALYSIS OF THE QUANTIFIED ARGUMENT CALCULUS
- Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees
- Universal algebra in higher types
- Corrected upper bounds for free-cut elimination
- Infinite versions of some problems from finite complexity theory
- Equivalences for truth predicates
- Logics of intuitionistic Kripke-Platek set theory
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
- Abstract deduction and inferential models for type theory
- On elementary theories of ordinal notation systems based on reflection principles
- Elementary patterns of resemblance
- Cut-elimination and redundancy-elimination by resolution
- Mass problems associated with effectively closed sets
- An extension of the omega-rule
- A sequent calculus for a negative free logic
- Geometric Rules in Infinitary Logic
- Extended normal form theorems for logical proofs from axioms
- On Relating Theories: Proof-Theoretical Reduction
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
- Subsystems of true arithmetic and hierarchies of functions
- Classes and truths in set theory
- Proof theory and mathematical meaning of paraconsistent C-systems
- A generalization of the second incompleteness theorem and some exceptions to it
- The Skolemization of existential quantifiers in intuitionistic logic
- Dependent choice, `quote' and the clock
- Contraction-elimination for implicational logics
- Algorithmic introduction of quantified cuts
- LINEAR TIME IN HYPERSEQUENT FRAMEWORK
- A proof-theoretical investigation of global intuitionistic (fuzzy) logic
- Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\)
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones
- Some results on cut-elimination, provable well-orderings, induction and reflection
- Notation systems for infinitary derivations
- Proof theory of reflection
- scientific article; zbMATH DE number 69315 (Why is no real title available?)
- Effective cut-elimination for a fragment of modal mu-calculus
- A proof-theoretic study of the correspondence of hybrid logic and classical logic
- Generalizing theorems in real closed fields
- Patterns of resemblance of order 2
- Cut-Elimination for SBL
- On Herbrand's theorem
- LK, LJ, dual intuitionistic logic, and quantum logic
- The Hydra battle and Cichon's principle
- A sequent calculus for urn logic
- Describing proofs by short tautologies
- Interpolation in extensions of first-order logic
- On the set-generic multiverse
- Passive induction and a solution to a Paris-Wilkie open question
- Herbrand analyses
- Gentzen's consistency proof without heightlines
- Paraconsistent informational logic
- An ordinal analysis for theories of self-referential truth
- The undecidability of \(k\)-provability
- The contraction rule and decision problems for logics without structural rules
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- Dispensing with the continuum
- Proofs and countermodels in non-classical logics
- Proof theory and ordinal analysis
- Functional interpretations of feasibly constructive arithmetic
- Ackermann's substitution method (remixed)
- A Conservation Result Concerning Bounded Theories and the Collection Axiom
- Sequent-calculi for metainferential logics
- Fixed points in Peano arithmetic with ordinals
- scientific article; zbMATH DE number 4033739 (Why is no real title available?)
- Proof theory. The first step into impredicativity
- Full operational set theory with unbounded existential quantification and power set
- Proof theory for theories of ordinals. I: Recursively Mahlo ordinals
- On the strength of König's duality theorem for infinite bipartite graphs
- Improved witnessing and local improvement principles for second-order bounded arithmetic
- ``Gaisi Takeuti's finitist standpoint and its mathematical embodiment
- On Takeuti's early view of the concept of set
- A simple logical matrix and sequent calculus for Parry's logic of analytic implication
- scientific article; zbMATH DE number 5788436 (Why is no real title available?)
- Dialetheias and numbers distinct from themselves
- TWO-SORTED FREGE ARITHMETIC IS NOT CONSERVATIVE
- , , AND REINHARDT’S PROGRAM
- Normalization Proof for Derivations in PA after P. Cohen
- A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem.
- Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms
- Defeasible inheritance on cyclic networks
- Cut-elimination and proof schemata
- A note on Gentzen's ordinal assignment
- Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
- Sequent calculi for the propositional logic of HYPE
- Hypersequent and display calculi -- a unified perspective
- Axioms and models of linear logic
- Derivatives of normal functions and \(\omega \)-models
- Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
- NONCLASSICAL TRUTH WITH CLASSICAL STRENGTH. A PROOF-THEORETIC ANALYSIS OF COMPOSITIONAL TRUTH OVER HYPE
- Sequent calculi for intuitionistic Gödel-Löb logic
This page was built for publication: Proof theory. 2nd ed
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1086559)
