Sequent Calculi for Orthologic with Strict Implication

Tomoaki Kawano

doi:10.18778/0138-0680.2021.22

Authors

Tomoaki Kawano Tokyo Institute of Technology, School of Computing, Department of Mathematical and Computing Science, 2-12-1 Okayama, Meguro-ku, Tokyo, Japan https://orcid.org/0000-0002-0524-7614

DOI:

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

Keywords:

Quantum logic, sequent calculus, completeness theorem, implication, orthologic

Abstract

In this study, new sequent calculi for a minimal quantum logic (\(\bf MQL\)) are discussed that involve an implication. The sequent calculus \(\bf GO\) for \(\bf MQL\) was established by Nishimura, and it is complete with respect to ortho-models (O-models). As \(\bf GO\) does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) as the expansions of \(\bf GO\). Both \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) are complete with respect to the O-models. In this study, the completeness and decidability theorems for these new systems are proven. Furthermore, some details pertaining to new rules and the strict implication are discussed.

References

J. C. Abbott, Orthoimplication Algebras, Studia Logica, vol. 35(2) (1976), pp. 173–177, DOI: https://doi.org/10.1007/BF02120879
Google Scholar DOI: https://doi.org/10.1007/BF02120879

K. Bednarska, A. Indrzejczak, Hypersequent Calculi for S5 – The Methods of Cut-elimination, Logic and Logical Philosophy, vol. 24(3) (2015), pp. 277–311, DOI: https://doi.org/10.12775/LLP.2015.018
Google Scholar DOI: https://doi.org/10.12775/LLP.2015.018

G. Birkhoff, J. V. Neumann, The Logic of Quantum Mechanics, Annals of Mathematics, vol. 37(4) (1936), pp. 823–843, DOI: https://doi.org/10.2307/1968621
Google Scholar DOI: https://doi.org/10.2307/1968621

I. Chajda, The axioms for implication in orthologic, Czechoslovak Mathematical Journal, vol. 58(1) (2008), pp. 735–744, DOI: https://doi.org/10.1007/s10587-008-0002-2
Google Scholar DOI: https://doi.org/10.1007/s10587-008-0002-2

I. Chajda, J. Cirulis, An Implicational Logic for Orthomodular Lattices, Acta Scientiarum Mathematicarum, vol. 82(34) (2016), pp. 383–394, DOI: https://doi.org/10.14232/actasm-015-813-6
Google Scholar DOI: https://doi.org/10.14232/actasm-015-813-6

I. Chajda, R. Halaš, An Implication in Orthologic, International Journal of Theoretical Physics, vol. 44(7) (2005), pp. 735–744, DOI: https://doi.org/10.1007/s10773-005-7051-1
Google Scholar DOI: https://doi.org/10.1007/s10773-005-7051-1

I. Chajda, R. Halaš, H. Länger, Orthomodular Implication Algebras, International Journal of Theoretical Physics, vol. 40(11) (2001), pp. 1875–1884, DOI: https://doi.org/10.1023/A:1011933018776
Google Scholar DOI: https://doi.org/10.1023/A:1011933018776

I. Chajda, H. Länger, Orthomodular Posets Can Be Organized as Conditionally Residuated Structures, Acta Universitatis Palackianae Olomucensis. Facultas Rerum Naturalium. Mathematica, vol. 53(2) (2014), pp. 29–33, URL: https://kma.upol.cz/data/xinha/ULOZISTE/ActaMath/2014/53-2-02.pdf
Google Scholar

I. Chajda, H. Länger, Orthomodular lattices can be converted into left-residuated l-groupoids, Miskolc Mathematical Notes, vol. 18(2) (2017), pp. 685–689, DOI: https://doi.org/10.18514/mmn.2017.1730
Google Scholar DOI: https://doi.org/10.18514/MMN.2017.1730

I. Chajda, H. Länger, Residuation in orthomodular lattices, Topological Algebra and its Applications, vol. 5(1) (2017), pp. 1–5, DOI: https://doi.org/10.1515/taa-2017-0001
Google Scholar DOI: https://doi.org/10.1515/taa-2017-0001

I. Chajda, H. Länger, How to introduce the connective implication in orthomodular posets, Asian-European Journal of Mathematics, vol. 14(4) (2021), p. 2150066, DOI: https://doi.org/10.1142/S1793557121500662
Google Scholar DOI: https://doi.org/10.1142/S1793557121500662

M. L. D. Chiara, R. Giuntini, Quantum Logics, [in:] D. M. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, Springer Netherlands, Dordrecht (2002), pp. 129–228, DOI: https://doi.org/10.1007/978-94-017-0460-1_2
Google Scholar DOI: https://doi.org/10.1007/978-94-017-0460-1_2

P. D. Finch, Quantum logic as an implication algebra, Bulletin of the Australian Mathematical Society, vol. 2(1) (1970), pp. 101–106, DOI: https://doi.org/10.1017/S0004972700041642
Google Scholar DOI: https://doi.org/10.1017/S0004972700041642

G. M. Hardegree, Material Implication in Orthomodular (and Boolean) Lattices, Notre Dame Journal of Formal Logic, vol. 22(2) (1981), pp. 163–182, DOI: https://doi.org/10.1305/ndjfl/1093883401
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093883401

G. M. Hardegree, Quasi-implication algebras, Part I: Elementary theory, Algebra Universalis, vol. 12(1) (1981), pp. 30––47, DOI: https://doi.org/10.1007/BF02483861
Google Scholar DOI: https://doi.org/10.1007/BF02483861

G. M. Hardegree, Quasi-implication algebras, Part II: Structure theory, Algebra Universalis, vol. 12(1) (1981), pp. 48–65, DOI: https://doi.org/10.1007/BF02483862
Google Scholar DOI: https://doi.org/10.1007/BF02483862

L. Herman, E. L. Marsden, R. Piziak, Implication Connectives in Orthomodular Lattices, Notre Dame Journal of Formal Logic, vol. 16(3) (1975), pp. 305–328, DOI: https://doi.org/10.1305/ndjfl/1093891789
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093891789

A. Indrzejczak, Two Is Enough – Bisequent Calculus for S5, [in:] A. Herzig, A. Popescu (eds.), Frontiers of Combining Systems, Springer International Publishing, Cham (2019), pp. 277–294, DOI: https://doi.org/10.1007/978-3-030-29007-8_16
Google Scholar DOI: https://doi.org/10.1007/978-3-030-29007-8_16

A. Indrzejczak, Sequents and Trees. An Introduction to the Theory and Applications of Propositional Sequent Calculi, Studies in Universal Logic, Birkhäuser, Basel (2021), DOI: https://doi.org/10.1007/978-3-030-57145-0
Google Scholar DOI: https://doi.org/10.1007/978-3-030-57145-0

K. Ishii, R. Kashima, K. Kikuchi, Sequent Calculi for Visser’s Propositional Logics, Notre Dame Journal of Formal Logic, vol. 42(1) (2001), pp. 1–22, DOI: https://doi.org/10.1305/ndjfl/1054301352
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1054301352

G. Kalmbach, Orthomodular Lattices, Academic Press, New York (1983).
Google Scholar

T. Kawano, Advanced Kripke Frame for Quantum Logic, [in:] L. S. Moss, R. de Queiroz, M. Martinez (eds.), Logic, Language, Information, and Computation, Springer Berlin Heidelberg, Berlin, Heidelberg (2018), pp. 237–249, DOI: https://doi.org/10.1007/978-3-662-57669-4_14
Google Scholar DOI: https://doi.org/10.1007/978-3-662-57669-4_14

T. Kawano, Labeled Sequent Calculus for Orthologic, Bulletin of the Section of Logic, vol. 47(4) (2018), pp. 217–232, DOI: https://doi.org/10.18778/0138-0680.47.4.01
Google Scholar DOI: https://doi.org/10.18778/0138-0680.47.4.01

S. Negri, Proof Theory for Modal Logic, Philosophy Compass, vol. 6(8) (2011), pp. 523–538, DOI: https://doi.org/10.1111/j.1747-9991.2011.00418.x
Google Scholar DOI: https://doi.org/10.1111/j.1747-9991.2011.00418.x

H. Nishimura, Sequential method in quantum logic, Journal of Symbolic Logic, vol. 45(2) (1980), pp. 339–352, DOI: https://doi.org/10.2307/2273194
Google Scholar DOI: https://doi.org/10.2307/2273194

H. Nishimura, Proof Theory for Minimal Quantum Logic I, International Journal of Theoretical Physics, vol. 33(1) (1994), pp. 103–113, DOI: https://doi.org/10.1007/BF00671616
Google Scholar DOI: https://doi.org/10.1007/BF00671616

H. Nishimura, Proof Theory for Minimal Quantum Logic II, International Journal of Theoretical Physics, vol. 33(7) (1994), pp. 1427–1443, DOI: https://doi.org/10.1007/BF00670687
Google Scholar DOI: https://doi.org/10.1007/BF00670687

H. Ozawa, H. Odera, S. Chitani, Formal System QL for Quantum Logic, The Japan Association for Logical Philosophy, Logical Philosophy Research, vol. 3 (2003).
Google Scholar

M. Ozawa, Operational Meanings of Orders of Observables Defined through Quantum Set Theories with Different Conditionals, Electronic Proceedings in Theoretical Computer Science, vol. 236 (2017), pp. 127–144, DOI: https://doi.org/10.4204/eptcs.236.9
Google Scholar DOI: https://doi.org/10.4204/EPTCS.236.9

F. Poggiolesi, Gentzen Calculi for Modal Propositional Logic, vol. 32 of Trends in Logic, Springer, Dordrecht (2011).
Google Scholar DOI: https://doi.org/10.1007/978-90-481-9670-8

A. Visser, A Propositional Logic with Explicit Fixed Points, Studia Logica, vol. 40(2) (1981), pp. 155–175, DOI: https://doi.org/10.1007/BF01874706
Google Scholar DOI: https://doi.org/10.1007/BF01874706