Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation

TL;DR

This paper introduces a novel, purely model-theoretic semantics for negation in extensional higher-order logic programming, ensuring a unique minimum model and resolving longstanding semantic paradoxes.

Contribution

It provides the first purely model-theoretic semantics for negation in extensional higher-order logic programming, based on non-monotonic fixed-point theory.

Findings

Every higher-order logic program with negation has a unique minimum infinite-valued model.

The approach resolves the semantic paradox introduced by Wadge.

It preserves key properties of traditional logic programming.

Abstract

Extensional higher-order logic programming has been introduced as a generalization of classical logic programming. An important characteristic of this paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we consider the semantics of negation in the context of the new paradigm. Using some recent results from non-monotonic fixed-point theory, we demonstrate that every higher-order logic program with negation has a unique minimum infinite-valued model. In this way we obtain the first purely model-theoretic semantics for negation in extensional higher-order logic programming. Using our approach, we resolve an old paradox that was introduced by W. W. Wadge in order to demonstrate the semantic difficulties of higher-order logic programming.