First-order typed fuzzy logics and their categorical semantics: Linear completeness and baaz translation via lawvere hyperdoctrine theory

It is known that some fuzzy predicate logics, such as Łukasiewicz predicate logic, are not complete with respect to the standard real-valued semantics. In the present paper we focus upon a typed version of first-order MTL (Monoidal T-norm Logic), which gives a unified framework for different fuzzy logics including, inter alia, Hajek's basic logic, Łukasiewicz logic, and Gödel logic. And we show that any extension of first-order typed MTL, including Łukasiewicz predicate logic, is sound and complete with respect to the corresponding categorical semantics in the style of Lawvere's hyperdoctrine, and that the so-called Baaz delta translation can be given in the first-order setting in terms of Lawvere's hyperdoctrine. A hyperdoctrine may be seen as a fibred algebra, and the first-order completeness, then, is a fibred extension of the algebraic completeness of propositional logic. While the standard real-valued semantics for Łukasiewicz predicate logic is not complete, the hyperdoctrine, or fibred algebraic, semantics is complete because it encompasses a broader class of models that is sufficient to prove completeness; in this context, incompleteness may be understood as telling that completeness does not hold when the class of models is restricted to the standard class of real-valued hyperdoctrine models. We expect that this finally leads to a unified categorical understanding of Takeuti-Titani's fuzzy models of set theory.