Skolemization and Herbrand Theorems for Lattice-Valued Logics

Abstrakt

In classical first-order logic, questions of validity and semantic consequence reduce to the satisfiability of a set of sentences; Skolemization methods and Herbrand theorems then further reduce these questions to the satisfiability of a set of propositional formulas (see, e.g., [4]). For first-order non-classical logics, the situation is not so straightforward. First, due to the absence of certain quantifier shifts, formulas are not always equivalent to prenex formulas, and, second, semantic consequence does not (typically) reduce to satisfiability. Hence (non-prenex) sentences should be considered separately as premises and conclusions of consequences. General Skolemization methods and Herbrand theorems therefore take various forms, applying either to the left or right of the consequence relation, and to restricted sets of formulas.