Abstract
We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination, and for the most comprehensive account of axiomatic extensions and expansions of Lattice Logic in a single overarching framework. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
This research has been funded by the NWO Vidi grant 016.138.314, the NWO Aspasia grant 015.008.054, and a Delft Technology Fellowship awarded to the second author in 2013.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Properly displayable logics (cf. [50]) are those amenable to be presented in the form of a proper display calculus. The notion of properly displayable logic has been characterized in a purely proof-theoretic way in [9]. In [37], an alternative characterization of properly displayable logics has been proposed which builds on the algebraic theory of unified correspondence [10, 12, 14, 15, 18,19,20,21, 30, 42,43,44,45]. The techniques and insights of unified correspondence are also available for lattice-based logics, cf. [11, 13, 16, 17]).
- 2.
A sequent calculus verifies the visibility property if both the auxiliary formulas and the principal formula of each operational rule of the calculus occur in an empty context. Hence, by design, L1 verifies the visibility property.
- 3.
The multiplicative form of the introduction rules is the most important aspect in which L1 departs from the calculus of [47], which adopts the additive formulation for the introduction rules for conjunction and disjunction.
- 4.
We overload the symbol \(\mathbb {L}\) and use it both to denote the complete lattice and its underlying poset.
- 5.
We follow the notational conventions introduced in [36]: Each structural connective in the upper row of the synoptic tables is interpreted as the logical connective in the left (resp. right) slot in the lower row when occurring in precedent (resp. succedent) position.
- 6.
The translations of the axioms involving disjunction are perfectly symmetric, and are omitted.
References
Belnap, N.: A useful four-valued logic. In: Dunn, J.M., Epstein, G. (eds.) Moder Uses of Multiple-Valued Logic, pp. 5–37. D. Reidel Springer Netherlands Edition, Dordrecht (1977)
Belnap, N.: Display logic. J. Philos. Logic 11, 375–417 (1982)
Belnap, N.: Linear logic displayed. Notre Dame J. Formal Log. 31(1), 14–25 (1990)
Belnap, N.: Life in the undistributed middle. In: Došen, K., Schroeder-Heister, P. (eds.) Substructural Logics, pp. 31–41. Oxford University Press, Oxford (1993)
Bílková, M., Greco, G., Palmigiano, A., Tzimoulis, A., Wijnberg, N.: The logic of resources and capabilities (submitted). arXiv preprint arXiv:1608.02222
Birkhoff, G.: Lattice Theory, vol. 25. American Mathematical Society, Providence (1967)
Birkhoff, G., Lipson, J.D.: Heterogeneous algebras. J. Comb. Theory 8(1), 115–133 (1970)
Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Springer, Heidelberg (2006)
Agata, C., Revantha, R.: Power and limits of structural display rules. ACM Trans. Comput. Logic (TOCL) 17(3), 17 (2016)
Conradie, W., Craig, A.: Canonicity results for mu-calculi: an algorithmic approach. J. Logic Comput. (forthcoming). arXiv preprint arXiv:1408.6367
Conradie, W., Craig, A., Palmigiano, A., Zhao, Z.: Constructive canonicity for lattice-based fixed point logics (submitted). arXiv preprint arXiv:1603.06547
Conradie, W., Fomatati, Y., Palmigiano, A., Sourabh, S.: Algorithmic correspondence for intuitionistic modal mu-calculus. Theoret. Comput. Sci. 564, 30–62 (2015)
Conradie, W., Frittella, S., Palmigiano, A., Piazzai, M., Tzimoulis, A., Wijnberg, N.M.: Categories: how i learned to stop worrying and love two sorts. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 145–164. Springer, Heidelberg (2016). doi:10.1007/978-3-662-52921-8_10. arXiv preprint arXiv:1604.00777
Conradie, W., Ghilardi, S., Palmigiano, A.: Unified correspondence. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics. OCL, vol. 5, pp. 933–975. Springer, Cham (2014). doi:10.1007/978-3-319-06025-5_36
Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for distributive modal logic. Ann. Pure Appl. Logic 163(3), 338–376 (2012)
Conradie, W., Palmigiano, A.: Constructive canonicity of inductive inequalities (submitted). arXiv preprint arXiv:1603.08341
Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for non-distributive logics (submitted). arXiv preprint arXiv:1603.08515
Conradie, W., Palmigiano, A., Sourabh, S.: Algebraic modal correspondence: Sahlqvist and beyond. J. Log. Algebr. Methods Programm. (2016). arXiv preprint arXiv:1606.06881
Conradie, W., Palmigiano, A., Sourabh, S., Zhao, Z.: Canonicity and relativized canonicity via pseudo-correspondence: an application of ALBA (submitted). arXiv preprint arXiv:1511.04271
Conradie, W., Palmigiano, A., Zhao, Z.: Sahlqvist via translation (submitted). arXiv preprint arXiv:1603.08220
Conradie, W., Robinson, C.: On Sahlqvist theory for hybrid logic. J. Log. Comput. (2015). doi:10.1093/logcom/exv045
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)
Došen, K.: Sequent systems and groupoid models i. Stud. Logica 47, 353–389 (1988)
Došen, K.: Logical constants as punctuation marks. Notre Dame J. Formal Log. 30(3), 362–381 (1989)
Frittella, S., Greco, G., Kurz, A., Palmigiano, A.: Multi-type display calculus for propositional dynamic logic. J. Log. Comput. 26(6), 2067–2104 (2016). doi:10.1093/logcom/exu064
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimić, V.: Multi-type sequent calculi. In: Indrzejczak, A., Kaczmarek, J., Zawidski, M. (eds.) Proceedings Trends in Logic XIII, vol. 13, pp. 81–93 (2014)
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimić, V.: A proof-theoretic semantic analysis of dynamic epistemic logic. J. Log. Comput. 26(6), 1961–2015 (2016). doi:10.1093/logcom/exu063
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimić, V.: A multi-type display calculus for dynamic epistemic logic. J. Log. Comput. 26(6), 2017–2065 (2016). doi:10.1093/logcom/exu068
Frittella, S., Greco, G., Palmigiano, A., Yang, F.: A multi-type calculus for inquisitive logic. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 215–233. Springer, Heidelberg (2016). doi:10.1007/978-3-662-52921-8_14. arXiv preprint arXiv:1604.00936
Frittella, S., Palmigiano, A., Santocanale, L.: Dual characterizations for finite lattices via correspondence theory for monotone modal logic. J. Log. Comput. (2016). doi:10.1093/logcom/exw011
Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics, vol. 151. Elsevier, Amsterdam (2007)
Gentzen, G.: The Collected Papers of Gerhard Gentzen/Edited by M.E. Szabo. North-Holland Publishing Company, Amsterdam (1969)
Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1–101 (1987)
Greco, G., Liang, F., Moshier, A., Palmigiano, A.: Multi-type display calculus for semi De Morgan logic. In: Proceedings WoLLIC 2017 (forthcoming)
Goldblatt, R.I.: Semantic analysis of orthologic. J. Philos. Log. 3(1–2), 19–35 (1974)
Greco, G., Kurz, A., Palmigiano, A.: Dynamic epistemic logic displayed. In: Grossi, D., Roy, O., Huang, H. (eds.) LORI 2013. LNCS, vol. 8196, pp. 135–148. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40948-6_11
Greco, G., Ma, M., Palmigiano, A., Tzimoulis, A., Zhao, Z.: Unified correspondence as a proof-theoretic tool. J. Log. Comput. (2016). doi:10.1093/logcom/exw022
Greco, G., Palmigiano, A.: Lattice logic properly displayed. Extended version: arXiv:1612.05930
Greco, G., Palmigiano, A.: Linear logic properly displayed (submitted). arXiv preprint arXiv:1611.04181
Huhn, H.P.: \(n\)-distributivity and some questions of the equational theory of lattices. In: Contributions to Universal Algebra, Colloq. Math. Soc. J. Bolyai North-Holland, vol. 17 (1997)
Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65(3), 154–170 (1958)
le Roux, C.: Correspondence theory in many-valued modal logics. Master’s thesis, University of Johannesburg, South Africa (2016)
Ma, M., Zhao, Z.: Unified correspondence and proof theory for strict implication. J. Log. Comput. (2016). doi:10.1093/logcom/exw012. arXiv preprint arXiv:1604.08822
Palmigiano, A., Sourabh, S., Zhao, Z.: Jónsson-style canonicity for ALBA-inequalities. J. Log. Comput. (2015). doi:10.1093/logcom/exv041
Palmigiano, A., Sourabh, S., Zhao, Z.: Sahlqvist theory for impossible worlds. J. Log. Comput. (2016). doi:10.1093/logcom/exw014
Paoli, F.: Substructural Logics: A Primer, vol. 13. Springer, Heidelberg (2013)
Sambin, G., Battilotti, G., Faggian, C.: Basic logic: reflection, symmetry, visibility. J. Symb. Log. 65(3), 979–1013 (2014)
von Plato, J., Negri, S.: Proof systems for lattice logic. Math. Struct. Comput. Sci. 14(4), 507–526 (2014)
Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (2000)
Wansing, H.: Displaying Modal Logic. Kluwer, Dordrecht (1998)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
A Completeness
In the cases of the Identity and Absorption laws a formula occurs in isolation on one side of the turnstile, therefore we need to proceed by cases according to the shape of A (we just show \(A = C \wedge D\) and \(A = \bot \), respectively).
B Distributivity Fails
We will show that all the paths in the backward proof-search of the translation of the distributivity axiom end in deadlocks. First, we apply exhaustively all invertible operational rules (modulo display rules):
There are no rules in which \(\bullet \) and \(\centerdot \) interact, hence we are reduced to either isolate
in precedent position by the backward application of a display rule, or isolate the following structure in succedent position:
We only treat the first case, the second being analogous. Once in isolation, we can act on X only via Exchange, Weakening or Residuation. In each case we reach a dead end:
-
Case 1: (Exchange or) Residuation.
As an intermediate step, we can isolate any of the substructures of X via Residuation, or via Exchange and Residuation, as shown below. In each case we reach a dead end.
-
Case 2: (Exchange or) Weakening.
As an intermediate step, we can try to isolate an immediate substructure of X by applying backward Weakening. By directly applying Weakening, we obtain
and by applying Exchange and Weakening, we obtain
Notice that the second subcase can be reduced to the first one as follows:
As to the proof of the first subcase, let us preliminarily perform the following steps:
Again, we are in a situation in which we can act on Y only via Exchange, Weakening or Residuation, and also in this case any option leads to a dead end. Indeed:
-
Case 2.1: Exchange or Weakening. We can delete one of the immediate substructures of Y via Weakening or, respectively, Exchange and Weakening, obtaining
In each case, we reach a dead end, as shown below:
-
Case 2.2: Residuation. We can isolate any of the substructures of Y via Residuation, or via Exchange and Residuation. In each case we reach a dead end:
Rights and permissions
Copyright information
© 2017 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Greco, G., Palmigiano, A. (2017). Lattice Logic Properly Displayed. In: Kennedy, J., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2017. Lecture Notes in Computer Science(), vol 10388. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55386-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-662-55386-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-55385-5
Online ISBN: 978-3-662-55386-2
eBook Packages: Computer ScienceComputer Science (R0)