Identity of Proofs Based on Normalization and Generality
From MaRDI portal
Publication:4650310
DOI10.2178/bsl/1067620091zbMath1058.03061arXivmath/0208094OpenAlexW2068169489MaRDI QIDQ4650310
Publication date: 9 February 2005
Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/math/0208094
Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) History of mathematical logic and foundations (03-03) Proof theory in general (including proof-theoretic semantics) (03F03) Foundations, relations to logic and deductive systems (18A15)
Related Items
Generality of proofs and its Brauerian representation, Coherence in SMCCs and equivalences on derivations in IMML with unit, Gödel on deduction, Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, HARMONISING HARMONY, The Deduction Theorem (Before and After Herbrand), An intuitionistic formula hierarchy based on high‐school identities, Classical proof forestry, Proof-theoretic harmony: towards an intensional account, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, The Cantor–Bernstein theorem: how many proofs?, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, On paradoxes in normal form, Prawitz, Proofs, and Meaning, Inferential Semantics, The calculus of natural calculation, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Isomorphic formulae in classical propositional logic, The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Logical constants as punctuation marks
- Interpolants, cut elimination and flow graphs for the propositional calculus
- Weakly distributive categories
- Algebra of proofs
- On the structure of Brauer's centralizer algebras
- The undecidability of \(k\)-provability
- Self-adjunctions and matrices.
- Coherence in substructural categories
- Cut elimination in categories
- Untersuchungen über das logische Schliessen. II
- Bicartesian coherence
- A generalization of the functorial calculus
- Coherence in categories
- On algebras which are connected with the semisimple continuous groups
- λ-definable functionals andβη conversion
- Adjointness in Foundations
- Temperley-Lieb Recoupling Theory and Invariants of 3-Manifolds (AM-134)
- Isomorphic objects in symmetric monoidal closed categories
- Hilbert's Twenty-Fourth Problem
- Functional completeness of cartesian categories
- Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic
- Deductive systems and categories
- Aspects of topoi
