Interpolation properties for first-order Gödel logics

Ever since Craigs seminal result on interpolation, interpolation properties have been recognized as important desiderata of logical systems. Craig interpolation has many applications in mathematics and computer science, for instance consistency proofs, model checking, proofs in modular specifications and modular ontologies. A logic L has interpolation if whenever A implies B holds in L there exists a formula I in the common language of A and B such that A implies I and I implies B both hold in L. This project addresses the problem of interpolation for Gödel logics, especially first- order Gödel logics. 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 the corresponding subsets of the set of truth values. The characteristic operator of Gödel logics, the Gödel conditional, is defined as follows: a implies b is true if and only if a is not larger than b and 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.

Ever since Craig's seminal result on interpolation, interpolation properties have been recognized as important desiderata of logical systems. Craig interpolation has many applications in mathematics and computer science, for instance consistency proofs, model checking, proofs in modular specifications and modular ontologies. Recall that a logic L has interpolation if whenever A implies B holds in L there exists a formula I in the common language of A and B such that A implies I and I implies B both hold in L. This project has addressed the problem of interpolation for Gödel logics, especially first-order Gödel logics. Interpolation in some sense exists for two-valued, three-valued, and recursively enumerable infinitely-valued Gödel logics. The main insight of the project has been the dependence of the positive results on proof-theoretic observations, especially expansions, and the negative result on model theoretic observations. Expansions correspond to Herbrand disjunctions within the formulas. The existence of Herbrand disjunctions is one of the most important features of logics, because they show that the logic is in some sense constructive.