Brouwer's views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing generality: from the least general Kripke (...) semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order (...) logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

Hereditary structural completeness is established for a range of substructural logics, mainly without the weakening rule, including fragments of various relevant or many-valued logics. Also, structural completeness is disproved for a range of systems, settling some previously open questions.

This paper is a contribution to the study of the rôle of disjunction inAlgebraic Logic. Several kinds of (generalized) disjunctions, usually defined using a suitable variant of the proof by cases property, were introduced and extensively studied in the literature mainly in the context of finitary logics. The goals of this paper are to extend these results to all logics, to systematize the multitude of notions of disjunction (both those already considered in the literature and those introduced in this paper), (...) and to show several interesting applications allowed by the presence of a suitable disjunction in a given logic. (shrink)

Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon $ - (...) and $\tau $ -formulas and using the translation of quantifiers into $\varepsilon $ - and $\tau $ -terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate ${\varepsilon \tau }$ -calculi. The “extended” first $\varepsilon $ -theorem holds if the base logic is finite-valued Gödel–Dummett logic, and fails otherwise, but holds for certain provable formulas in infinite-valued Gödel logic. The second $\varepsilon $ -theorem also holds for finite-valued first-order Gödel logics. The methods used to prove the extended first $\varepsilon $ -theorem for infinite-valued Gödel logic suggest applications to theories of arithmetic. (shrink)

A continuoxis t- norm is a continuous map * from [0, 1]² into [0,1] such that is a commutative totally ordered monoid. Since the natural ordering on [0,1] is a complete lattice ordering, each continuous t-norm induces naturally a residuation → and becomes a commutative naturally ordered residuated monoid, also called a hoop. The variety of basic hoops is precisely the variety generated by all algebras, where * is a continuous t-norm. In this paper we investigate the structure of the (...) variety of basic hoops and some of its subvarieties. In particular we provide a complete description of the finite subdirectly irreducible basic hoops, and we show that the variety of basic hoops is generated as a quasivariety by its finite algebras. We extend these results to Hájek's BL-algebras, and we give an alternative proof of the fact that the variety of BL-algebras is generated by all algebras arising from continuous t-norms on [ 0,1] and their residua. The last part of the paper is devoted to the investigation of the subreducts of BL- algebras, of Gödel algebras and of product algebras. (shrink)

This paper is a contribution to Mathematical fuzzy logic, in particular to the algebraic study of t-norm based fuzzy logics. In the general framework of propositional core and Δ-core fuzzy logics we consider three properties of completeness with respect to any semantics of linearly ordered algebras. Useful algebraic characterizations of these completeness properties are obtained and their relations are studied. Moreover, we concentrate on five kinds of distinguished semantics for these logics–namely the class of algebras defined over the real unit (...) interval, the rational unit interval, the hyperreals , the strict hyperreals and finite chains, respectively–and we survey the known completeness methods and results for prominent logics. We also obtain new interesting relations between the real, rational and hyperreal semantics, and good characterizations for the completeness with respect to the semantics of finite chains. Finally, all completeness properties and distinguished semantics are also considered for the first-order versions of the logics where a number of new results are proved. (shrink)

Visser's rules form a basis for the admissible rules of . Here we show that this result can be generalized to arbitrary intermediate logics: Visser's rules form a basis for the admissible rules of any intermediate logic for which they are admissible. This implies that if Visser's rules are derivable for then has no nonderivable admissible rules. We also provide a necessary and sufficient condition for the admissibility of Visser's rules. We apply these results to some specific intermediate logics and (...) obtain that Visser's rules form a basis for the admissible rules of, for example, De Morgan logic, and that Dummett's logic and the propositional Gödel logics do not have nonderivable admissible rules. (shrink)

In this paper we define and study a generalized notion of a logical system that covers on an equal formal basis sentential, equational and sequential systems. We develop a general theory of equivalence between generalized logics that provides, first, a conception of algebraizable logic , second, a formal concept of equivalence between sequential systems and, third, a notion of equivalence between sentential and sequential systems. We also use our theory of equivalence for developing a general algebraic approach to conjunctive non-pseudo-axiomatic (...) self-extensional sentential logics. Finally, we consider within the framework of the mentioned approach various sequential formulations for some well-known sentential logics. (shrink)

Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by researchers (...) in the area, including the authors. In addition to providing alternative elegant presentations of fuzzy logics, proof-theoretic methods are useful for addressing theoretical problems and developing efficient deduction and decision algorithms. Proof-theoretic presentations also place fuzzy logics in the broader landscape of non-classical logics, revealing deep relations with other logics studied in Computer Science, Mathematics, and Philosophy. The book builds methodically from the semantic origins of fuzzy logics to proof-theoretic presentations such as Hilbert and Gentzen systems, introducing both theoretical and practical applications of these presentations. (shrink)

First-order Gödel logics are a family of finite- or infinite-valued logics where the sets of truth values V are closed subsets of [0,1] containing both 0 and 1. Different such sets V in general determine different Gödel logics GV (sets of those formulas which evaluate to 1 in every interpretation into V). It is shown that GV is axiomatizable iff V is finite, V is uncountable with 0 isolated in V, or every neighborhood of 0 in V is uncountable. Complete (...) axiomatizations for each of these cases are given. The r.e. prenex, negation-free, and existential fragments of all first-order Gödel logics are also characterized. (shrink)

It is proved that there are exactly 16 superintuitionistic propositional logics with the projective Beth property. These logics are finitely axiomatizable and have the finite model property. Simultaneously, all varieties of Heyting algebras with strong epimorphisms surjectivity are found.

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)

We study the topic of realization from classical justification logics in the context of the recently introduced Gödel justification logics. We show that the standard Gödel modal logics of Caicedo and Rodriguez are not realized by the Gödel justification logics and moreover, we study possible extensions of the Gödel justification logics, which are strong enough to realize the standard Gödel modal logics. On the other hand, we study the fragments of the standard Gödel modal logics, which are realized by the (...) usual Gödel justification logics. We prove the corresponding realization theorem by using Fitting’s merging of realizations as well as appropriate hypersequent calculi on the modal side, adapting the work by Metcalfe and Olivetti. For these hypersequent calculi, we also show a cut-elimination theorem. We provide natural semantical characterizations for all of these newly introduced logics. (shrink)

This book offers a concise introduction to both proof-theory and algebraic methods, the core of the syntactic and semantic study of logic respectively. The importance of combining these two has been increasingly recognized in recent years. It highlights the contrasts between the deep, concrete results using the former and the general, abstract ones using the latter. Covering modal logics, many-valued logics, superintuitionistic and substructural logics, together with their algebraic semantics, the book also provides an introduction to nonclassical logic for undergraduate (...) or graduate level courses.The book is divided into two parts: Proof Theory in Part I and Algebra in Logic in Part II. Part I presents sequent systems and discusses cut elimination and its applications in detail. It also provides simplified proof of cut elimination, making the topic more accessible. The last chapter of Part I is devoted to clarification of the classes of logics that are discussed in the second part. Part II focuses on algebraic semantics for these logics. At the same time, it is a gentle introduction to the basics of algebraic logic and universal algebra with many examples of their applications in logic. Part II can be read independently of Part I, with only minimum knowledge required, and as such is suitable as a textbook for short introductory courses on algebra in logic. (shrink)

Justification logics are special kinds of modal logics which provide a framework for reasoning about epistemic justifications. For this, they extend classical boolean propositional logic by a family of necessity-style modal operators “t : ”, indexed over t by a corresponding set of justification terms, which thus explicitly encode the justification for the necessity assertion in the syntax. With these operators, one can therefore not only reason about modal effects on propositions but also about dynamics inside the justifications themselves. We (...) replace this classical boolean base with Gödel logic, one of the three most prominent fuzzy logics, i.e. special instances of many-valued logics, taking values in the unit interval [0, 1], which are intended to model inference under vagueness. We extend the canonical possible-world semantics for justification logic to this fuzzy realm by considering fuzzy accessibility- and evaluation-functions evaluated over the minimum t-norm and establish strong completeness theorems for various fuzzy analogies of prominent extensions for basic justification logic. (shrink)

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.

This is a companion to a paper by the authors entitled “Gödel’s natural deduction,” which presented and made comments about the natural deduction system in Gödel’s unpublished notes for the elementary logic course he gave at the University of Notre Dame in 1939. In that earlier paper, which was itself a companion to a paper that examined the links between some philosophical views ascribed to Gödel and general proof theory, one can find a brief summary of Gödel’s notes for the (...) Notre Dame course. In order to put the earlier paper in proper perspective, a more complete summary of these interesting notes, with comments concerning them, is given here. (shrink)

Coming fromI andCl, i.e. from intuitionistic and classical propositional calculi with the substitution rule postulated, and using the sign to add a new connective there have been considered here: Grzegorozyk's logicGrz, the proof logicG and the proof-intuitionistic logicI set up correspondingly by the calculiFor any calculus we denote by the set of all formulae of the calculus and by the lattice of all logics that are the extensions of the logic of the calculus, i.e. sets of formulae containing the axioms (...) of and closed with respect to its rules of inference. In the logiclG the sign is decoded as follows: A = (A & A). The result of placing in the formulaA before each of its subformula is denoted byTrA. The maps are defined (in the definitions of x and the decoding of is meant), by virtue of which the diagram is constructed. (shrink)

Routley–Meyer semantics (RM-semantics) is defined for Gödel 3-valued logic G3 and some logics related to it among which a paraconsistent one differing only from G3 in the interpretation of negation is to be remarked. The logics are defined in the Hilbert-style way and also by means of proof-theoretical and semantical consequence relations. The RM-semantics is defined upon the models for Routley and Meyer’s basic positive logic B+, the weakest positive RM-semantics. In this way, it is to be expected that the (...) models defined can be adapted to other related many-valued logics. (shrink)

In this paper we consider the modal logic with both $$\Box $$ and $$\Diamond $$ arising from Kripke models with a crisp accessibility and whose propositions are valued over the standard Gödel algebra $$[0,1]_G$$. We provide an axiomatic system extending the one from Caicedo and Rodriguez (J Logic Comput 25(1):37–55, 2015) for models with a valued accessibility with Dunn axiom from positive modal logics, and show it is strongly complete with respect to the intended semantics. The axiomatizations of the most (...) usual frame restrictions are given too. We also prove that in the studied logic it is not possible to get $$\Diamond $$ as an abbreviation of $$\Box $$, nor vice-versa, showing that indeed the axiomatic system we present does not coincide with any of the mono-modal fragments previously axiomatized in the literature. (shrink)

Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Gödel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Gödel logics by Avron. It is shown that the system is sound and complete, and (...) allows cut-elimination. A question by Takano regarding the eliminability of the Takeuti-Titani density rule is answered affirmatively. (shrink)

On the Dummettian understanding, anti-realism regarding a particular discourse amounts to (or at the very least, involves) a refusal to accept the determinacy of the subject matter of that discourse and a corresponding refusal to assert at least some instances of excluded middle (which can be understood as expressing this determinacy of subject matter). In short: one is an anti-realist about a discourse if and only if one accepts intuitionistic logic as correct for that discourse. On careful examination, the strongest (...) Dummettian arguments for anti-realism of this sort fail to secure intuitionistic logic as the single, correct logic for anti-realist discourses. Instead, antirealists are placed in a situation where they fail to be justified in asserting monism (that intuitionistic logic is the unique correct logic). Thus, antirealists seem forced either to accept pluralism (i.e. one or more intermediate logic is at least as `correct’ as intuitionistic logic–an option I take to be unattractive from the anti-realist perspective), or they must be anti-realists about the realism/anti-realism debate (and, in particular, must refuse to assert the instance of excluded middle equivalent to logical monism or logical pluralism). (shrink)

Formal systems of fuzzy logic are well-established logical systems and respected members of the broad family of the so-called substructural logics closely related to the famous logic BCK. The study of fragments of logical systems is an important issue of research in any class of non-classical logics. Here we study the fragments of nine prominent fuzzy logics to all sublanguages containing implication. However, the results achieved in the paper for those nine logics are usually corollaries of theorems with much wider (...) scope of applicability. In particular, we show how many of these fragments are really distinct and we find axiomatic systems for most of them. In fact, we construct strongly separable axiomatic systems for eight of our nine logics. We also fully answer the question for which of the studied fragments the corresponding class of algebras forms a variety. Finally, we solve the problem how to axiomatize predicate versions of logics without the lattice disjunction. (shrink)

A 1-ary sentential context is aggregative (according to a consequence relation) if the result of putting the conjunction of two formulas into the context is a consequence (by that relation) of the results of putting first the one formula and then the other into that context. All 1-ary contexts are aggregative according to the consequence relation of classical propositional logic (though not, for example, according to the consequence relation of intuitionistic propositional logic), and here we explore the extent of this (...) phenomenon, generalized to having arbitrary connectives playing the role of conjunction; among intermediate logics, LC, shows itself to occupy a crucial position in this regard, and to suggest a characterization, applicable to a broader range of consequence relations, in terms of a variant of the notion of idempotence we shall call componentiality. This is an analogue, for the consequence relations of propositional logic, of the notion of a conservative operation in universal algebra. (shrink)

An overview of different versions and applications of Lorenzen’s dialogue game approach to the foundations of logic, here largely restricted to the realm of manyvalued logics, is presented. Among the reviewed concepts and results are Giles’s characterization of Łukasiewicz logic and some of its generalizations to other fuzzy logics, including interval based logics, a parallel version of Lorenzen’s game for intuitionistic logic that is adequate for finite- and infinite-valued Gödel logics, and a truth comparison game for infinite-valued Gödel logic.

The logic RM and its basic fragments (always with implication) are considered here as entire consequence relations, rather than as sets of theorems. A new observation made here is that the disjunction of RM is definable in terms of its other positive propositional connectives, unlike that of R. The basic fragments of RM therefore fall naturally into two classes, according to whether disjunction is or is not definable. In the equivalent quasivariety semantics of these fragments, which consist of subreducts of (...) Sugihara algebras, this corresponds to a distinction between strong and weak congruence properties. The distinction is explored here. A result of Avron is used to provide a local deduction-detachment theorem for the fragments without disjunction. Together with results of Sobociski, Parks and Meyer (which concern theorems only), this leads to axiomatizations of these entire fragments — not merely their theorems. These axiomatizations then form the basis of a proof that all of the basic fragments of RM with implication are finitely axiomatized consequence relations. (shrink)

It was shown recently that epimorphisms need not be surjective in a variety K of Heyting algebras, but only one counter-example was exhibited in the literature until now. Here, a continuum of such examples is identified, viz. the variety generated by the Rieger-Nishimura lattice, and all of its (locally finite) subvarieties that contain the original counter-example K . It is known that, whenever a variety of Heyting algebras has finite depth, then it has surjective epimorphisms. In contrast, we show that (...) for every integer $n \geq 2$ , the variety of all Heyting algebras of width at most n has a non-surjective epimorphism. Within the so-called Kuznetsov-Gerčiu variety (i.e., the variety generated by finite linear sums of one-generated Heyting algebras), we describe exactly the subvarieties that have surjective epimorphisms. This yields new positive examples, and an alternative proof of epimorphism surjectivity for all varieties of Gödel algebras. The results settle natural questions about Beth-style definability for a range of intermediate logics. (shrink)

For the given logical calculus we investigate the proportion of the number of true formulas of a certain length n to the number of all formulas of such length. We are especially interested in asymptotic behavior of this fraction when n tends to infinity. If the limit exists it is represented by a real number between 0 and 1 which we may call the density of truth for the investigated logic. In this paper we apply this approach to the intuitionistic (...) logic of one variable with implication and negation. The result is obtained by reducing the problem to the same one of Dummett's intermediate linear logic of one variable (see [2]). Actually, this paper shows the exact density of intuitionistic logic and demonstrates that it covers a substantial part (more than 93%) of classical prepositional calculus. Despite using strictly mathematical means to solve all discussed problems, this paper in fact, may have a philosophical impact on understanding how much the phenomenon of truth is sporadic or frequent in random mathematics sentences. (shrink)

The Löwenheim-Skolem theorem was published in Skolem's long paper of 1920, with the first section dedicated to the theorem. The second section of the paper contains a proof-theoretical analysis of derivations in lattice theory. The main result, otherwise believed to have been established in the late 1980s, was a polynomial-time decision algorithm for these derivations. Skolem did not develop any notation for the representation of derivations, which makes the proofs of his results hard to follow. Such a formal notation is (...) given here by which these proofs become transparent. A third section of Skolem's paper gives an analysis for derivations in plane projective geometry. To clear a gap in Skolem's result, a new conservativity property is shown for projective geometry, to the effect that a proper use of the axiom that gives the uniqueness of connecting lines and intersection points requires a conclusion with proper cases (logically, a disjunction in a positive part) to be proved. The forgotten parts of Skolem's first paper on the Löwenheim-Skolem theorem are the perhaps earliest combinatorial analyses of formal mathematical proofs, and at least the earliest analyses with profound results. (shrink)

We study the linear Lindenbaum algebra of Basic Propositional Calculus, called linear basic algebra.

In this paper we show that the subvarieties of BL, the variety of BL-algebras, generated by single BL-chains on [0, 1], determined by continous t-norms, are finitely axiomatizable. An algorithm to check the subsethood relation between these subvarieties is provided, as well as another procedure to effectively find the equations of each subvariety. From a logical point of view, the latter corresponds to find the axiomatization of every residuated many-valued calculus defined by a continuous t-norm and its residuum. Actually, the (...) paper proves the results for a more general class than t-norm BL-chains, the so-called regular BL-chains. (shrink)

In the paper we obtain a new characterization of the BCK-algebras which are subdirect product of BCK-chains. We give an axiomatic algebraizable extension of the BCK-calculus, by means of a recursively enumerable set of axioms, such that its equivalent algebraic semantics is definitionally equivalent to the quasivariety of BCK-algebras generated by the BCK-chains. We propose the concept of "linearization of a system" and we give some examples.

In this paper we carry out an algebraic investigation of the weak nilpotent minimum logic and its t-norm based axiomatic extensions. We consider the algebraic counterpart of WNM, the variety of WNM-algebras and prove that it is locally finite, so all its subvarieties are generated by finite chains. We give criteria to compare varieties generated by finite families of WNM-chains, in particular varieties generated by standard WNM-chains, or equivalently t-norm based axiomatic extensions of WNM, and we study their standard completeness (...) properties. We also characterize the generic WNM-chains, i. e. those that generate the variety [MATHEMATICAL DOUBLE-STRUCK CAPITAL W]ℕ[MATHEMATICAL DOUBLE-STRUCK CAPITAL M], and we give finite axiomatizations for some t-norm based extensions of WNM. (shrink)

The Visser rules form a basis of admissibility for the intuitionistic propositional calculus. We show how one can characterize the existence of covers in certain models by means of formulae. Through this characterization, we provide a new proof of the admissibility of a weak form of the Visser rules. Finally, we use this observation, coupled with a description of a generalization of the disjunction property, to provide a basis of admissibility for the intermediate logics BD2 and GSc.

The Komori–Kashima problem, that asks whether the implicational intermediate logics axiomatizable by formulas minimal in classical logic are only intuitionistic logic and classical logic, has stood for over a decade. In this paper, we give a counter-example to this problem. Additionally, we also give some open problems derived from this result.

In this paper we investigate some basic semantic and syntactic conditions characterizing the equivalence connective. In particular we define three basic classes of algebras: the class of weak equivalential algebras, the class of equivalential algebras and the class of regular equivalential algebras.Weak equivalential algebras can be used to study purely equivalential fragments of relevant logics and strict equivalential fragments of some modal logics. Equivalential algebras are suitable to study purely equivalential fragment of BCI and BCK logic. A subclass of the (...) class of regular equivalential algebras is suitable to study equivalential fragments of ukasiewicz logics. Some subvarieties of the class of regular equivalential algebras provide natural semantics for equivalential fragments of the intuitionistic prepositional logic and various intermediate logics. (shrink)

In this article we investigate infinitary propositional logics from the perspective of their completeness properties in abstract algebraic logic. It is well-known that every finitary logic is complete with respect to its relatively subdirectly irreducible models. We identify two syntactical notions formulated in terms of intersection-prime theories that follow from finitarity and are sufficient conditions for the aforementioned completeness properties. We construct all the necessary counterexamples to show that all these properties define pairwise different classes of logics. Consequently, we obtain (...) a new hierarchy of logics going beyond the scope of finitarity. (shrink)

Attention is drawn to the fact that what is alternatively known as Dummett logic, Gödel logic, or Gödel-Dummett logic, was actually introduced by Skolem already in 1913. A related work of 1919 introduces implicative lattices, or Heyting algebras in today's terminology.

I show that the lattice of the positive integers ordered by division is characteristic for Urquhart’s positive semilattice relevance logic; that is, a formula is valid in positive semilattice relevance logic if and only if it is valid in all models over the positive integers ordered by division. I show that the same frame is characteristic for positive intuitionistic logic, where the class of models over it is restricted to those satisfying a heredity condition. The results of this article highlight (...) deep connections between intuitionistic and semilattice relevance logic. (shrink)

This paper aims at being a systematic investigation of different completeness properties of first-order predicate logics with truth-constants based on a large class of left-continuous t-norms . We consider standard semantics over the real unit interval but also we explore alternative semantics based on the rational unit interval and on finite chains. We prove that expansions with truth-constants are conservative and we study their real, rational and finite chain completeness properties. Particularly interesting is the case of considering canonical real and (...) rational semantics provided by the algebras where the truth-constants are interpreted as the numbers they actually name. Finally, we study completeness properties restricted to evaluated formulae of the kind , where φ has no additional truth-constants. (shrink)

In Hájek et al. (J Symb Logic 65(2):669–682, 2000) the authors introduce the concept of supersound logic, proving that first-order Gödel logic enjoys this property, whilst first-order Łukasiewicz and product logics do not; in Hájek and Shepherdson (Ann Pure Appl Logic 109(1–2):65–69, 2001) this result is improved showing that, among the logics given by continuous t-norms, Gödel logic is the only one that is supersound. In this paper we will generalize the previous results. Two conditions will be presented: the first (...) one implies the supersoundness and the second one non-supersoundness. To develop these results we will use, between the other machineries, the techniques of completions of MTL-chains developed in Labuschagne and van Alten (Proceedings of the ninth international conference on intelligent technologies, 2008) and van Alten (2009). We list some of the main results. The first-order versions of MTL, SMTL, IMTL, WNM, NM, RDP are supersound; the first-order version of an axiomatic extension of BL is supersound if and only it is n-potent (i.e. it proves the formula ${\varphi^{n}\,\to\,\varphi^{n\,{+}\,1}}$ for some ${n\,\in\,\mathbb{N}^+}$ ). Concerning the negative results, we have that the first-order versions of ΠMTL, WCMTL and of each non-n-potent axiomatic extension of BL are not supersound. (shrink)

The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic.