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 Author 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 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 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 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 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 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 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 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

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 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 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 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 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 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 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 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 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 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 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 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 DOI: https://doi.org/10.1305/ndjfl/1054301352

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

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 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 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 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 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 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 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).

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 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). 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 DOI: https://doi.org/10.1007/BF01874706