Uniform Algebras: Models and constructive Completeness for Full, Simply Typed {\lambda}Prolog

TL;DR

This paper develops a model theory for resolution in Higher Order Hereditarily Harrop formulae, proving soundness and completeness, and introduces new methods to handle the impredicativity of higher-order logic.

Contribution

It presents a novel model-theoretic framework and constructive completeness proof for resolution in HOHH, addressing impredicativity challenges in higher-order logic.

Findings

Proves soundness and completeness of resolution for HOHH

Introduces a fixed point semantics for higher-order logic

Develops a constructive completeness theorem with a new cut-elimination approach

Abstract

This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves soundness and completeness of resolution. The semantics and the proof of completeness of the formal system is shown in several ways, suitably adapted to deal with the impredicativity of higher-order logic, which rules out definitions of truth based on induction on formula structure. First, we use the least fixed point of a certain operator on interpretations, in the style of Apt and Van Emden, Then a constructive completeness theorem is given using a proof theoretic variant of the Lindenbaum algebra, which also contains a new approach to establishing cut-elimination.