A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite -valued logic if the labels are interpreted as sets of truth values. Furthermore, it is shown that any finite -valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of (...) labels needed is logarithmic in the number of truth values, and it is shown that this bound is tight. (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)

The problem of approximating a propositional calculus is to find many-valued logics which are sound for the calculus (i.e., all theorems of the calculus are tautologies) with as few tautologies as possible. This has potential applications for representing (computationally complex) logics used in AI by (computationally easy) many-valued logics. It is investigated how far this method can be carried using (1) one or (2) an infinite sequence of many-valued logics. It is shown that the optimal candidate matrices (...) for (1) can be computed from the calculus. (shrink)

A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.

Propositional logics in general, considered as a set of sentences, can be undecidable even if they have “nice” representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple—at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics (...) represented in various ways can be approximated by finite-valued logics. It is shown that the minimal m-valued logic for which a given calculus is strongly sound can be calculated. It is also investigated under which conditions propositional logics can be characterized as the intersection of (effectively given) sequences of finite-valued logics. (shrink)

In this paper, we study multiplicative extensions of propositional many-place sequent calculi for finitely-valued logics arising from those introduced in Sect. 5 of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) through their translation by means of singularity determinants for logics and restriction of the original many-place sequent language. Our generalized approach, first of all, covers, on a uniform formal basis, both the one developed in Sect. 5 of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, (...) 2004) for singular finitely-valued logics (when singularity determinants consist of a variable alone) and conventional Gentzen-style (i.e., two-place sequent) calculi suggested in Pynko (Bull Sect Logic 33(1):23–32, 2004) for finitely-valued logics with equality determinant. In addition, it provides a universal method of constructing Tait-style (i.e., one-place sequent) calculi for finitely-valued logics with singularity determinant (in particular, for Łukasiewicz finitely-valued logics) that fits the well-known Tait calculus (Lecture Notes in Mathematics, Springer, Berlin, 1968) for the classical logic. We properly extend main results of Pynko (J Multiple-Valued Logic Soft Comput 10:339–362, 2004) and explore calculi under consideration within the framework of Sect. 7 of Pynko (Arch Math Logic 45:267–305, 2006), generalizing the results obtained in Sect. 7.5 of Pynko (Arch Math Logic 45:267–305 2006) for two-place sequent calculi associated with finitely-valued logics with equality determinant according to Pynko (Bull Sect Logic 33(1):23–32, 2004). We also exemplify our universal elaboration by applying it to some denumerable families of well-known finitely-valued logics. (shrink)

In this paper we describe, in a purely algebraic language, truth-complete finite-valued propositional logical calculi extending the classical Boolean calculus. We also give a new proof of the Completeness Theorem for such calculi. We investigate the quasi-varieties of algebras playing an analogous role in the theory of these finite-valued logics to the role played by the variety of Boolean algebras in classical logic.

The primary objective of this paper, which is an addendum to the author’s [8], is to apply the general study of the latter to Łukasiewicz’s n-valued logics [4]. The paper provides an analytical expression of a 2(n−1)-place sequent calculus (in the sense of [10, 9]) with the cut-elimination property and a strong completeness with respect to the logic involved which is most compact among similar calculi in the sense of a complexity of systems of premises of introduction rules. (...) This together with a quite effective procedure of construction of an equality determinant (in the sense of [5]) for the logics involved to be extracted from the constructive proof of Proposition 6.10 of [6] yields an equally effective procedure of construction of both Gentzen-style [2] (i.e., 2-place) and Tait-style [11] (i.e., 1-place) minimal sequent calculi following the method of translations described in Subsection 4.2 of [7]. (shrink)

In this paper we present a method to reduce the decision problem of several infinite-valued propositional logics to their finite-valued counterparts. We apply our method to Łukasiewicz, Gödel and Product logics and to some of their combinations. As a byproduct we define sequent calculi for all these infinite-valued logics and we give an alternative proof that their tautology problems are in co-NP.

When considering m-sequents, it is always possible to obtain an m-sequent calculus VL for every m-valued logic (defined from an arbitrary finite algebra L of cardinality m) following for instance the works of the Vienna Group for Multiple-valued Logics. The Gentzen relations associated with the calculi VL are always finitely equivalential but might not be algebraizable. In this paper we associate an algebraizable 2-Gentzen relation with every sequent calculus VL in a uniform way, provided the original (...) algebra L has a reduct that is a distributive lattice or a pseudocomplemented distributive lattice. We also show that the sentential logic naturally associated with the provable sequents of this algebraizable Gentzen relation is the logic that preserves degrees of truth with respect to the original algebra (in contrast with the more common logic that merely preserves truth). Finally, for some particular logics we obtain 2-sequent calculi that axiomatize the algebraizable Gentzen relations obtained so far. (shrink)

. The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have designated values or not. The transformation preserves (...) the general structure of proofs in the original calculus in a way ensuring preservation of the weak cut elimination theorem under the transformation. The described transformation metod is illustrated on several concrete examples of many-valued logics, including a new application to information sources logics. (shrink)

A method of developing a relational semantics and relational proof systems for many-valued logics based on finite algebras of truth values is presented. The method is applied to Rosser-Turquette logic, logics based on symmetric Heyting algebras with operators and a Post-style logic.

This is the preface for a special volume published by the Journal of Applied Non-Classical Logics Volume 9, Issue 1, 1999.

his paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way. We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Lowenheim-Skolem theorem. The paper is completely self-contained and includes examples of application (...) to particular many-valued formal systems. (shrink)

A rejection system, also referred to as a complementary calculus, is a proof system axiomatising the invalid formulas of a logic, in contrast to traditional calculi which axiomatise the valid ones. Rejection systems therefore introduce a purely syntactic way of determining non-validity without having to consider countermodels, which can be useful in procedures for automated deduction and proof search. Rejection calculi have first been formally introduced by Łukasiewicz in the context of Aristotelian syllogistic and subsequently rejection systems for many (...) well-known logics have been proposed. In this paper, we deal with rejection systems for so-called non-deterministic finite-valued logics, a special case of non-deterministic many-valued logics which were introduced by Avron and Lev as a generalisation of traditional many-valued logics. More specifically, we introduce a systematic method for constructing sequent-style rejection systems for any given non-deterministic finite-valued logic. Furthermore, as special instances of our method, we provide concrete calculi for specific paraconsistent logics which can be characterised in terms of non-deterministic two- and three-valued semantics, respectively. (shrink)

The article deals with finding finite total equivalence systems for formulas based on an arbitrary closed class of functions of several variables defined on the set {0, 1, 2} and taking values in the set {0,1} with the property that the restrictions of its functions to the set {0, 1} constitutes a closed class of Boolean functions. We consider all classes whose restriction closure is either the set of all functions of two-valued logic or the set T (...) a of functions preserving \. In each of these cases, we find a finite total equivalence system, construct a canonical type for formulas, and present a complete algorithm for determining whether any two formulas are equivalent. (shrink)

We argue that the simplicity condition on a probability function on sentences of a predicate language L that it takes only finitely many values on the sentences of any finite sublanguage of L can be viewed as rational. We then go on to investigate consequences of this condition, linking it to the model theoretic notion of quantifier elimination.

The article explores the following question: which among the most often examined in the literature method of constructing Hilbert-type axiom systems for finite-valued propositional logics of Łukasi...

A proof-theoretical analysis of finite-valuedness in the domain of cumulative inference systems is presented.

In the monograph [1] of Chang and Keisler, a considerable extent of model theory of the first order continuous logic is ingeniously developed without using any notion of provability.In this paper we shall define the notion of provability in continuous logic as well as the notion of matrix, which is a natural extension of one in finite-valued logic in [2], and develop the syntax and semantics of it mostly along the line in the preceding paper (...) [2]. Fundamental theorems of model theory in continuous logic, which have been proved with purely model-theoretic proofs in [1], will be proved with proofs which are natural extensions of those in two-valued logic. (shrink)

In this paper the completeness theorems for the finite-valued ukasiewicz logics are proved with the use of the Lindenbaum algebra.

In this paper we deepen Mundici's analysis on reducibility of the decision problem from infinite-valued ukasiewicz logic to a suitable m-valued ukasiewicz logic m , where m only depends on the length of the formulas to be proved. Using geometrical arguments we find a better upper bound for the least integer m such that a formula is valid in if and only if it is also valid in m. We also reduce the notion of logical consequence (...) in to the same notion in a suitable finite set of finite-valued ukasiewicz logics. Finally, we define an analytic and internal sequent calculus for infinite-valued ukasiewicz logic. (shrink)

The roots of the Lvov-Warsaw School can be traced back to Aristotle himself. But in later times we better put them into thinking GW Leibniz and who somehow inherited many of these ways of thinking, such as the philosopher and mathematician Bernhard Bolzano. Since he would pass the key figure of Franz Brentano, who had as one of his disciples to Kazimierz Twardowski, which starts with the brilliant Polish school of mathematics and philosophy dealt with. Among them, one of the (...) most interesting thinkers must be Jan Lukasiewicz, the father of many-valued logic.Jan Łukasiewicz began teaching at the University of Lvov, and then at Warsaw, but after World War II must to continue in Dublin. Some questions may be very astonishing in the CV of Łukasiewicz. For instance, that a firstly Polish Minister of Education in Paderewski cabinet, into the new Polish Republic, and also Rector for two times at Warsaw University, was awarded with a Doctorate ‘Honoris Causa’ in spring 1936, at University of Münster, into the maximum of effervescency of Nazism in Germany. The explanation must be their good relation with a very good friend, the former theologian, and then logician, Heinrich Schölz, who was the first Chairman of Mathematical Logic in German universities.Łukasiewicz firstly studied Law, and then Mathematics and Philosophy in Lvov. His doctoral supervisor was Kazimierz Twardowski, and in 1902 he obtain his Ph. D. title with a very special mention: ‘sub auspiciis Imperatoris’. Also he received a doctorate ring with diamonds from the Kaiser of the Austro-Hungarian Empire, Franz Joseph I.From 1902, Łukasiewicz was employed as a private teacher, and also as a desk in the Universitary Library of Lvov. So it was until 1904 when he obtained a scholarship to study abroad. He defends his ‘Habilitationschrift’ in 1906, entitled “Analysis and construction of the concept of cause”. This permits to give university courses. His first lectures were on the Algebra of Logic, according to the recent translation to Polish of this book of the French logician Louis Couturat.Between 1902 and 1906, Lukasiewicz continued his studies in the universities of Berlin and Leuwen. In 1906, by his ‘Habilitationschrift’, he obtain the qualification as university professor at Lvov. And the, in 1911, he was appointed as associate professor in his ‘alma mater’.Jan Łukasiewicz was also very active in historical research on logic, giving a new and up-to-date interpretation of Aristotle’s syllogism and of the Stoics’ propositional calculus. According to Scholz, the better pages on history of logic are due to him. And also, as Arianna Betti says, “Jan Lukasiewicz is first and foremost associated with the rejection of the Principle of Bivalence and the discovery of Many-Valued Logic.”The discovery of MVL by Lukasiewicz was in 1918, a little earlier than Emil Leon Post. According to Jan Wolenski, “although Post’s remarks were parenthetical and extremely condensed, Lukasiewicz explained his intuitions and motivations carefully and at length. He was guided by considerations about future contingents and the concept of possibility”. So, he introduces, firstly, three-valued logic, then four-valued logic, generalized to logics with an arbitrary finite number of veritative values, and finally, to logics with a countably infinite-valued number of such values.Very noteworthy is his treatment of the history of logic in the light of the new formal logic. Thus, not only he addressed the issue of future contingents departing from Aristotle, but also put in value logic of the Stoics, at least so far taken. In fact, Heinrich Scholz said, rightly, that Lukasiewicz had written the most lucid pages on the history of logic. (shrink)

The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of (...) a truth value and the exclusion of the opposite truth value describe the same situation.). (shrink)

Automated reasoning issues are addressed for a finite lattice-valued propositional logic LnP(X) with truth-values in a finite lattice-valued logical algebraic structure—lattice implication algebra. We investigate extended strategies and rules from classical logic to LnP(X) to simplify the procedure in the semantic level for testing the satisfiability of formulas in LnP(X) at a certain truth-value level α (α-satisfiability) while keeping the role of truth constant formula played in LnP(X). We propose a lock resolution method at (...) a certain truth-value level α (α-lock resolution) in LnP(X) and have proved its theorems of soundness and weak completeness, respectively. We provide more efficient resolution based automated reasoning in LnP(X) and key supports for α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic. (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. (shrink)

We show that the complete first order theory of an MV algebra has equation image countable models unless the MV algebra is finitely valued. So, Vaught's Conjecture holds for all MV algebras except, possibly, for finitely valued ones. Additionally, we show that the complete theories of finitely valued MV algebras are equation image and that all ω-categorical complete theories of MV algebras are finitely axiomatizable and decidable. As a final result we prove that the free algebra on (...) countably many generators of any locally finite variety of MV algebras is ω-categorical. (shrink)

We study structural rules in the context of multi-valued logics with finitely-many truth-values. We first extend Gentzen’s traditional structural rules to a multi-valued logic context; in addition, we propos some novel structural rules, fitting only multi-valued logics. Then, we propose a novel definition, namely, structural rules completeness of a collection of structural rules, requiring derivability of the restriction of consequence to atomic formulas by structural rules only. The restriction to atomic formulas relieves the need to concern (...) logical rules in the derivation. (shrink)

In this note we prove that some familiar systems of finitely many-valued logics havefactor semantics, and establish necessary conditions for a system of many-valued logic having semantics of this kind.

This paper investigates a problem related to quantifiers which has some analogies to that of propositional completeness I give a definition of quantifier in many-valued logics generalizing the cases which already occur in first order many- valued logics. Though other definitions are possible, this particular one, which I call distribution quantifiers, generalizes the classical quantifiers in a very natural way, and occurs in finite numbers in every m-valued logic. We then call the problem of quantificationa2 (...) completeness in m-valued logic the problem of characterizing which are the quantifiers in a given language which can generate all other quantifiers in this language, using the connectives, as is the case, for example, of the universal and exis- tential quantifiers in classical logic, using negation. We are interested, in particular, in those many-valued quantifiers which closely mimic the behavior of existential an universal quantifiers in generating all other quantifiers using negation: these I call perfect quantifiers, as defined below. The main result of this paper is the characterization of all perfect quantifiers in 3-valued logics, which are complete if the logic is functionally complete. As a byproduct, we obtain the same result for the classical logic, which we include mainly for motivation. (shrink)

The closed world assumption plays a fundamental role in the theory of deductive databases. On the other hand, multi-valued logics occupy a vast field in non-classical logics. Some questions are better explained and expressed in terms of such logics. To enhance the expressive power and the declarative ability of a deductive database, we extend various CWA formalizations, including the naive CWA, the generalized CWA and the careful CWA, to multi-valued logics. The basic idea is to embed logic (...) formulae into some polynomial ring. The extensions can be applied in a uniform manner to any finitely multi-valued logics. Therefore they have also computational interest. (shrink)

In many-valued logic the decision of functional completeness is a basic and important problem, and the thorough solution to this problem depends on determining all maximal closed sets in the set of many-valued logic functions. It includes three famous problems, i.e., to determine all maximal closed sets in the set of the total, of the partial and of the unary many-valued logic functions, respectively. The first two problems have been completely solved , and the (...) solution to the third problem boils down to determining all maximal subgroups in the k-degree symmetric group Sk, which is an open problem in the finite group theory. In this paper, all maximal closed sets in the set of unary p-valued logic functions are determined, where p is a prime. (shrink)

We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation (...) theorem for finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers. (shrink)

We present a method that generates two-sided sequent calculi for four-valued logics like "first degree entailment" (FDE). (We say that a logic is FDE-like if it has finitely many operators of finite arity, including negation, and if all of its operators are truth-functional over the four truth-values 'none', 'false', 'true', and 'both', where 'true' and 'both' are designated.) First, we show that for every n-ary operator * every truth table entry f*(x1,...,xn) = y can be characterized in (...) terms of a pair of sequent rules. Secondly, we use these sequent rules to build sequent calculi and prove their completeness. With the help of two simplification procedures we then show that the 2⋅4^n sequent rules that characterize an n-ary operator can be systematically reduced to at most four sequent rules. Thirdly, we use our method to investigate the proof-theoretical consequences of including intuitive truth-functional implications in FDE-like logics. (shrink)