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

EasyChair Preprint 3621, version 2

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. Contributions of this paper include (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.

Keyphrases: Free Higher-Order Logic, Interactive and Automated Theorem Proving, Knowledge Representation and Reasoning, Partiality and undefinedness, Philosophical foundations of AI, Prior’s paradox, free logic, positive free logic

@booklet{EasyChair:3621,
  author    = {Irina Makarenko and Christoph Benzmüller},
  title     = {Positive Free Higher-Order Logic and its Automation via a Semantical Embedding},
  howpublished = {EasyChair Preprint 3621},
  year      = {EasyChair, 2020}}