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
- 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?)
- 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
- 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
(34)- Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics
- Isomorphic formulae in classical propositional logic
- Gödel on deduction
- The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
- Coherence in SMCCs and equivalences on derivations in IMML with unit
- An intuitionistic formula hierarchy based on high‐school identities
- Prawitz, Proofs, and Meaning
- A more general general proof theory
- A prologue to the theory of deduction
- On sets of premises
- Proof-theoretic harmony: towards an intensional account
- Inferential Semantics
- What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
- Problems of a proof-theoretic characterization of paradoxes
- Intensional harmony as isomorphism
- HARMONISING HARMONY
- Eta-rules in Martin-Löf type theory
- Some general results about proof normalization
- Generality of proofs and its Brauerian representation
- Proof Transformations and Structural Invariance
- Proof Identity for Classical Logic: Generalizing to Normality
- Classical proof forestry
- The calculus of natural calculation
- Comparing sense and denotation in bilateralist proof systems for proofs and refutations
- The Deduction Theorem (Before and After Herbrand)
- Formal ontology and mathematics. A case study on the identity of proofs
- The Cantor-Bernstein theorem: how many proofs?
- Deduction at the crossroads
- A new conjecture about identity of proofs
- Inside classical logic: truth, contradictions, fractionality
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- On paradoxes in normal form
- Canonicity of proofs in constructive modal logic
- On the equivalence of proofs involving identity
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)
