We describe a method for obtaining classical logic from intuitionistic logic which does not depend on any proof system, and show that by applying it to the most important implicational relevance logics we get relevance logics with nice semantical and proof-theoretical properties. Semantically all these logics are sound and strongly complete relative to classes of structures in which all elements except one are designated. Proof-theoretically they correspond to cut-free hypersequential Gentzen-type calculi. Another major property of all these logic is that (...) the classical implication can faithfully be translated into them. (shrink)

In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is (...) treated as designated, the above logic is a “common denominator” for Kleene and Łukasiewicz 3-valued logics, which represent its two different “determinizations”. In turn, the weak semantics—where both t and u are treated as designated—represents such a “common denominator” for two major 3-valued paraconsistent logics. We give sound and complete, cut-free sequent calculi for both versions of the logic generated by the rough set Nmatrix. Then we derive from these calculi sequent calculi with the same properties for the various “determinizations” of those two versions of the logic (including Łukasiewicz 3-valued logic). Finally, we show how to embed the four above-mentioned determinizations in extensions of the basic rough set logics obtained by adding to those logics a special two-valued “definedness” or “crispness” operator. (shrink)

Most philosophers take Benacerraf’s argument in ‘What numbers could not be’ to rebut successfully the reductionist view that numbers are sets. This philosophical consensus jars with mathematical practice, in which reductionism continues to thrive. In this note, we develop a new challenge to Benacerraf’s argument by contesting a central premise which is almost unanimously accepted in the literature. Namely, we argue that — contra orthodoxy — there are metaphysically relevant reasons to prefer von Neumann ordinals over other set-theoretic reductions of (...) arithmetic. In doing so, we provide set-theoretical facts which, we believe, are crucial for informed assessment of reductionism. (shrink)

A formula A is said to have the contraction property in a logic L if whenever A, A, Γ ⊨ L B also A, Γ & ; L B. In MLL and in MALL without the additive constants a formula has the contraction property if it is a theorem. Adding the mix rule does not change this fact. In MALL and in affine logic A has the contraction property if either A is provable of A is equivalent to the additive (...) constant 0. We present some general proof-theoretical principles from which all these results easily follow. (shrink)

Hypersequents are finite sets of ordinary sequents. We show that multiple-conclusion sequents and single-conclusion hypersequents represent two different natural methods of switching from a single-conclusion calculus to a multiple-conclusion one. The use of multiple-conclusion sequents corresponds to using a multiplicative disjunction, while the use of single-conclusion hypersequents corresponds to using an additive one. Moreover: each of the two methods is usually based on a different natural semantic idea and accordingly leads to a different class of algebraic structures. In the cases (...) we consider here the use of multiple-conclusion sequents corresponds to focusing the attention on structures in which there is a full symmetry between the sets of designated and antidesignated elements. The use of single-conclusion hypersequents, on the other hand, corresponds to the use of structures in which all elements except one are designated. Not surprisingly, the use of multiple-conclusion hypersequents corresponds to the use of structures which are both symmetrical and with a single nondesignated element. (shrink)

We describe a method for obtaining classical logic from intuitionistic logic which does not depend on any proof system, and show that by applying it to the most important implicational relevance logics we get relevance logics with nice semantical and proof-theoretical properties. Semantically all these logics are sound and strongly complete relative to classes of structures in which all elements except one are designated. Proof-theoretically they correspond to cut-free hypersequential Gentzen-type calculi. Another major property of all these logics is that (...) the classical implication can faithfully be translated into them. (shrink)

We show that the elimination rule for the multiplicative (or intensional) conjunction $\wedge$ is admissible in many important multiplicative substructural logics. These include LL m (the multiplicative fragment of Linear Logic) and RMI m (the system obtained from LL m by adding the contraction axiom and its converse, the mingle axiom.) An exception is R m (the intensional fragment of the relevance logic R, which is LL m together with the contraction axiom). Let SLL m and SR m be, respectively, (...) the systems which are obtained from LL m and R m by adding this rule as a new rule of inference. The set of theorems of SR m is a proper extension of that of R m , but a proper subset of the set of theorems of RMI m . Hence it still has the variable-sharing property. SR m has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLL m relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLL m corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element (in the first case we get the system BCK m , in the second - the system SR m ). Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts. (shrink)

We show that the elimination rule for the multiplicative conjunction $\wedge$ is admissible in many important multiplicative substructural logics. These include LL$_m$ and RMI$_m$ An exception is R$_m$. Let SLL$_m$ and SR$_m$ be, respectively, the systems which are obtained from LL$_m$ and R$_m$ by adding this rule as a new rule of inference. The set of theorems of SR$_m$ is a proper extension of that of R$_m$, but a proper subset of the set of theorems of RMI$_m$. Hence it still (...) has the variable-sharing property. SR$_m$ has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLL$_m$ relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLL$_m$ corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element. Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts. (shrink)

We define in precise terms the basic properties that an ‘ideal propositional paraconsistent logic’ is expected to have, and investigate the relations between them. This leads to a precise characterization of ideal propositional paraconsistent logics. We show that every three-valued paraconsistent logic which is contained in classical logic, and has a proper implication connective, is ideal. Then we show that for every n > 2 there exists an extensive family of ideal n -valued logics, each one of which is not (...) equivalent to any k -valued logic with k < n. (shrink)

This paper has two goals. First, we develop frameworks for logical systems which are able to reflect not only non-monotonic patterns of reasoning, but also paraconsistent reasoning. Our second goal is to have a better understanding of the conditions that a useful relation for nonmonotonic reasoning should satisfy. For this we consider a sequence of generalizations of the pioneering works of Gabbay, Kraus, Lehmann, Magidor and Makinson. These generalizations allow the use of monotonic nonclassical logics as the underlying logic upon (...) which nonmonotonic reasoning may be based. Our sequence of frameworks culminates in what we call plausible, nonmonotonic, multiple-conclusion consequences relations . Our study yields intuitive justifications for conditions that have been proposed in previous frameworks and also clarifies the connections among some of these systems. In addition, we present a general method for constructing plausible nonmonotonic relations. This method is based on a multiple-valued semantics, and on Shoham's idea of preferential models. (shrink)

Zemach's arguments have gone to show that terms might be rigid designators in ordinary language even though they are not natural kind terms. It has been argued that his argument is inconclusive. However it has been claimed that Putnam's argument is much too strong for it would preclude interesting scientific hypotheses about identity between what appear to be different substances, solely on the grounds of modal necessity.It has been shown that rigid designators can be disjunctive but that this possibility is (...) not a foregone conclusion, as Zemach would have us believe. We have to allow for differences between how wesingled out the extension of a natural kind termin the past and how we intend to single out such extensionin the future. Language is not inherently conservative. There is much room for reformist manoevres. *** DIRECT SUPPORT *** A0985038 00002. (shrink)

This study is dedicated to exploring the ways in which Kierkegaard provides a criterion for thinking about the principles of plurality when, in the context of distinguishing between Socrates and Christ, between different conceptions of difference—between those that support the difference of the other and those that do not—he writes that, just as no one must separate what God has joined, so no one must join what God has separated. When Kierkegaard then makes central to faith the incommensurability of single (...) individuals, he indicates that the inviolable singularity of self and other is the one principle that can be true for all—that can be plural—since it is the one principle that is inclusive of all. In my paper I argue through Kierkegaard that the relationship between the singular and the plural embraces the paradox of absolute difference, the paradox of difference as absolute: the single individual exists only by standing in absolute relation to all others as absolute; the plural exists only insofar as it involves the commitment to the singular standard that, as absolute, preserves the difference of all. (shrink)

Through reading Kierkegaard and Derrida together I argue that deconstruction has its historical origin in, and goes no further than, biblical principles. I begin with an analysis of the complexities in Kierkegaard’s exposition of the biblical command to love the neighbor: in showing the command to express the deconstructionof originary presence, Kierkegaard appears to invoke as central to it the apparent binary opposition between divine and human being. I next turn to the Derridean deconstruction of binary opposites and particularly to (...) Derrida’s insistence that deconstruction is justice and that it never proceeds without love. In then engaging Kierkegaard’s critical distinction between ancient Greek and biblical thought, as well as Derrida’s response to issues posed by such a distinction, I show that the deconstruction of Kierkegaard can proceed only on the basis of principles whose origin is biblical and, therefore, that ideas central to Derridean deconstruction, including différance and the supplement, presuppose and express the biblical concept of neighbor. (shrink)

When, in The Gay Science, Nietzsche poses the question of how the natural sciences are possible, he insists that they depend not on a principle that is natural but on the will to truth, the will not to deceive even oneself, with which, he holds, ?we stand on moral ground.? Yet, that the natural sciences stand on ground that is moral also means, for Nietzsche, that their origin is to be located in ?a faith that is thousands of years old,? (...) a faith that, in the Genealogy of Morals, he develops as presupposing what he calls the ascetic ideals of Judaism and Christianity. Further, in holding that the natural sciences have their origin in principles that are biblical, Nietzsche goes on to indicate that, like the natural sciences, his own critical position, unconditionally honest atheism, is, in forbidding itself ?the lie involved in belief in God,? not opposed to, but is rather an expression of, Judaism and Christianity's ascetic ideals. In addressing the interrelationships among the religious, the secular, and the natural sciences in light of Nietzsche, I argue that the natural sciences have their origin in principles that are not natural but that are no less religious than secular. (shrink)

We provide a general investigation of Logic in which the notion of a simple consequence relation is taken to be fundamental. Our notion is more general than the usual one since we give up monotonicity and use multisets rather than sets. We use our notion for characterizing several known logics (including Linear Logic and non-monotonic logics) and for a general, semantics-independent classi cation of standard connectives via equations on consequence relations (these include Girard's \multiplicatives" and \additives"). We next investigate the (...) standard methods for uniformly representing consequence relations: Hilbert type, Natural Deduction and Gentzen type. The advantages and disadvantages of using each system and what should be taken as.. (shrink)

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall investigate (...) the relation between Linear Logic and previously known systems, especially Relevance logics. (shrink)

Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers (...) to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91]). (shrink)

We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ+, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is (...) based on non-deterministic four-valued or three-valued structures, and prove soundness and completeness for all of them. We show that the role of each rule is to reduce the degree of non-determinism in the corresponding systems. We also show that all the systems considered are decidable, and our semantics can be used for the corresponding decision procedures. Most of the extensions of LJ+ (with or without ff) are shown to be conservative over the underlying logic, and it is determined which of them are not. (shrink)

In order to handle inconsistent knowledge bases in a reasonable way, one needs a logic which allows nontrivial inconsistent theories. Logics of this sort are called paraconsistent. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. Da Costa’s approach has led to the family of logics (...) of formal (in)consistency (LFIs). In this paper we provide in a modular way simple non-deterministic semantics for 64 of the most important logics from this family. Our semantics is 3-valued for some of the systems, and infinite-valued for the others. We prove that these results cannot be improved: neither of the systems with a three-valued non-deterministic semantics has either a finite characteristic ordinary matrix or a two-valued characteristic non-deterministic matrix, and neither of the other systems we investigate has a finite characteristic non-deterministic matrix. Still, our semantics provides decision procedures for all the systems investigated, as well as easy proofs of important proof-theoretical properties of them. (shrink)

Non-deterministic matrices are multiple-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options. We consider two different types of semantics which are based on Nmatrices: the dynamic one and the static one . We use the Rasiowa-Sikorski decomposition methodology to get sound and complete proof systems employing finite sets of mv-signed formulas for all propositional logics based on such structures with either of the above (...) types of semantics. Later we demonstrate how these systems can be converted into cut-free ordinary Gentzen calculi which are also sound and complete for the corresponding non-deterministic semantics. As a by-product, we get new semantic characterizations for some well-known logics. (shrink)

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...) unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. (shrink)

We show by way of example how one can provide in a lot of cases simple modular semantics for rules of inference, so that the semantics of a system is obtained by joining the semantics of its rules in the most straightforward way. Our main tool for this task is the use of finite Nmatrices, which are multi-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set (...) of options. The method is applied in the area of logics with a formal consistency operator (known as LFIs), allowing us to provide in a modular way effective, finite semantics for thousands of different LFIs. (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)

The logic $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ was introduced in Robles and Mendéz as a paraconsistent logic which is based on Gödel’s 3-valued matrix, except that Kleene–Łukasiewicz’s negation is added to the language and is used as the main negation connective. We show that $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ is exactly the intersection of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$, the two truth-preserving 3-valued logics which are based on the same truth tables. We then construct a Hilbert-type system which has for $\to $ as its sole rule of inference, and is (...) strongly sound and complete for $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Then we show how, by adding one axiom or one new rule of inference, we get strongly sound and complete systems for $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Finally, we provide quasi-canonical Gentzen-type systems which are sound and complete for those logics and show that they are all analytic, by proving the cut-elimination theorem for them. (shrink)

A logic \ is called self-extensional if it allows to replace occurrences of a formula by occurrences of an \-equivalent one in the context of claims about logical consequence and logical validity. It is known that no three-valued paraconsistent logic which has an implication can be self-extensional. In this paper we show that in contrast, there is exactly one self-extensional three-valued paraconsistent logic in the language of \ for which \ is a disjunction, and \ is a conjunction. We also (...) investigate the main properties of this logic, determine the expressive power of its language, and provide a cut-free Gentzen-type proof system for it. (shrink)

Many efforts have been made in recent years to construct formal systems for mechanizing general mathematical reasoning. Most of these systems are based on logics which are stronger than first-order logic. However, there are good reasons to avoid using full second-order logic for this task. In this work we investigate a logic which is intermediate between FOL and SOL, and seems to be a particularly attractive alternative to both: ancestral logic. This is the logic which is obtained from FOL by (...) augmenting it with the transitive closure operator. While the study of this logic has so far been mostly model-theoretical, this work is devoted to its proof theory. Two natural Gentzen-style proof systems for ancestral logic are presented: one for the reflexive transitive closure, and one for the non-reflexive one. We show that these systems are sound for ancestral logic and provide evidence that they indeed encompass all forms of reasoning for this logic that are used in practice. The two systems are shown to be equivalent by providing translation algorithms between them. We end with an investigation of two main proof-theoretical properties: cut elimination and constructive consistency proof. (shrink)

It is well known that every propositional logic which satisfies certain very natural conditions can be characterized semantically using a multi-valued matrix ([Los and Suszko, 1958; W´ ojcicki, 1988; Urquhart, 2001]). However, there are many important decidable logics whose characteristic matrices necessarily consist of an infinite number of truth values. In such a case it might be quite difficult to find any of these matrices, or to use one when it is found. Even in case a logic does have a (...) finite characteristic matrix it might be difficult to discover this fact, or to find such a matrix. The deep reason for these difficulties is that in an ordinary multi-valued semantics the rules and axioms of a system should be considered as a whole, and there is no method for separately determining the semantic effects of each rule alone. (shrink)

There is a long tradition (See e.g. [9, 10]) starting from [12], according to which the meaning of a connective is determined by the introduction and elimination rules which are associated with it. The supporters of this thesis usually have in mind natural deduction systems of a certain ideal type (explained in Section 3 below). Unfortunately, already the handling of classical negation requires rules which are not of that type. This problem can be solved in the framework of multiple-conclusion Gentzen-type (...) systems (also first introduced in [12]), where instead of introduction and elimination rules there are left introduction rules and right introduction rules. (shrink)

A proof is presented showing that there is no paraconsistent logics with a standard implication which have a three-valued characteristic matrix, and in which the replacement principle holds.

In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) do, but (...) the connections and reasons for preference remain unclear after reading them (at least to the present author, and obviously also the authors of OS], in which a theorem-prover, based exclusively on tableaux, is described). The confusion becomes greater when the reader is introduced to Kowalski's form of a clause ( Ko], Bu]), which is nothing but a Gentzen's sequent of atomic formulae, and when he realizes that resolution is just a form of a Cut, and so that while the elimination of cuts is the principal tool in proof-theory, its use is the main technique in AD! (shrink)

A quasi-canonical Gentzen-type system is a Gentzen-type system in which each logical rule introduces either a formula of the form , or of the form , and all the active formulas of its premises belong to the set . In this paper we investigate quasi-canonical systems in which exactly one of the two classical rules for negation is included, turning the induced logic into either a paraconsistent logic or a paracomplete logic, but not both. We provide a constructive coherence criterion (...) for such systems, and show that a quasi-canonical system of the type we investigate is coherent iff it is strongly paraconsistent or strongly paracomplete (in a sense defined in the paper), iff it has a trivalent, non-deterministic semantics of a special type (also defined in the paper) for which it is sound and complete. Finally, we determine when a system of this sort admits cut-elimination, and provide a simple procedure for transforming one which does not into one which does. (shrink)

A logic \ is called self-extensional if it allows to replace occurrences of a formula by occurrences of an \-equivalent one in the context of claims about logical consequence and logical validity. It is known that no three-valued paraconsistent logic which has an implication can be self-extensional. In this paper we show that in contrast, the famous Dunn–Belnap four-valued logic has exactly one self-extensional four-valued extension which has an implication. We also investigate the main properties of this logic, determine the (...) expressive power of its language, and provide a cut-free Gentzen-type proof system for it. (shrink)

Hermann Weyl was one of the greatest mathematicians of the 20th century, with contributions to many branches of mathematics and physics. In 1918 he wrote a famous book, “Das Kontinuum”, on the foundations of mathematics. In that book he described mathematical analysis as a ‘house built on sand’, and tried to ‘replace this shifting foundation with pillars of enduring strength’. In this paper we reexamine and explain the philosophical and mathematical ideas that underly Weyl’s system in “Das Kontinuum”, and show (...) that they are still useful and relevant. We propose a precise formalization of that system, which is the first to be completely faithful to what is written in the book. Finally, we suggest that a certain set-theoretical modern system reflects better Weyl’s ideas than previous attempts (most notably by Feferman) of achieving this goal. (shrink)

We have avoided here the term \false", since we do not want to commit ourselves to the view that A is false precisely when it is not true. Our formulation of the intuition is therefore obviously circular, but this is unavoidable in intuitive informal characterizations of basic connectives and quanti ers.

We show that the rule that allows the inference of A from A ⊗ B is admissible in many of the basic multiplicative systems. By adding this rule to these systems we get, therefore, conservative extensions in which the tensor behaves as classical conjunction. Among the systems obtained in this way the one derived from RMIm has a particular interest. We show that this system has a simple infinite-valued semantics, relative to which it is strongly complete, and a nice cut-free (...) Gentzen-type formulation which employs hypersequents . Moreover: classical logic has a simple, strong translation into this logic. This translation uses definable connectives and preserves the consequence relation of classical logic . Similar results, but with a 3-valued semantics, obtain if instead of RMIm we use RMm. (shrink)

We suggest a new framework for the Weyl-Feferman predicativist program by constructing a formal predicative set theory P ZF which resembles ZF , and is suitable for mechanization. The basic idea is that the predicatively acceptable instances of the comprehension schema are those which determine the collections they define in an absolute way, independent of the extension of the “surrounding universe”. The language of P ZF is type-free, and it reflects real mathematical practice in making an extensive use of statically (...) defined abstract set terms. Another important feature of P ZF is that its underlying logic is ancestral logic (i.e. the extension of first-order logic with a transitive closure operation). (shrink)

The notion of a bilattice was rst introduced by Ginsburg (see Gin]) as a general framework for a diversity of applications (such as truth maintenance systems, default inferences and others). The notion was further investigated and applied for various purposes by Fitting (see Fi1]- Fi6]). The main idea behind bilattices is to use structures in which there are two (partial) order relations, having di erent interpretations. The two relations should, of course, be connected somehow in order for the mathematical structure (...) to be useful. It is not clear, however, what this connection should be. Ginsberg, for example, has made the connection through an extra operation of negation. Fitting, on the other hand, has investigated connections in the form of conditions on the structure (such as being interlaced { see below). These conditions are independent of the existence, or even the possibility to de ne, operations like Ginsberg's negation.* Fitting de nes, accordingly, notions like \an interlaced bilattice", \a distributive bilattice", \a bilattice with negation" and others. He does not provide, however, any de nition of the notion of bilattice itself (without an extra modi er). I was unable to nd anywhere, in fact, a de nition which will cover all the structures which were called \bilattice" in the literature. (shrink)

We provide a constructive, direct, and simple proof of the completeness of the cut-free part of the hypersequential calculus for G¨odel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions.

We present correct and natural development of fundamental analysis in a predicative set theory we call PZFU\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathsf {PZF}^{\mathsf {U}}}$$\end{document}. This is done by using a delicate and careful choice of those Dedekind cuts that are adopted as real numbers. PZFU\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathsf {PZF}^{\mathsf {U}}}$$\end{document} is based on ancestral logic rather than on first-order logic. Its key feature is that it is definitional in the sense (...) that every object which is shown in it to exist is defined by some closed term of the theory. This allows for a very concrete, computationally-oriented model of it, and makes it very suitable for MKM and ITP. The development of analysis in PZFU\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathsf {PZF}^{\mathsf {U}}}$$\end{document} does not involve coding, and the definitions it provides for the basic notions are the natural ones, almost the same as one can find in any standard analysis book. (shrink)

A canonical Gentzen-type system is a system in which every rule has the subformula property, it introduces exactly one occurrence of a connective, and it imposes no restrictions on the contexts of its applications. A larger class of Gentzen-type systems which is also extensively in use is that of quasi-canonical systems. In such systems a special role is given to a unary connective \ of the language. Accordingly, each application of a logical rule in such systems introduces either a formula (...) of the form \\), or of the form \\), and all the active formulas of its premises belong to the set \. In this paper we investigate the whole class of quasi-canonical systems. We provide a constructive coherence criterion for such systems, and show that a quasi-canonical system is coherent iff it is analytic iff it has a characteristic non-deterministic matrix which is based on some subset of the set of the four truth-values which are used in the famous Dunn–Belnap four-valued matrix for information processing. In addition, we determine when a quasi-canonical system admits cut-elimination. (shrink)

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a (...) non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. (shrink)

A paraconsistent logic is a logic which allows non-trivial inconsistent theories. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. da Costa’s approach has led to the family of Logics of Formal (In)consistency (LFIs). In this paper we provide non-deterministic semantics for a very large family (...) of first-order LFIs (which includes da Costa’s original system.. (shrink)