Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Skolemization In Intermediate Logics

Matthias Baaz, Mariami Gamsakhurdia, Rosalie Iemhoff, Raheleh Jalali

TL;DR

This article characterize intermediate first-order logics that admit standard (and Andrews) Skolemization and analyzes predicate intuitionistic logic with quantifier shift axioms and demonstrates its Kripke frame-incompleteness, may foster resolution-based theorem provers for non-classical logics.

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.

Skolemization In Intermediate Logics

TL;DR

This article characterize intermediate first-order logics that admit standard (and Andrews) Skolemization and analyzes predicate intuitionistic logic with quantifier shift axioms and demonstrates its Kripke frame-incompleteness, may foster resolution-based theorem provers for non-classical logics.

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.
Paper Structure (17 sections, 36 theorems, 191 equations, 1 figure, 1 table)

This paper contains 17 sections, 36 theorems, 191 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Sequent Calculi
  4. Kripke Frames and Models
  5. Skolemization
  6. Logic of quantifier shifts
  7. Turning to Proof Theory
  8. From deSkolemization to quantifier shifts
  9. Sequent calculi ${\bf LK}^{++}$ and ${\bf LJ}^{++}$
  10. From quantifier shifts to deSkolemization
  11. Parallel Skolemization
  12. Frame-incompleteness
  13. Frame characterization
  14. Kripke frame-incompleteness
  15. Fragments of $\mathsf{QFS}$
  16. ...and 2 more sections

Key Result

Theorem 17

The logics $\mathsf{QFS}$, $\mathsf{IQC}+ \{\mathrm{CD} , \mathrm{SW}\},$ and $\mathsf{IQC}+ \{\mathrm{CD} , \mathrm{ED}\}$ are all frame-incomplete.

Figures (1)

  • Figure 1: The lattice-based 5-valued logic.

Theorems & Definitions (101)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Remark 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Definition 10
  • ...and 91 more