Identity of Proofs Based on Normalization and Generality
From MaRDI portal
Abstract: In general proof theory there are two approaches to the question of identity criteria for proofs. The first approach, which stems from Prawitz, Kreisel and Lambek, and is based on normalization of proofs, gives good results in intuitionistic, but not in classical logic. The second approach, which stems from Lambek, Mac Lane and Kelly, and is inspired by the generality of proofs, seems to be more promissing in classical logic.
Recommendations
Cites work
- A generalization of the functorial calculus
- Adjointness in Foundations
- Algebra of proofs
- Aspects of topoi
- Bicartesian coherence
- Coherence in categories
- Coherence in substructural categories
- Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic
- Cut elimination in categories
- Deductive systems and categories
- Functional completeness of cartesian categories
- Hilbert's Twenty-Fourth Problem
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1028236 (Why is no real title available?)
- scientific article; zbMATH DE number 1092415 (Why is no real title available?)
- scientific article; zbMATH DE number 3348059 (Why is no real title available?)
- Interpolants, cut elimination and flow graphs for the propositional calculus
- Isomorphic objects in symmetric monoidal closed categories
- Logical constants as punctuation marks
- On algebras which are connected with the semisimple continuous groups
- On the structure of Brauer's centralizer algebras
- Self-adjunctions and matrices.
- Temperley-Lieb Recoupling Theory and Invariants of 3-Manifolds (AM-134)
- The maximality of Cartesian categories
- The undecidability of k-provability
- Untersuchungen über das logische Schliessen. II
- Weakly distributive categories
- λ-definable functionals andβη conversion
Cited in
(36)- On the equivalence of proofs involving identity
- A more general general proof theory
- Some general results about proof normalization
- What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
- The calculus of natural calculation
- The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
- On paradoxes in normal form
- Coherence in SMCCs and equivalences on derivations in IMML with unit
- Gödel on deduction
- Proof-theoretic harmony: towards an intensional account
- Isomorphic formulae in classical propositional logic
- Generality of proofs and its Brauerian representation
- HARMONISING HARMONY
- A prologue to the theory of deduction
- Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics
- Conceptions of Proof from Aristotle to Gentzen’s Calculi
- Proof normalisation in a logic identifying isomorphic propositions
- An intuitionistic formula hierarchy based on high‐school identities
- The Cantor-Bernstein theorem: how many proofs?
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Prawitz, Proofs, and Meaning
- Inferential Semantics
- On sets of premises
- Eta-rules in Martin-Löf type theory
- Proof Transformations and Structural Invariance
- Proof Identity for Classical Logic: Generalizing to Normality
- The Deduction Theorem (Before and After Herbrand)
- Classical proof forestry
- Canonicity of proofs in constructive modal logic
- Intensional harmony as isomorphism
- Formal ontology and mathematics. A case study on the identity of proofs
- Comparing sense and denotation in bilateralist proof systems for proofs and refutations
- Deduction at the crossroads
- A new conjecture about identity of proofs
- Problems of a proof-theoretic characterization of paradoxes
- Inside classical logic: truth, contradictions, fractionality
This page was built for publication: Identity of Proofs Based on Normalization and Generality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4650310)
