A method is described for obtaining conjunctive normal forms for logics using Gentzen-style rules possessing a special kind of strong invertibility. This method is then applied to a number of prominent fuzzy logics using hypersequent rules adapted from calculi defined in the literature. In particular, a normal form with simple McNaughton functions as literals is generated for łukasiewicz logic, and normal forms with simple implicational formulas as literals are obtained for Gödel logic, Product logic, and Cancellative hoop logic.

A t-tautology is a propositional formula which is a tautology in all fuzzy logics defined by continuous triangular norms. In this paper we show that the problem of recognizing t-tautologies is coNP complete, and thus decidable.

We consider an extension of Gödel logic by a unary operator that enables the addition of non-negative reals to truth-values. Although its propositional fragment has a simple proof system, first-order validity is Π2-hard. We explain the close connection to Scarpellini’s result on Π2-hardness of Łukasiewicz’s logic.

Entailment in propositional Gödel logics can be defined in a natural way. While all infinite sets of truth values yield the same sets of tautologies, the entailment relations differ. It is shown that there is a rich structure of infinite-valued Gödel logics, only one of which is compact. It is also shown that the compact infinite-valued Gödel logic is the only one which interpolates, and the only one with an r.e. entailment relation.

The last decade has seen an enormous development in infinite-valued systems and in particular in such systems which have become known as mathematical fuzzy logics. The paper discusses the mathematical background for the interest in such systems of mathematical fuzzy logics, as well as the most important ones of them. It concentrates on the propositional cases, and mentions the first-order systems more superficially. The main ideas, however, become clear already in this restricted setting.

We present a semantic game for Gödel logic and its extensions, where the players’ interaction stepwise reduces arbitrary claims about the relative order of truth degrees of complex formulas to atomic ones. The paper builds on a previously developed game for Gödel logic with projection operator in Fermüller et al., Information processing and management of uncertainty in knowledge-based systems, Springer, Cham, 2020, pp. 257–270). This game is extended to cover Gödel logic with involutive negations and constants, and then lifted to (...) a provability game using the concept of disjunctive strategies. Winning strategies in the provability game, with and without constants and involutive negations, turn out to correspond to analytic proofs in a version of \ :1941–1958, 2010) and in a sequent-of-relations calculus, Automated reasoning with analytic tableaux and related methods, Springer, Berlin, 1999, pp. 36–51) respectively. (shrink)

In this paper we give a rather detailed algebraic investigation of interpolation and Beth’s property in propositional many-valued logics extending Hájek’s Basic Logic [P. Hájek, Metamathematics of Fuzzy Logic, Kluwer, 1998], and we connect such properties with amalgamation and strong amalgamation in the corresponding varieties of algebras. It turns out that, while the most interesting extensions of in the language of have deductive interpolation, very few of them have Beth’s property or Craig interpolation. Thus in the last part of the (...) paper we look for conservative extensions of having such properties. (shrink)

In this paper we investigate the connections between quantifier elimination, decidability and Uniform Craig Interpolation in Δ-core fuzzy logics added with propositional quantifiers. As a consequence, we are able to prove that several propositional fuzzy logics have a conservative extension which is a Δ-core fuzzy logic and has Uniform Craig Interpolation.

The Craig interpolation property is investigated for substructural logics whose algebraic semantics are varieties of semilinear pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the “R-mingle with unit” logic that have the Craig interpolation property. This latter characterization is obtained using a model-theoretic quantifier elimination strategy to determine the varieties of Sugihara monoids (...) admitting the amalgamation property. (shrink)

Formulas of n variables of Łukasiewicz sentential calculus can be represented, via McNaughton’s theorem, by piecewise linear functions, with integer coefficients, from hypercube [0,1] n to [0,1], called McNaughton functions. As a consequence of the McNaughton representation of a formula it is obtained a canonical form of a formula. Indeed, up to logical equivalence, any formula can be written as an infimum of finite suprema of formulas associated to McNaughton functions which are truncated functions to $[0,1]$ of the restriction to (...) [0,1] n of single hyperplanes, for short, called simple McNaughton functions. In the present paper we will concern with the problem of presenting formulas of Lukasiewicz sentential calculus in normal form. Here we list the main results we obtained: a) we give an axiomatic description of some classes of formulas having the property to be canonically mapped one-to-one onto the class of simple Mc Naughton functions; b) we provide normal forms for Lukasiewicz sentential calculus, making use of formulas defined in a); c) we prove the polynomial complexity of formulas, in normal form, coming from a certain class described as in a); d) we extend the results described in a), b) and c) to Rational Lukasiewicz logic. (shrink)

It is shown that Gqp↑, the quantified propositional Gödel logic based on the truth-value set V↑ = {1 - 1/n : n≥1}∪{1}, is decidable. This result is obtained by reduction to Büchi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of Gqp↑ as the intersection of all finite-valued quantified propositional Gödel logics.