Harmony and Normalisation in Bilateral Logic

Pedro del Valle-Inclan

doi:10.18778/0138-0680.2023.14

Authors

Pedro del Valle-Inclan Scuola Normale Superiore, Department of Philosophy

DOI:

https://doi.org/10.18778/0138-0680.2023.14

Keywords:

bilateralism, normalisation, harmony

Abstract

In a recent paper del Valle-Inclan and Schlöder argue that bilateral calculi call for their own notion of proof-theoretic harmony, distinct from the usual (or ‘unilateral’) ones. They then put forward a specifically bilateral criterion of harmony, and present a harmonious bilateral calculus for classical logic.

In this paper, I show how del Valle-Inclan and Schlöder’s criterion of harmony suggests a notion of normal form for bilateral systems, and prove normalisation for two (harmonious) bilateral calculi for classical logic, HB₁ and HB₂. The resulting normal derivations have the usual desirable features, like the separation and subformula properties. HB₁-normal form turns out to be strictly stronger that the notion of normal form proposed by Nils Kürbis, and HB₂-normal form is neither stronger nor weaker than a similar proposal by Marcello D’Agostino, Dov Gabbay, and Sanjay Modgyl.

References

M. D’Agostino, D. Gabbay, S. Modgil, Normality, Non-Contamination and Logical Depth in Classical Natural Deduction, Studia Logica, vol. 108(2) (2020), pp. 291–357, DOI: https://doi.org/10.1007/s11225-019-09847-4
Google Scholar DOI: https://doi.org/10.1007/s11225-019-09847-4

P. del Valle-Inclan, J. J. Schlöder, Coordination and Harmony in Bilateral Logic, Mind, (2022), DOI: https://doi.org/10.1093/mind/fzac012
Google Scholar DOI: https://doi.org/10.1093/mind/fzac012

M. Dummett, The Logical Basis of Metaphysics, Harvard University Press (1991).
Google Scholar

F. Ferreira, The Co-Ordination Principles: A Problem for Bilateralism, Mind, vol. 117(468) (2008), pp. 1051–1057, DOI: https://doi.org/10.1093/mind/fzn036
Google Scholar DOI: https://doi.org/10.1093/mind/fzn036

N. Kürbis, Some Comments on Ian Rumfitt’s Bilateralism, Journal of Philosophical Logic, vol. 45(6) (2016), pp. 623–644, DOI: https://doi.org/10.1007/s10992-016-9395-9
Google Scholar DOI: https://doi.org/10.1007/s10992-016-9395-9

N. Kürbis, Normalisation for Bilateral Classical Logic with Some Philosophical Remarks, Journal of Applied Logics, vol. 2(8) (2021), pp. 531–556.
Google Scholar

D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Stockholm, Sweden: Dover Publications (1965).
Google Scholar

A. N. Prior, The Runabout Inference-Ticket, Analysis, vol. 21(2) (1960), p. 38, DOI: https://doi.org/10.1093/analys/21.2.38
Google Scholar DOI: https://doi.org/10.1093/analys/21.2.38

I. Rumfitt, Yes and No, Mind, vol. 109(436) (2000), pp. 781–823, DOI: https://doi.org/10.1093/mind/109.436.781
Google Scholar DOI: https://doi.org/10.1093/mind/109.436.781

F. Steinberger, On the Equivalence Conjecture for Proof-Theoretic Harmony, Notre Dame Journal of Formal Logic, vol. 54(1) (2013), pp. 79–86, DOI: https://doi.org/10.1215/00294527-1731398
Google Scholar DOI: https://doi.org/10.1215/00294527-1731398

N. Tennant, Negation, Absurdity and Contrariety, [in:] D. M. Gabbay, H. Wansing (eds.), What is Negation?, Springer Netherlands, Dordrecht (1999), pp. 199–222, DOI: https://doi.org/10.1007/978-94-015-9309-0_10
Google Scholar DOI: https://doi.org/10.1007/978-94-015-9309-0_10