Skolemization In Intermediate Logics

TL;DR

This paper characterizes which intermediate first-order logics support standard Skolemization, introduces new Skolem functions for some non-standard cases, and analyzes predicate intuitionistic logic's frame-incompleteness, advancing theorem proving in non-classical logics.

Contribution

It identifies conditions for Skolemization in intermediate logics, develops innovative Skolem functions for non-standard cases, and analyzes the frame-incompleteness of predicate intuitionistic logic.

Findings

Intermediate logics admitting classical Skolemization are characterized.

New Skolem functions are developed for certain non-standard logics.

Predicate intuitionistic logic with quantifier shift axioms is shown to be Kripke frame-incomplete.

Abstract

Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classical quantifier shift principles. For some logics not in this category, innovative forms of Skolem functions are developed that allow Skolemization. Moreover, we analyze predicate intuitionistic logic with quantifier shift axioms and demonstrate its Kripke frame-incompleteness. These findings may foster resolution-based theorem provers for non-classical logics. This article is part of a larger project investigating Skolemization in non-classical logics.