Abstract
In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.
The research of the first author has been funded by the National Research Foundation of South Africa, Grant number 81309. The research of the third and fourth author has been funded by the NWO Vidi grant 016.138.314, the NWO Aspasia grant 015.008.054, and a Delft Technology Fellowship awarded in 2013.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Namely, the tame and proper canonicity, cf. Sect. 3.
- 2.
The same methodology can be used also to define Gentzen calculi, as is witnessed by [25] in the setting of strict implication logics.
- 3.
We say that \(g:\mathbb {A}^n\rightarrow \mathbb {A}\) is the right residual of \(f:\mathbb {A}^n\rightarrow \mathbb {A}\) in its i-th coordinate if for any \(a_1, \ldots , a_{n}, b\in \mathbb {A}\), \(f(a_1, \ldots , a_i, \ldots , a_{n})\le b\) iff \(a_i\le g(a_1, \ldots , b, \ldots , a_{n})\). We also say that f is the left residual of g in its j-th coordinate.
- 4.
We say that \(g:\mathbb {A}^n\rightarrow \mathbb {A}\) is the left Galois adjoint of \(f:\mathbb {A}^n\rightarrow \mathbb {A}\) in its i-th coordinate if for any \(a_1, \ldots , a_{n}, b\in \mathbb {A}\), \(f(a_1, \ldots , a_i, \ldots , a_{n})\le b\) iff \(g(a_1, \ldots , b, \ldots , a_{n})\le a_i\). We say that g is the right Galois adjoint of f in its i-th coordinate if for any \(a_1, \ldots , a_{n}, b\in \mathbb {A}\), \(b\le f(a_1, \ldots , a_i, \ldots , a_{n})\) iff \(a_i\le g(a_1, \ldots , b, \ldots , a_{n})\).
- 5.
Although that argument is given in the distributive setting, it can be easily verified that it does not make use of any specific feature of that setting.
- 6.
In other settings, nominals are interpreted as completely join-irreducible elements in \(\mathbb {A}^{\delta }\), while in the constructive setting, the constructive canonical extensions might not be perfect, therefore there might not be enough completely join-irreducible elements, therefore nominals are interpreted as closed elements instead in the constructive setting.
- 7.
Indeed, the U-shaped argument is the algorithmic version of the Sambin–Vaccaro canonicity proof [29]. In [26], this method has been unified with Jónsson’s canonicity proof [24]; in [12], it has been unified with constructive canonicity introduced in Ghilardi and Meloni [22]; in [16], the canonicity via pseudo-correspondence has been presented as an instance of this method.
- 8.
A term \(\varphi \) is positive (negative) in a variable p if in the signed generation tree \(+\varphi \) all p-nodes are signed \(+\) (−). An inequality \(\varphi \le \psi \) is positive (negative) in p if \(\varphi \) is negative (positive) in p and \(\psi \) is positive (negative) in p.
- 9.
The purpose of this restriction is to enforce preservation of non-empty joins by the term function \(\varphi '^{\mathbb {C}}\). The soundness of the rule is founded upon this and approximation of the argument \(\gamma \) as the join of all closed elements below it. In the non-constructive setting of [14] the same strategy is followed, except that the approximation is done by means of completely join-irreducibles. Since this can give rise to empty sets of approximants and hence empty joins, \(+\vee \) is excluded in the analogous approximation rule in [14], as the join does not preserve empty joins coordinate-wise. In the present setting, the set of closed approximants is never empty, and hence this restriction may be dropped. Similar considerations apply to \(-\wedge \).
References
Ambler, S., Kwiatkowska, M., Measor, N.: Duality and the completeness of the modal \(\mu \)-calculus. Theoret. Comput. Sci. 151, 3–27 (1995)
Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Log. (TOCL) 13, 2 (2012)
Bezhanishvili, N., Hodkinson, I.: Sahlqvist theorem for modal fixed point logic. Theoret. Comput. Sci. 424, 1–19 (2012)
Bilkova, M., Majer, O., Pelis, M.: Epistemic logics for sceptical agents. J. Log. Comput. 26, 1815–1841 (2016)
Britz, C.: Correspondence theory in many-valued modal logics. Master’s thesis, University of Johannesburg, South Africa (2016)
Conradie, W., Craig, A.: Canonicity results for mu-calculi: an algorithmic approach. J. Log. Comput. 27, 705–748 (2017)
Conradie, W., Craig, A., Palmigiano, A., Zhao, Z.: Constructive canonicity for lattice-based fixed point logics. 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
Conradie, W., Frittella, S., Palmigiano, A., Piazzai, M., Tzimoulis, A., Wijnberg, N.M.: Towards an epistemic-logical theory of categorization (2017, submitted). https://sites.google.com/site/willemconradie/files/EpLogicalViewCategorization.pdf
Conradie, W., Ghilardi, S., Palmigiano, A.: Unified correspondence. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics, Outstanding Contributions to Logic, vol. 5, pp. 933–975. Springer International Publishing, Cham (2014)
Conradie W., Palmigiano, A.: Constructive canonicity of inductive inequalities (submitted). ArXiv preprint arXiv:1603.08341
Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for distributive modal logic. Ann. Pure Appl. Log. 163, 338–376 (2012)
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 Program. (2016). doi:10.1016/j.jlamp.2016.10.006
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., Robinson, C.: On Sahlqvist theory for hybrid logic. J. Log. Comput. 27, 867–900 (2017)
Dunn, J.M., Gehrke, M., Palmigiano, A.: Canonical extensions and relational completeness of some substructural logics. J. Symb. Log. 70, 713–740 (2005)
Frittella, S., Palmigiano, A., Santocanale, L.: Dual characterizations for finite lattices via correspondence theory for monotone modal logic. J. Log. Comput. 27, 639–678 (2017)
Gavazzo, F.: Investigations into linear logic with fixed-point operators. ILLC MoL thesis (2015)
Gehrke, M., Harding, J.: Bounded lattice expansions. J. Algebra 238, 345–371 (2001)
Ghilardi, S., Meloni, G.: Constructive canonicity in non-classical logics. Ann. Pure Appl. Log. 86, 1–32 (1997)
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
Jónsson, B.: On the canonicity of Sahlqvist identities. Stud. Logica 53, 473–491 (1994)
Ma, M., Zhao, Z.: Unified correspondence and proof theory for strict implication. J. Log. Comput. 27, 921–960 (2017)
Palmigiano, A., Sourabh, S., Zhao, Z.: Jónsson-style canonicity for ALBA-inequalities. J. Log. Comput. 27, 817–865 (2017)
Palmigiano, A., Sourabh, S., Zhao, Z.: Sahlqvist theory for impossible worlds. J. Log. Comput. 27, 775–816 (2017)
Sahlqvist, H.: Completeness and correspondence in the first and second order semantics for modal logic. Stud. Log. Found. Math. 82, 110–143 (1975)
Sambin, G., Vaccaro, V.: A new proof of Sahlqvist’s theorem on modal definability and completeness. J. Symb. Log. 54(3), 992–999 (1989)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Conradie, W., Craig, A., Palmigiano, A., Zhao, Z. (2017). Constructive Canonicity for Lattice-Based Fixed Point Logics. 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_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-55386-2_7
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)