×

zbMATH — the first resource for mathematics

Isomorphic formulae in classical propositional logic. (English) Zbl 1262.03119
Any categorical interpretation of logic determines a notion of isomorphism between two formulae. The paper under review investigates such isomorphisms in classical propositional logic: in that case, following a remark by Joyal [J. Lambek and P. J. Scott, Introduction to higher order categorical logic. Cambridge etc.: Cambridge University Press (1986; Zbl 0596.03002)], if one restricts to Cartesian closed models, isomorphism collapses to logical equivalence and becomes irrelevant.
Therefore, the authors drop the Cartesian closedness condition and turn to categories where morphisms are generated by compositions and monoidal operations from a set of primitive arrows, subject to coherence equations. Syntactic characterizations of pairs of isomorphic formulae are then obtained, in the spirit of coherence results in monoidal categories [G. M. Kelly and S. MacLane, J. Pure Appl. Algebra 1, 97–140 (1971; Zbl 0212.35001)].

MSC:
03F03 Proof theory in general (including proof-theoretic semantics)
03B05 Classical propositional logic
03F07 Structure of proofs
03F52 Proof-theoretic aspects of linear logic and other substructural logics
03G30 Categorical logic, topoi
PDF BibTeX Cite
Full Text: DOI
References:
[1] Anderson, Alonzo Church’s contributions to philosophy and intensional logic, Bull. Symb. Log. 4 pp 129– (1998) · Zbl 0908.03002
[2] V. Balat Uneétude des sommes fortes: isomorphismes et formes normales PhD thesis, Université Paris VII 2002
[3] Burris, Tarski’s high school identities, Am. Math. Mon. 100 pp 231– (1993) · Zbl 0782.08010
[4] Carnap, Meaning and Necessity: A Study in Semantics and Modal Logic (1947) · Zbl 0034.00106
[5] Church, On Carnap’s analysis of statements of assertion and belief, Analysis 10 pp 97– (1950)
[6] Došen, Logic and Scientific Methods. Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995 pp 289– (1997)
[7] Došen, Identity of proofs based on normalization and generality, Bull. Symb. Log. 9 pp 477– (2003) · Zbl 1058.03061
[8] Došen, Models of deduction, Synthese 148 pp 639– (2006) · Zbl 1103.03052
[9] Došen, Isomorphic objects in symmetric monoidal closed categories, Math. Struct. Comput. Sci. 7 pp 639– (1997) · Zbl 0897.18004
[10] Došen, Cartesian isomorphisms are symmetric monoidal: A justification of linear logic, J. Symb. Log. 64 pp 227– (1999) · Zbl 0928.03070
[11] Došen, Generality of proofs and its Brauerian representation, J. Symb. Log. 68 pp 740– (2003) · Zbl 1058.03062
[12] Došen, A Brauerian representation of split preorders, Math. Log. Q. 49 pp 579– (2003) · Zbl 1035.03034
[13] Došen, Proof-Theoretical Coherence, Studies in Logic Vol. 1 (2004)
[14] Došen, Proof-Net Categories (2007)
[15] K. Došen Z. Petrić Syntax for split preorders 2009
[16] Fiore, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Ann. Pure Appl. Log. 141 pp 35– (2006) · Zbl 1099.03011
[17] Kelly, Coherence in closed categories, J. Pure Appl. Algebra 1 (219) pp 97– (1971) · Zbl 0212.35001
[18] Lambek, Category Theory, Homology Theory and their Applications I pp 76– (1969)
[19] Lambek, Introduction to Higher Order Categorical Logic Cambridge Studies in Advanced Mathematics Vol. 7 (1986)
[20] Seely, Categories in Computer Science and Logic pp 371– (1989)
[21] S. V. Soloviev The category of finite sets and cartesian closed categories (in Russian), Zapiski Nauchnykh Seminarov (LOMI) 105 174 194 1981 22
[22] Soloviev, Logic Programming and Automated Reasoning pp 360– (1993)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.