Abstract
This survey discusses the interplay among unquantified relational logics, propositional modal logics, and set theories. To set up a common ground, cross-translation methods among languages commonly used to work with relations, modalities, and sets, are revisited. This paper also reports on many experiments aimed at providing automated support for reasoning based on the calculus of dyadic relations.
The authors are members of the INdAM Research group GNCS. This research has been partially supported by INdAM-GNCS grants, and by the projects YASMIN (R.d.B.–UniPG2016–17) and FRA-UniTS (2014 and 2016).
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.
We are referring to the action COST n.274 (2002–2005), whose acronym stands for ‘Theory and Applications of Relational Structures as Knowledge Instruments’.
- 2.
Equipollence in means of expression is being referred to, here and throughout. Equipollence in means of proof requires in fact the associative law for \(\varvec{;}\,\), which, as Tarski showed, is not provable in first-order logic restricted to three variables—four variables are required. Equipollence of both kinds is achieved when conjugated quasi-projections (as discussed in the ongoing) are available.
- 3.
In what follows, we will denote these three conditions, separately, by \(\mathbf{(Pair)}_{1}\), \(\mathbf{(Pair)}_{2}\), and \(\mathbf{(Pair)}_{3}\), respectively.
- 4.
We remark that symbols such as \(\in \) and \(\subseteq \) should not be confused with the corresponding set-theoretic symbols used at the meta-level.
- 5.
That is, atomic elements of some unspecified sort.
- 6.
We thank the anonymous referee for suggesting the question of generalizing the first example to Sahlqvist formulae.
- 7.
Our rationale for keeping the predicate \(\mathsf {in}\) distinct from membership is that we must avoid constraining the primitive \(\in \) too much in the present context—e.g., as already noticed, an extensional \(\in \) would not do to our case.
- 8.
For 19 alternative versions of this axiom, (cf. Paulson and Grąbczewski 1996), p.309.
- 9.
Notice that when c belongs to \(a_{\ell }\) (\(\ell =0,1\)), then \(c\subsetneq a_{1-\ell }\); hence there is a \(c'\) in \(a_{1-\ell }\setminus c\), so that c belongs to \(c'\). Then \(c'\subsetneq a_{\ell }\), and so on. Starting w.l.o.g. with \(c_0\) in \(a_0\), one finds distinct sets \(c_0,c_1,c_2,\ldots \) with \(c_{\ell +2\cdot i}\) in \(a_\ell \) for \(\ell =0,1\) and \(i=0,1,2,\ldots \,.\).
- 10.
The interested reader can find all sources and output files of the Otter theorem prover in http://www.dmi.unipg.it/formis/tarski. (The theorem prover Prover9 (McCune 2010) can be used as well).
- 11.
As a matter of fact, (R) will play no role in this task; nor will, for the limited goal of proving \(\mathsf{Func}\mathsf{(}{\varvec{\pi }_{0}}\mathsf{)}\) and \(\mathsf{Func}\mathsf{(}{\varvec{\pi }_{1}}\mathsf{)}\), any of the proper axioms.
- 12.
In the special case when \(Q\mathbf{=}{{\varnothing }}\), Lemma 6.1 boils down to the relatively intuitive fact that \(\mathsf{Func}\mathsf{(}{R^\mathbf{-1}}\mathsf{)}\) holds for any \(R^\mathbf{-1}\) which is the functional part of some relation.
- 13.
An anonymous referee of this paper pointed out that also the stronger implication
$$S\,\varvec{;}\,\texttt {1}\!\!\texttt {l}\mathbf{=}\texttt {1}\!\!\texttt {l}\wedge S\,\varvec{;}\,E \varvec{\subseteq }P\wedge N\,\varvec{;}\,E^\mathbf{-1}\mathbf{=}\texttt {1}\!\!\texttt {l}\rightarrow P \,\varvec{;}\,N^\mathbf{-1}\mathbf{=}\texttt {1}\!\!\texttt {l}$$(obtained by deleting “\(\texttt {1}\!\!\texttt {l}\,\varvec{;}\,N\varvec{\cup }\)”) can be established outright.
References
Aczel, P. (1988). Non-well-founded Sets. CSLI Lecture Notes.
Bresolin, D., Golińska-Pilarek, J., & Orłowska, E. (2006). A relational dual tableaux for interval temporal logics. Journal of Applied Non-classical Logics, 16(3–4), 251–278.
Brink, C., Kahl, W., & Schmidt, G. (Eds.). (1997). Relational Methods in Computer Science. Advances in Computing Science. New York: Springer.
Burrieza, A., Mora, A., Ojeda-Aciego, M., & Orłowska, E. (2009). An implementation of a dual tableaux system for order-of-magnitude qualitative reasoning. International Journal of Computer Mathematics, 86(10–11), 1852–1866.
Caianiello, P., Costantini, S., & Omodeo, E. G. (2003). An environment for specifying properties of dyadic relations and reasoning about them I: Language extension mechanisms. In H. de Swart, E. Orłowska, M. Roubens, & G. Schmidt (Eds.), Theory and Applications of Relational Structures as Knowledge Instruments (Vol. 2929, pp. 87– 106). Lecture Notes in Computer Science. Berlin: Springer.
Cantone, D., Cavarra, A., & Omodeo, E. (1997). On existentially quantified conjunctions of atomic formulae of \({\mathscr {L}^+}\). In M. P. Bonacina & U. Furbach (Eds.), Proceedings of the FTP97 International Workshop on First-Order Theorem Proving (97–50, pp. 45–52). RISC-Linz Report Series.
Cantone, D., Omodeo, E., & Policriti, A. (2001). Set Theory for Computing–From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Berlin: Springer.
Cantone, D., Formisano, A., Omodeo, E., & Zarba, C. G. (2003). Compiling dyadic first-order specifications into map algebra. Theoretical Computer Science, 293(2), 447–475.
Cantone, D., Formisano, A., Nicolosi Asmundo, M., & Omodeo, E. (2012). A graphical representation of relational formulae with complementation. RAIRO – Theoretical Informatics and Applications, 46(2), 261–289.
Cohen, P. J. (1966). Set Theory and the Continuum Hypothesis. New York: Benjamin.
D’Agostino, G., Montanari, A., & Policriti, A. (1995). A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning, 15(3), 317–337.
Demri, S. & Orłowska, E. (1996). Logical analysis of demonic nondeterministic programs. Theoretical Computer Science, 166(1–2), 173–202.
Demri, S. & Orłowska, E. (2002). Incomplete Information: Structure, Inference, Complexity. Monographs in Theoretical Computer Science. An EATCS series. Berlin: Springer.
Dovier, A., Formisano, A., & Omodeo, E. (2006). Decidability results for sets with atoms. ACM Transactions on Computational Logic, 7(2), 269–301.
Düntsch, I. & Orłowska, E. (2001). Beyond modalities: Sufficiency and mixed algebras. In E. Orłowska & A. Szałas (Eds.), Relational Methods for Computer Science Applications (Vol. 65, pp. 263–285). Studies in Fuzziness and Soft Computing. Heidelberg: Springer-Physica Verlag.
Düntsch, I. & Orłowska, E. (2000). Logics of complementarity in information systems. Mathematical Logic Quarterly, 46(2), 267–288.
Düntsch, I., Orłowska, E., Radzikowska, A., & Vakarelov, D. (2005). Relational representation theorems for some lattice-based structures. Journal of Relational Methods in Computer Science, 1, 132–160.
Formisano, A. & Omodeo, E. (2000). An equational re-engineering of set theories. In R. Caferra & G. Salzer (Eds.), Automated Deduction in Classical and Nonclassical Logics, Selected Papers (Vol. 1761, pp. 175–190). Lecture Notes in Computer Science. Berlin: Springer.
Formisano, A. & Nicolosi Asmundo, M. (2006). An efficient relational deductive system for propositional non-classical logics. Journal of Applied Non-Classical Logics, 16(3–4), 367–408.
Formisano, A. & Simeoni, M. (2001). An AGG application supporting visual reasoning. Electronic Notes in Theoretical Computer Science, 50(3), 302–309.
Formisano, A., Omodeo, E., & Temperini, M. (2000). Goals and benchmarks for automated map reasoning. Journal of Symbolic Computation, 29(2), 259–297.
Formisano, A., Omodeo, E., & Simeoni, M. (2001a). A graphical approach to relational reasoning. Electronic Notes in Theoretical Computer Science, 44(3), 153–174.
Formisano, A., Omodeo, E., & Temperini, M. (2001b). Layered map reasoning: An experimental approach put to trial on sets. Electronic Notes in Theoretical Computer Science, 48, 1–28.
Formisano, A., Omodeo, E., & Temperini, M. (2001c). Instructing equational setreasoning with Otter. In R. Goré, A. Leitsch, & T. Nipkow (Eds.), Automated Reasoning, Proceedings of the 1st International Joint Conference, IJCAR 2001 (Vol. 2083, pp. 152–167). Lecture Notes in Computer Science. Berlin: Springer.
Formisano, A., Omodeo, E., & Policriti, A. (2004). Three-variable statements of set-pairing. Theoretical Computer Science, 322(1), 147–173.
Formisano, A., Omodeo, E., & Policriti, A. (2005). The axiom of elementary sets on the edge of Peircean expressibility. Journal of Symbolic Logic, 70(3), 953–968.
Formisano, A., Omodeo, E., & Orłowska, E. (2006). An environment for specifying properties of dyadic relations and reasoning about them II: Relational presentation of non-classical logics. In H. de Swart, E. Orłowska, M. Roubens, & G. Schmidt (Eds.), Theory and Applications of Relational Structures as Knowledge Instruments II: International Workshops of COST Action 274, TARSKI, 2002–2005, Selected Revised Papers (Vol. 4342, pp. 89–104). Lecture Notes in Artificial Intelligence. Berlin: Springer.
Golińska-Pilarek, J. & Orłowska, E. (2007). Tableaux and dual tableaux: Transformation of proofs. Studia Logica, 85(3), 283–302.
Golińska-Pilarek, J. & Orłowska, E. (2011). Dual tableau for monoidal triangular norm logic MTL. Fuzzy Sets and Systems, 162(1), 39–52.
Goranko, V. (1990). Modal definability in enriched languages. Notre Dame Journal of Formal Logic, 31(1), 81–105.
Humberstone, L. (1983). Inaccessible worlds. Notre Dame Journal of Formal Logic, 24(3), 346–352.
Järvinen, J. & Orłowska, E. (2006). Relational correspondences for lattices with operators. In W. MacCaull, M. Winter, & I. Düntsch (Eds.), Relational Methods in Computer Science: 8th International Seminar on Relational Methods in Computer Science, 3rd International Workshop on Applications of Kleene Algebra, and Workshop of COST Action 274: TARSKI, Selected Revised Papers (Vol. 3929, pp. 134–146). Lecture Notes in Computer Science. Berlin: Springer.
Jech, T. J. (1978). Set Theory. New York: Academic Press.
Jifeng, H. & Hoare, C. A. R. (1986). Weakest prespecifications, Part I. Fundamenta Informaticae, 9, 51–84. Part II: ibidem, 9, 217–252.
Konikowska, B., Morgan, C., & Orłowska, E. (1998). A relational formalisation of arbitrary finite-valued logics. Logic Journal of the IGPL, 6(5), 755–774.
Kwatinetz, M. K. (1981). Problems of Expressibility in Finite Languages. Doctoral dissertation, University of California, Berkeley.
MacCaull, W. & Orłowska, E. (2002). Correspondence results for relational proof systems with applications to the Lambek calculus. Studia Logica, 71(3), 389–414.
MacCaull, W. & Orłowska, E. (2006). A logic of typed relations and its applications to relational databases. Journal of Logic and Computation, 16(6), 789–815.
Maddux, R. D. (2006). Relation Algebras. Studies in Logic and the Foundations of Mathematics. Amsterdam: Elsevier.
Manin, Y. I. (2010). A Course in Mathematical Logic for Mathematicians (2nd ed.). Graduate Texts in Mathematics. Berlin: Springer.
McCune, W. W. (2003). OTTER 3.3 reference manual. CoRR, arXiv:cs.SC/0310056. Retrieved from http://arxiv.org/abs/cs.SC/0310056.
McCune, W. W. (2005–2010). Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/.
Omodeo, E., Orłowska, E., & Policriti, A. (2004). Rasiowa-Sikorski style relational elementary set theory. In R. Berghammer, B. Möller, & G. Struth (Eds.), Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12–17, 2003, Revised Selected Papers (Vol. 3051, pp. 215–226). Lecture Notes in Computer Science. Berlin: Springer.
Omodeo, E., Policriti, A., & Tomescu, A. I. (2012). Infinity, in short. Journal of Logic and Computation, 22(6), 1391–1403.
Orłowska, E. (1988a). Proof system for weakest prespecification. Information Processing Letters, 27(6), 309–313.
Orłowska, E. (1988b). Relational interpretation of modal logics. In H. Andreka, D. Monk, & I. Németi (Eds.), Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai (Vol. 54, pp. 443–471). Amsterdam: North Holland.
Orłowska, E. (1992). Relational proof systems for relevant logics. Journal of Symbolic Logic, 57(4), 1425–1440.
Orłowska, E. (1994). Relational semantics for non-classical logics: Formulas are relations. In J. Woleński (Ed.), Philosophical Logic in Poland (pp. 167–186). New York: Kluwer.
Orłowska, E. (1995). Temporal logics in a relational framework. In L. Bolc & A. Szałas (Eds.), Time and Logic: a Computational Approach (pp. 249–277). University College London Press.
Orłowska, E. (1996). Relational proof systems for modal logics. In H. Wansing (Ed.), Proof Theory of Modal Logics (pp. 55–78). Berlin-New York: Kluwer Academic Publishers.
Orłowska, E. (1997). Relational formalisation of nonclassical logics. In C. Brink, W. Kahl, & G. Schmidt (Eds.), Relational Methods in Computer Science (pp. 90–105). Wien/New York: Springer.
Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.
Orłowska, E. & Vakarelov, D. (2005). Lattice-based modal algebras and modal logics. In P. Hájek, L. Valdés-Villanueva, & D. Westerståhl (Eds.), Logic, Methodology and Philosophy of Science: Proceedings of the 12th International Congress (pp. 147–170). Abstract in the volume of abstracts, 22–23. King’s College London Publications.
Parlamento, F. & Policriti, A. (1991). Expressing infinity without foundation. Journal of Symbolic Logic, 56(4), 1230–1235.
Paulson, L. C. & Grąbczewski, K. (1996). Mechanizing set theory. Journal of Automated Reasoning, 17(3), 291–323.
Rasiowa, H. & Sikorski, R. (1963). The Mathematics of Metamathematics. Warsaw: Polish Scientific Publishers.
Schmidt, G. (2011). Relational Mathematics. Encyclopedia of Mathematics and its Applications. Cambridge: Cambridge University Press.
Schmidt, G. & Ströhlein, T. (1993). Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Berlin: Springer.
Tarski, A. (1953a). A formalization of set theory without variables. Journal of Symbolic Logic, 18, 189 (Abstracts of the 15th meeting of the Association for Symbolic Logic).
Tarski, A. (1953b). Some metalogical results concerning the calculus of relations. Journal of Symbolic Logic, 18, 188–189 (Abstracts of the 15th meeting of the Association for Symbolic Logic).
Tarski, A. & Givant, S. (1987). Formalization of Set Theory Without Variables. Colloquium Publications. Providence: American Mathematical Society.
van Benthem, J., D’Agostino, G., Montanari, A., & Policriti, A. (1996). Modal deduction in second-order logic and set theory-I. Journal of Logic and Computation, 7(2), 251–265.
van Benthem, J., D’Agostino, G., Montanari, A., & Policriti, A. (1998). Modal deduction in second-order logic and set theory-II. Studia Logica, 60(2), 387–420.
Zermelo, E. (1977). Untersuchungen über die Grundlagen der Mengenlehre I. In J. Van Heijenoort (Ed.), From Frege to Gödel – A Source Book in Mathematical Logic, 1879–1931 (3rd edn., pp. 199–215). Cambridge: Harvard University Press.
Acknowledgements
The authors are grateful to the anonymous referees for careful reading and providing invaluable advice: one of them even produced a detailed sketch of the proof of Lemma 6.3 and showed that it must rely on (E). Thanks are also due to Giovanna D’Agostino for pleasant discussions, concerning in particular Sect. 6.2.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Formisano, A., Omodeo, E.G., Policriti, A. (2018). Reasoning on Relations, Modalities, and Sets. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-97879-6_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-97878-9
Online ISBN: 978-3-319-97879-6
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)