Higher-Order Fuzzy Logics and their Categorical Semantics: Higher-Order Linear Completeness and Baaz Translation via Substructural Tripos Theory

There are, in general, two kinds of logical foundations of mathematics, namely set theory and higher-order logic (aka. type theory). Fuzzy set theory and class theory have been studied extensively for a long time. Studies on higher-order fuzzy logic, by contrast, just started more recently and there is much yet to be done. Here we introduce higher-order fuzzy logics over MTL (monoidal t-norm logic; uniform foundations of fuzzy logics such as Hájek's basic logic, Lukasiewicz logic, and Gödel logic); higher-order MTL boils down to the standard higherorder intuitionistic logic (i.e., the internal logic of topos) with the pre-linearity axiom when equipped with the contraction rule. We give uniform categorical semantics for all higher-order fuzzy logics over MTL in terms of tripos theory. We prove the linear completeness of tripos semantics for higher-order fuzzy logics, and a tripos-theoretical Baaz translation theorem, which allows us to simulate higher-order classical logic within fuzzy logics. The relationships between topos theory and fuzzy set theory have been pursued for a long time; yet no complete topos semantics of fuzzy set theory has been found. Here we give complete tripos semantics of higher-order fuzzy logic (or fuzzy type theory).