Lattice Logic Properly Displayed | SpringerLink
Skip to main content

Lattice Logic Properly Displayed

  • Conference paper
  • First Online:
Logic, Language, Information, and Computation (WoLLIC 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10388))

  • 551 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 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. 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. 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. 4.

    We overload the symbol \(\mathbb {L}\) and use it both to denote the complete lattice and its underlying poset.

  5. 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. 6.

    The translations of the axioms involving disjunction are perfectly symmetric, and are omitted.

References

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

    Chapter  Google Scholar 

  2. Belnap, N.: Display logic. J. Philos. Logic 11, 375–417 (1982)

    MathSciNet  MATH  Google Scholar 

  3. Belnap, N.: Linear logic displayed. Notre Dame J. Formal Log. 31(1), 14–25 (1990)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  5. Bílková, M., Greco, G., Palmigiano, A., Tzimoulis, A., Wijnberg, N.: The logic of resources and capabilities (submitted). arXiv preprint arXiv:1608.02222

  6. Birkhoff, G.: Lattice Theory, vol. 25. American Mathematical Society, Providence (1967)

    MATH  Google Scholar 

  7. Birkhoff, G., Lipson, J.D.: Heterogeneous algebras. J. Comb. Theory 8(1), 115–133 (1970)

    Article  MathSciNet  MATH  Google Scholar 

  8. Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  9. Agata, C., Revantha, R.: Power and limits of structural display rules. ACM Trans. Comput. Logic (TOCL) 17(3), 17 (2016)

    MathSciNet  Google Scholar 

  10. Conradie, W., Craig, A.: Canonicity results for mu-calculi: an algorithmic approach. J. Logic Comput. (forthcoming). arXiv preprint arXiv:1408.6367

  11. Conradie, W., Craig, A., Palmigiano, A., Zhao, Z.: Constructive canonicity for lattice-based fixed point logics (submitted). arXiv preprint arXiv:1603.06547

  12. Conradie, W., Fomatati, Y., Palmigiano, A., Sourabh, S.: Algorithmic correspondence for intuitionistic modal mu-calculus. Theoret. Comput. Sci. 564, 30–62 (2015)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  15. Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for distributive modal logic. Ann. Pure Appl. Logic 163(3), 338–376 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  16. Conradie, W., Palmigiano, A.: Constructive canonicity of inductive inequalities (submitted). arXiv preprint arXiv:1603.08341

  17. Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for non-distributive logics (submitted). arXiv preprint arXiv:1603.08515

  18. Conradie, W., Palmigiano, A., Sourabh, S.: Algebraic modal correspondence: Sahlqvist and beyond. J. Log. Algebr. Methods Programm. (2016). arXiv preprint arXiv:1606.06881

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

  20. Conradie, W., Palmigiano, A., Zhao, Z.: Sahlqvist via translation (submitted). arXiv preprint arXiv:1603.08220

  21. Conradie, W., Robinson, C.: On Sahlqvist theory for hybrid logic. J. Log. Comput. (2015). doi:10.1093/logcom/exv045

  22. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)

    Book  MATH  Google Scholar 

  23. Došen, K.: Sequent systems and groupoid models i. Stud. Logica 47, 353–389 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  24. Došen, K.: Logical constants as punctuation marks. Notre Dame J. Formal Log. 30(3), 362–381 (1989)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

  31. Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics, vol. 151. Elsevier, Amsterdam (2007)

    MATH  Google Scholar 

  32. Gentzen, G.: The Collected Papers of Gerhard Gentzen/Edited by M.E. Szabo. North-Holland Publishing Company, Amsterdam (1969)

    Google Scholar 

  33. Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1–101 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  34. Greco, G., Liang, F., Moshier, A., Palmigiano, A.: Multi-type display calculus for semi De Morgan logic. In: Proceedings WoLLIC 2017 (forthcoming)

    Google Scholar 

  35. Goldblatt, R.I.: Semantic analysis of orthologic. J. Philos. Log. 3(1–2), 19–35 (1974)

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

  38. Greco, G., Palmigiano, A.: Lattice logic properly displayed. Extended version: arXiv:1612.05930

  39. Greco, G., Palmigiano, A.: Linear logic properly displayed (submitted). arXiv preprint arXiv:1611.04181

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

    Google Scholar 

  41. Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65(3), 154–170 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  42. le Roux, C.: Correspondence theory in many-valued modal logics. Master’s thesis, University of Johannesburg, South Africa (2016)

    Google Scholar 

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

  44. Palmigiano, A., Sourabh, S., Zhao, Z.: Jónsson-style canonicity for ALBA-inequalities. J. Log. Comput. (2015). doi:10.1093/logcom/exv041

  45. Palmigiano, A., Sourabh, S., Zhao, Z.: Sahlqvist theory for impossible worlds. J. Log. Comput. (2016). doi:10.1093/logcom/exw014

  46. Paoli, F.: Substructural Logics: A Primer, vol. 13. Springer, Heidelberg (2013)

    MATH  Google Scholar 

  47. Sambin, G., Battilotti, G., Faggian, C.: Basic logic: reflection, symmetry, visibility. J. Symb. Log. 65(3), 979–1013 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  48. von Plato, J., Negri, S.: Proof systems for lattice logic. Math. Struct. Comput. Sci. 14(4), 507–526 (2014)

    MATH  Google Scholar 

  49. Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (2000)

    Book  MATH  Google Scholar 

  50. Wansing, H.: Displaying Modal Logic. Kluwer, Dordrecht (1998)

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Giuseppe Greco .

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

figure ad
figure ae

B Distributivity Fails

figure af

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

figure ag

There are no rules in which \(\bullet \) and \(\centerdot \) interact, hence we are reduced to either isolate

figure ah

in precedent position by the backward application of a display rule, or isolate the following structure in succedent position:

figure ai

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.

figure aj
figure ak
  • 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

figure al

and by applying Exchange and Weakening, we obtain

figure am

Notice that the second subcase can be reduced to the first one as follows:

figure an

As to the proof of the first subcase, let us preliminarily perform the following steps:

figure ao

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:

    figure ap
  • 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:

    figure aq
    figure ar

Rights and permissions

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

Publish with us

Policies and ethics