Top

Published in:

2020 | OriginalPaper | Chapter

Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding

Authors : Irina Makarenko, Christoph Benzmüller

Published in: KI 2020: Advances in Artificial Intelligence

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Free logics are a family of logics that are free of any existential assumptions. Unlike traditional classical and non-classical logics, they support an elegant modeling of nonexistent objects and partial functions as relevant for a wide range of applications in computer science, philosophy, mathematics, and natural language semantics. While free first-order logic has been addressed in the literature, free higher-order logic has not been studied thoroughly so far. The contribution of this paper includes (i) the development of a notion and definition of free higher-order logic in terms of a positive semantics (partly inspired by Farmer’s partial functions version of Church’s simple type theory), (ii) the provision of a faithful shallow semantical embedding of positive free higher-order logic into classical higher-order logic, (iii) the implementation of this embedding in the Isabelle/HOL proof-assistant, and (iv) the exemplary application of our novel reasoning framework for an automated assessment of Prior’s paradox in positive free quantified propositional logics, i.e., a fragment of positive free higher-order logic.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Nonmonotonic Inferences with Qualitative Conditionals Based on Preferred Structures on Worlds

next chapter Low-Rank Subspace Override for Unsupervised Domain Adaptation

Available only for authorised users

There is no serious restriction to a two-valued base set so that further base types could be added [8].

The set of primitive logical constants could be a much smaller one, e.g., equality is known to be sufficient in order to define all remaining logical constants of classical higher-order logic apart from the description operator [6].

For an abstraction, being right-associative means that its body extends as far right as possible. For instance, \( \lambda x. s \, t \) corresponds to \( \lambda x. \, ( s \, t ) \) and not \( (\lambda x. \, s ) \, t \).

In the paper at hand, the terms existent/existing and defined are used interchangeably even though a differentiation is advisable. The same applies to the terms nonexistent/nonexisting and undefined.

Restricting nondenotation to the domain of individuals, i.e., to define \( E_i \subsetneq D_i \) and for all \( \alpha \ne i \), \( E_\alpha \! = \! D_\alpha \), is reasonable but complicates the definition of strict functions.

Farmer also checked the function itself for existence. But since the distinction between existing and nonexisting functions – in contrast to existing/nonexisting individuals – is unusual and not well-defined, this was left out.

Restraining applications like this could lead to malformed evaluations, i.e., evaluated terms might not receive the actually intended value. For instance, the ite operator must be handled separately when the then- or else-parts are meant to be undefined.

As shown by Farmer and Schütte [31], it is possible to give a Henkin-style completeness proof for free higher-order logic defined based on a partial valuation function.

A similar translation, although for free first-order logic, was provided and proved to be sound and complete by Meyer and Lambert [26] and Benzmüller and Scott [10].

The Isabelle/HOL sources are also available at https://github.com/stilleben/Free-Higher-Order-Logic.

Andrews, P.B.: General models and extensionality. J. Symbol. Logic 37(2), 395–397 (1972)MathSciNetMATHCrossRef

Andrews, P.B.: General models, descriptions, and choice in type theory. J. Symbol. Logic 37(2), 385–394 (1972)MathSciNetMATHCrossRef

Bacon, A., Hawthorne, J., Uzquiano, G.: Higher-order free logic and the Prior-Kaplan paradox. Canadian J. Philos. 46(4–5), 493–541 (2016)CrossRef

Bencivenga, E.: Free logics. In: Gabbay, D.M., Günthner, F. (eds.) Handbook of Philosophical Logic. Volume III: Alternatives in Classical Logic, pp. 373–426. Springer, Netherlands, Dordrecht (1986)CrossRef

Benzmüller, C.: Universal (Meta-)logical reasoning: recent successes. Sci. Comput. Program. 172, 48–62 (2019)CrossRef

Benzmüller, C., Andrews, P.B.: Church’s type theory. In: Zalta, E.N. (ed.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2019 edition (2019)

Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symbol. Logic 69(4), 1027–1088 (2004)MathSciNetMATHCrossRef

Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Computational Logic. Handbook of the History of Logic, vol. 9, pp. 215–254. Elsevier, North Holland (2014)MATHCrossRef

Benzmüller, C., Parent, X., van der Torre, L.: Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artif. Intell. 287, 103348 (2020)MathSciNetCrossRef

10.

Benzmüller, C., Scott, D.S.: Automating free logic in HOL, with an experimental application in category theory. J. Autom. Reason. 64(1), 53–72 (2019). https://doi.org/10.1007/s10817-018-09507-7MathSciNetMATHCrossRef

11.

Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11CrossRef

12.

Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111–117. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_11CrossRef

13.

Church, A.: A formulation of the simple theory of types. J. Symbol. Logic 5(2), 56–68 (1940)MathSciNetMATHCrossRef

14.

Farmer, W.M.: A Partial Functions Version of Church’s Simple Theory of Types. J. Symbol. Log. 55, 1269–1291 (1990)MathSciNetMATHCrossRef

15.

Feferman, S.: Logics for termination and correctness of functional programs. In: Moschovakis, Y.N. (ed.) Logic from Computer Science, pp. 95–127. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-2822-6_5CrossRef

16.

Gumb, R.D.: Free logic in program specification and verification. In: Morscher, E., Hieke, A. (eds.) New Essays in Free Logic. In Honour of Karel Lambert, vol. 23, pp. 157–193. In Honour of Karel Lambert. Springer, Dordrecht (2001). https://doi.org/10.1007/978-94-015-9761-6_9CrossRef

17.

Gumb, R.D., Lambert, K.: Definitions in nonstrict positive free logic. Modern Logic 7(1), 25–55 (1997)MathSciNetMATH

18.

Henkin, L.: Completeness in the theory of types. J. Symbol. Logic 15(2), 81–91 (1950)MathSciNetMATHCrossRef

19.

Kaplan, D.: A problem in possible worlds semantics. In: Sinnott-Armstrong, W., Raffman, D., Asher, N. (eds.) Modality, Morality and Belief: Essays in Honor of Ruth Barcan Marcus, pp. 41–52. Cambridge University Press, Cambridge (1995)

20.

Kirchner, D., Benzmüller, C., Zalta, E.N.: Mechanizing principia Logico-Metaphysica in functional type theory. Rev. Symbol. Logic 13(1), 206–218 (2020)MathSciNetMATHCrossRef

21.

Lambert, K.: The Definition of E! in Free Logic. The International Congress for Logic, Methodology and Philosophy of Science, Abstracts (1960)

22.

Lambert, K.: Free logic and the concept of existence. Notre Dame J. Formal Logic 1–2(8), 133–144 (1967)MathSciNetMATHCrossRef

23.

Lambert, K.: Philosophical Applications of Free Logic. Oxford University Press, Oxford (1991)

24.

Lehmann, S.: ‘No Input, No Output’ Logic. In: Morscher, E., Hieke, A. (eds.) New Essays in Free Logic. In Honour of Karel Lambert, vol. 23, pp. 147–155. Springer, Netherlands, Dordrecht (2001). https://doi.org/10.1007/978-94-015-9761-6_8CrossRef

25.

Makarenko, I.: Free Higher-Order Logic - Notion, Definition and Embedding in HOL. Master’s thesis, Freie Universität Berlin (2020)

26.

Meyer, R.K., Lambert, K.: Universally free logic and standard quantification theory. J. Symbol. Logic 33(1), 8–26 (1968)MathSciNetMATHCrossRef

27.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic (2019). http://isabelle.in.tum.de/doc/tutorial.pdf. Accessed 30 Dec 2019

28.

Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 131–146 (2015)

29.

Prior, A.N.: On a Family of Paradoxes. Notre Dame J. Formal Logic 2(1), 16–32 (1961)MathSciNetMATHCrossRef

30.

Schock, R.: Logics Without Existence Assumptions. Almqvist & Wiksell, Stockholm (1968)MATH

31.

Schütte, K.: Syntactical and semantical properties of simple type theory. J. Symbol. Logic 25(4), 305–326 (1960)MathSciNetMATHCrossRef

32.

Dana Scott. Existence and Description in Formal Logic. In Ralph Schoenman, editor, Bertrand Russell: Philosopher of the Century, pages 181–200. Little, Brown & Company, Boston, 1967. Repr. in [23], pp. 28–48

33.

Steen, A., Benzmüller, C.: Sweet SIXTEEN: automation via embedding into classical higher-Order Logic. Logic Logical Philos. 25(4), 535–554 (2016)MathSciNetMATH

34.

Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108–116. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_8CrossRef

35.

Villadsen, J., Schlichtkrull, A.: Formalization of many-valued logics. In: Christiansen, H., Dolores Jiménez-López, M., Loukanova, R., Moss, L.S. (eds.), Partiality and Underspecification in Information, Languages, and Knowledge, pp. 219–256. Cambridge Scholars Press (2017)

36.

Zalta, E.N.: Principia Logico-Metaphysica. http://mally.stanford.edu/principia.pdf. Draft/Excerpt; Accessed 31 May 2020

Title: Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding
Authors: Irina Makarenko
Christoph Benzmüller
Publisher: Springer International Publishing
Book: KI 2020: Advances in Artificial Intelligence
Print ISBN: 978-3-030-58284-5

Electronic ISBN: 978-3-030-58285-2

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-58285-2_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner