Gödel logics: the prenex forms

The existence of logically equivalent prenex forms is one of the oldest observed properties of classical first-order logic. These prenex forms are generated in a non-unique way using the shift of quantifiers. Prenex forms are the original basis of Herbrands theorem and thereby of automated theorem proving (Herbrands theorem is a statement that a valid existential formula corresponds to a propositionally valid disjunction). In this project we intend to determine the relation of Gödel logics to its prenex fragments. Gödel logics were introduced by Gödel in 1932 to show that there are countably many propositional logics between intuitionistic and classical propositional logic. Gödel logics can be characterized in a roughand-ready way as follows: The language is a standard (propositional, quantified propositional, first-order) language. The logics are many-valued, and the sets of truth values considered are (closed) subsets of [0, 1] which contain both 0 and 1. 1 is the designated value, i.e., a formula is valid if it receives the value 1 in every interpretation. The truth functions of conjunction and disjunction are minimum and maximum, respectively, and in the first-order case quantifiers are defined by infimum and supremum over subsets of the set of truth values. The characteristic operator of Gödel logics, the Gödel conditional, is defined by: A implies B is true if A is less or equal B, and A implies B is B otherwise. As the evaluation of a formula depends only on the order and not on the size of the truth values involved Gödel logics are suitable for formalizing comparisons. Gödel logics are also intermediary logics, specified by finitely or countable linearly ordered Kripke frames of constant domain. The prenex fragments of Gödel logics admit Skolemization, and are therefore the basis of reasonable automated theorem proving procedures. Furthermore the prenex fragments admit Herbrands theorems or approximative versions thereof. In addition they provide general normal form theorems which demonstrate the complexity of particular Gödel logics.