Free Higher-Order Logic - Notion, Definition and Embedding in HOL

Abstract

Free logics are a family of logics that are free of any existential assumptions. This family can roughly be divided into positive, negative, neutral and supervaluational free logic whose semantics differ in the way how nondenoting terms are treated. While there has been remarkable work done concerning the definition of free first-order logic, free higher-order logic has not been addressed thoroughly so far. The purpose of this thesis is, firstly, to give a notion and definition of free higher-order logic based on simple type theory and, secondly, to propose faithful shallow semantical embeddings of free higher-order logic into classical higher order logic found on this definition. Such embeddings can then effectively be utilized to enable the application of powerful state-of-the-art higher-order interactive and automated theorem provers for the formalization and verification and also the further development of increasingly important free logical theories.