Abstract We investigate the property of strict coherence in the setting of many-valued logics. Our main results read as follows: (i) a map from an MV-algebra to [0,1] is strictly coherent if and only if it satisfies Carnap’s regularity condition, and (ii) a [0,1]-valued book on a finite set of many-valued events is strictly coherent if and only if it extends to a faithful state of an MV-algebra that contains them. Remarkably this latter result allows us to relax the rather demanding conditions for the Shimony-Kemeny characterisation of strict coherence put forward in the mid 1950s in this Journal.

We investigate uninorm algebras satisfying a strong version of involutiveness. More precisely, we require that negation is an order reversing monoid isomorphism between the positive cone and the negative cone. A rather surprising consequence of this property is that the negative cones of these algebras are BL-algebras which do not admit MV-components with more than two elements. Among other things, we prove standard completeness and co-NP completeness of the logic corresponding to these algebras.

We extend the methodology in Baaz and Fermüller (1999) [5] to systematically construct analytic calculi for semi-projective logics-a large family of (propositional) locally finite many-valued logics. Our calculi, defined in the framework of sequents of relations, are proof search oriented and can be used to settle the computational complexity of the formalized logics. As a case study we derive sequent calculi of relations for Nilpotent Minimum logic and for Hajek's Basic Logic extended with the [Formula: see text]-contraction axiom ([Formula: see text]). The introduced calculi are used to prove that the decidability problem in these logics is Co-NP complete.

In this article, we compare models for many-valued probabilistic reasoning from the point of view of the sets of satisfiable formulas, positive satisfiable formulas, and tautologies. The results arising from this comparison will be used in the final part of the present article to provide results about the computational complexity for the problem of deciding if a formula belongs to one of the previously discussed sets.

We introduce a new approach to conditional probability over many-valued events, which is based on bets. Then we show that this approach fits with Kroupa's approach, and we give two characterizations of coherence for books on conditional many-valued events, the first one based on states, and the second one based on logical coherence of a suitable theory on many-valued logic.

All promiment examples of first-order predicate fuzzy logics are undecidable. This leads to the problem of the arithmetical complexity of their sets of tautologies and satisfiable sentences. This article is a contribution to the general study of this problem. We propose the classes of first-order core and Δ-core fuzzy logics as a good framework to address these arithmetical complexity issues. We obtain general results providing lower bounds for the complexities associated with arbitrary semantics, and we compute upper bounds and exact positions in the arithmetical hierarchy for distinguished semantics: general semantics given by all chains, finite-chain semantics, standard semantics and rational semantics.

We introduce a proof system for Hájek's logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL , are sound and invertible with respect to any valuation of BL into a suitable algebra, called (ω)[0,1]. Refining the notion of reduction tree that arises naturally from RHBL , we obtain a decision algorithm for BL provability whose running time upper bound is 2 O ( n ) , where n is the number of connectives of the input formula. Moreover, if a formula is unprovable, we exploit the constructiveness of a polynomial time algorithm for leaves validity for providing a procedure to build countermodels in (ω)[0, 1]. Finally, since the size of the reduction tree branches is O ( n 3 ), we can describe a polynomial time verification algorithm for BL unprovability.

Abstract Substructural fuzzy logics are substructural logics that are complete with respect to algebras whose lattice reduct is the real unit interval [0, 1]. In this paper, we introduce Uninorm logicULas Multiplicative additive intuitionistic linear logicMAILLextended with the prelinearity axiom((A → B) ∧ t) V ((B → A)∧ t). Axiomatic extensions ofULinclude known fuzzy logics such as Monoidalt-norm logicMIXand Gödel logicG, and new weakening-free logics. Algebraic semantics for these logics are provided by subvarieties of (representable) pointed bounded commutative residuated lattices. Gentzen systems admitting cut-elimination are given in the framework of hypersequents. Completeness with respect to algebras with lattice reduct [0, 1] is established forULand several extensions using a two-part strategy. First, completeness is proved for the logic extended with Takeuti and Titani's density rule. A syntactic elimination of the rule is then given using a hypersequent calculus. As an algebraic corollary, it follows that certain varieties of residuated lattices are generated by their members with lattice reduct [0, 1].

In this work we investigate several complexity and definability problems for the logic ŁΠ12⁠. We show that the universal fragment of the theory of real closed fields can be faithfully interpreted in such a logic. Then we investigate the logics of t-norms definable in ŁΠ12⁠, and we prove that they are all in PSPACE. Finally we show that the most important fuzzy logics are complete with respect to classes of t-norms which are definable in ŁΠ12⁠.

Starting from a decomposition result of monoidal t-norm-based logic (MTL)-chains as ordinal sums, we focus our attention on a particular kind of indecomposable semihoops, namely weakly cancellative semihoops. The weak cancellation property is proved to be the difference between cancellation and pseudocomplementation, so it gives a new axiomatization of product logic and ΠMTL. By adding this property, some new fuzzy logics (propositional and first-order) are defined and studied obtaining some results about their (finite) strong standard completeness and other logical and algebraic properties.

To every many-valued logic L we associate a logic LS obtained from L by the adding of a storage operator* which has some analogies with Girard's exponential !. The algebraic counterpart of * is the operator I associating to any element a of a many-valued algebra the greatest idempotent below a. We investigate the algebraic completeness of the logics obtained in this way, as well as completeness with respect to real and rational-valued semantics. For some of these logics, we also discuss decidability and complexity. In the predicate case, the storage operator allows one to obtain a multiplicative universal quantifier which can be regarded as the iteration of the multiplicative conjunction, in the same way as the usual universal quantifier can be regarded as the iteration of the additive conjunction.

In this paper we investigate the falsehood-free fragments of main residuated fuzzy logics related to continuous t-norms (Hájek's Basic fuzzy logic BL and some well-known axiomatic extensions), and we relate them to the varieties of 0-free subreducts of the corresponding algebras. These turn out to be classes of algebraic structures known as hoops. We provide axiomatizations of all these fragments and we call them hoop logics; we prove they are strongly complete with respect to their corresponding classes of hoops, and that each fuzzy logic is a conservative extension of the corresponding hoop logic. Analogously, we also study the falsehood-free fragment of a weaker logic than BL, called MTL, which is the logic of left-continuous t-norms and their residua, and we introduce the related algebraic structures which are called semihoops. Moreover, we also consider the falsehood-free fragments of the fuzzy predicate calculi of the above logics and show completeness and conservativeness results. The role of axiom (∀3) in these predicate logics is studied. Finally, computational complexity issues of the prepositional logics are also addressed.

We introduce a tableau calculus for Háajek's Basic Logic BL. This calculus has many of the desirable properties of a proof system: it is cut‐free, it has the subformula property, correctness of proof can be checked in P‐time, and the number of symbols in any branch of the reduction tree of any sequent Γ is polynomial in the number of symbols of Γ. As a corollary we obtain an alternative proof of Co‐NP completeness of BL.

Abstract In this paper the modal operator “x is provable in Peano Arithmetic” is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

In Parikh [71] it is shown that, if T is an r.e. consistent extension of Peano arithmetic PA, then, for each primitive recursive function g, there is a formula φ of PA such that (In the following, Proof T(z, φ) and Prov T(φ) denote the metalinguistic assertions that z codes a proof of φ in T and that φ is provable in T respectively, where ProofT(z, ┌φ┐) and ProvT(┌φ┐) are the formalizations of Proof T(z,φ) and ProvT(φ) respectively in the language of PA, ┌φ┐ denotes the Gödel number of φ and ┌φ┐ denotes the corresponding numeral. Also, for typographical reasons, subscripts will not be made boldface.) If g is a rapidly increasing function, we express (1) by saying that ProvT(┌φ┐) has a much shorter proof modulo g than φ. Parikh's result is based on the fact that a suitable formula A(x), roughly asserting that (1) holds with x in place of φ, has only provable fixed points. In de Jongh and Montagna [89], this situation is generalized and investigated in a modal context. There, a characterization is given of arithmetical formulas arising from modal formulas of a suitable modal language which have only provable fixed points, and Parikh's result is obtained as a particular case.

The dominical categories were introduced by Di Paola and Heller, as a first step toward a category-theoretic treatment of the generalized first Godel incompleteness theorem [1]. In his Ph.D. dissertation [7], Rosolini subsequently defined the closely related p-categories, which should prove pertinent to category-theoretic representations of incompleteness for intuitionistic systems. The precise relationship between these two concepts is as follows: every dominical category is a pointed p-category, but there are p-categories, indeed pointed p-isotypes (all pairs of objects being isomorphic) with a Turing morphism that are not dominical. The first of these assertions is an easy consequence of the fact that in a dominical category C by definition the near product functor when restricted to the subcategory Ct, of total morphisms of C (as “total” is defined in [1]) constitutes a bona fide product such that the derived associativity and commutativity isomorphisms are natural on C × C × C and C × C, respectively, as noted in [7]. As to the second, p-recursion categories (that is, pointed p-isotypes having a Turing morphism) that are not dominical were defined and studied by Montagna in [6], the syntactic p-categories ST and S′T associated with consistent, recursively enumerable extensions of Peano arithmetic, PA. These merit detailed investigation on several counts.

Recursion categories have been proposed by Di Paola and Heller in [DPH] as the basis for a category-theoretic approach to recursion theory, in the context of a more general and ambitious project of a purely algebraic treatment of incompleteness phenomena. The way in which the classical notion of creative set is rendered in this new category-theoretic framework plays, therefore, a central role. This is done in [DPH] (Definition 8.1) by defining the notion of creative domains or, rather, domains which are creative relative to some criterion: thus, in a recursion category, every criterion provides a notion of creativeness. A basic result on creative domains (cf. [DPH, Theorem 8.13]) is that, under certain assumptions, a version of the classical result, due to Myhill [MYH], stating that every creative set is complete, holds: in a recursion category with equality (i.e. exists for every object X) and having enough atoms, every domain which is creative with respect to atoms is also complete.

By Solovay's theorem [16], the modal logic of provability GL gives a complete description of the propositional schemata involving the provability predicate PrPA(x) for Peano arithmetic PA, which are provable in PA. However, many important aspects of provability cannot be fully expressed in terms of PrPA(x). For this reason, many authors have introduced extensions of GL which take account either of Rosser constructions or of other important metamathematical formulas (see, for example, [5], [6], [14], [16], and [19]). In this paper, we concentrate on the modal logic of the provability predicate for finitely axiomatizable subtheories of PA; the interest of this modal logic is based on the following facts. First of all, it provides a modal translation of a very important property of PA, namely the essential reflexiveness. Secondly, in view of Orey's theorem [10] it constitutes a possible approach to the study of interpretability of finite extensions of PA. Indeed, by Orey's theorem PA + θ is interpretable in PA + θ′ iff for every n, and, therefore, relative interpretability of finitely axiomatizable extensions of PA can be expressed by means of the provability predicate for finitely axiomatizable subtheories of PA. In §1, we introduce three modal logics extending GL and discuss their arithmetical interpretations; §2 deals with Kripke semantics for two of these logics. In §3, a theorem on arithmetical completeness is shown, which characterizes the logic of the provability predicate for finitely axiomatizable subtheories of PA; a uniform version of this theorem is proved in §4.

When dealing with axiomatic theories from a recursion-theoretic point of view, the notion of r.e. preordering naturally arises. We agree that an r.e. preorder is a pair = 〈P, ≤P〉 such that P is an r.e. subset of the set of natural numbers (denoted by ω), ≤P is a preordering on P and the set {〈;x, y〉: x ≤Py} is r.e.. Indeed, if is an axiomatic theory, the provable implication of yields a preordering on the class of (Gödel numbers of) formulas of . Of course, if ≤P is a preordering on P, then it yields an equivalence relation ~P on P, by simply letting x ~Py iff x ≤Py and y ≤Px. Hence, in the case of P = ω, any preordering yields an equivalence relation on ω and consequently a numeration in the sense of [4]. It is also clear that any equivalence relation on ω (hence any numeration) can be regarded as a preordering on ω. In view of this connection, we sometimes apply to the theory of preorders some of the concepts from the theory of numerations (see also Eršov [6]). Our main concern will be in applications of these concepts to logic, in particular as regards sufficiently strong axiomatic theories (essentially the ones in which recursive functions are representable). From this point of view it seems to be of some interest to study some remarkable prelattices and Boolean prealgebras which arise from such theories. It turns out that these structures enjoy some rather surprising lattice-theoretic and universal recursion-theoretic properties. After making our main definitions in §1, we examine universal recursion-theoretic properties of some r.e. prelattices in §2.