Expanding Gödel logic with truth constants and the equality, strict order, delta operators

Abstract

Concerning the three fundamental first-order fuzzy logics, the set of logically valid formulae is Π2-complete for Łukasiewicz logic, Π2-hard for Product logic, and Σ1-complete for Gödel logic, as with classical first-order logic. Among these fuzzy logics, only Gödel logic is recursively axiomatisable. Hence, it was necessary to provide a hyperresolution-based proof method suitable for automated deduction, as one has done for classical logic. As another step, we can incorporate a countable set of intermediate truth constants of the form. c, c ∈ (0, 1), together with the equality, ≖, strict order, ≺, projection, Δ, operators in Gödel logic; and modify the hyperresolution calculus, inferring over so-called order clauses. We shall investigate the deduction problem of a formula from a countable theory in this expansion and the so-called canonical standard completeness, where the semantics of Gödel logic is given by the standard G-algebra as well as truth constants are interpreted by ‘themselves’. The hyperresolution calculus is refutation sound and complete for a countable order clausal theory under a certain condition for the set of truth constants occurring in the theory. We get an affirmative solution to the open problem of recursive enumerability of unsatisfiable formulae in this expansion of Gödel logic.