On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 187-237.

Voir la notice de l'article provenant de la source Library of Science

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus 𝚂𝙲2𝙸𝚗𝚝 for the bi-intuitionistic logic 2𝙸𝚗𝚝. A distinctive feature of 𝚂𝙲2𝙸𝚗𝚝 is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of 𝚂𝙲2𝙸𝚗𝚝, in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of 2𝙸𝚗𝚝. By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in 𝚂𝙲2𝙸𝚗𝚝 is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously.
Keywords: bilateralism, bi-intuitionistic logic \(\mathtt{2Int}\), cut-elimination, identity of derivations, synonymy
@article{BSL_2023_52_2_a2,
     author = {Ayhan, Sara and Wansing, Heinrich},
     title = {On {Synonymy} in {Proof-Theoretic} {Semantics:} {The} {Case} of {\(\mathtt{2Int}\)}},
     journal = {Bulletin of the Section of Logic},
     pages = {187--237},
     publisher = {mathdoc},
     volume = {52},
     number = {2},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a2/}
}
TY  - JOUR
AU  - Ayhan, Sara
AU  - Wansing, Heinrich
TI  - On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
JO  - Bulletin of the Section of Logic
PY  - 2023
SP  - 187
EP  - 237
VL  - 52
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a2/
LA  - en
ID  - BSL_2023_52_2_a2
ER  - 
%0 Journal Article
%A Ayhan, Sara
%A Wansing, Heinrich
%T On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\)
%J Bulletin of the Section of Logic
%D 2023
%P 187-237
%V 52
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a2/
%G en
%F BSL_2023_52_2_a2
Ayhan, Sara; Wansing, Heinrich. On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\). Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 187-237. http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a2/

[1] A. Almukdad, D. Nelson, Constructible falsity and inexact predicates, The Journal of Symbolic Logic, vol. 49 (1984), pp. 231–233 | DOI

[2] S. Ayhan, Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations, manuscript in preparation.

[3] S. Ayhan, Uniqueness of Logical Connectives in a Bilateralist Setting, [in:] M. Blicha, I. Sedlár (eds.), The Logica Yearbook 2020, College Publications, London (2021), pp. 1–16.

[4] S. Drobyshevich, A bilateral Hilbert-style investigation of 2-intuitionistic logic, Journal of Logic and Computation, vol. 29(5) (2019), pp. 665–692 | DOI

[5] S. Drobyshevich, S. Odintsov, H. Wansing, Moisil’s modal logic and related systems, [in:] K. Bimbó (ed.), Essays in Honour of Michael Dunn, College Publications, London (2022), pp. 150–177.

[6] R. Goré, Dual Intuitionistic Logic Revisited, [in:] R. Dyckhoff (ed.), Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000, Springer-Verlag, Berlin (2000), pp. 252–267 | DOI

[7] N. Kamide, H. Wansing, Proof theory of Nelson’s paraconsistent logic: A uniform perspective, Theoretical Computer Science, vol. 415 (2012), pp. 1–38 | DOI

[8] N. Kamide, H. Wansing, Proof Theory of N4-related paraconsistent logics, College Publications, London (2015).

[9] T. Kowalski, H. Ono, Analytic cut and interpolation for bi-intuitionistic logic, The Review of Symbolic Logic, vol. 10(2) (2017), pp. 259–283 | DOI

[10] S. Negri, J. von Plato, Structural proof theory, Cambridge University Press, Cambridge/New York (2001) | DOI

[11] L. Postniece, Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic, Ph.D. thesis, The Australian National University, Canberra (2010).

[12] D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm (1965).

[13] C. Rauszer, A formalization of the propositional calculus of H-B logic, Studia Logica, vol. 33(1) (1974), pp. 23–34 | DOI

[14] F. von Kutschera, Ein verallgemeinerter Widerlegungsbegriff für Gentzenkalküle, Archiv für mathematische Logik und Grundlagenforschung, vol. 12 (1969), pp. 104–118 | DOI

[15] H. Wansing, Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450 | DOI

[16] H. Wansing, On Split Negation, Strong Negation, Information, Falsification, and Verification, [in:] K. Bimbó (ed.), J. Michael Dunn on Information Based Logics. Outstanding Contributions to Logic, vol. 8, Springer (2016), pp. 161–189 | DOI

[17] H. Wansing, A more general general proof theory, Journal of Applied Logic, vol. 25 (2017), pp. 23–46 | DOI

[18] H. Wansing, A note on synonymy in proof-theoretic semantics, [in:] T. Piecha, K. Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics. Outstanding Contributions to Logic, Springer (forthcoming).

[19] H. Wansing, S. Ayhan, Logical multilateralism (2023), submitted.