This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.

This paper investigates (modal) extensions of Heyting-Brouwer logic, i.e., the logic which results when the dual of implication (alias coimplication) is added to the language of intuitionistic logic. We first develop matrix as well as Kripke style semantics for those logics. Then, by extending the Gö;del-embedding of intuitionistic logic into S4, it is shown that all (modal) extensions of Heyting-Brouwer logic can be embedded into tense logics (with additional modal operators). An extension of the Blok-Esakia-Theorem is proved for this embedding.

Two new first-order paraconsistent logics with De Morgan-type negations and co-implication, called symmetric paraconsistent logic (SPL) and dual paraconsistent logic (DPL), are introduced as Gentzen-type sequent calculi. The logic SPL is symmetric in the sense that the rule of contraposition is admissible in cut-free SPL. By using this symmetry property, a simpler cut-free sequent calculus for SPL is obtained. The logic DPL is not symmetric, but it has the duality principle. Simple semantics for SPL and DPL are introduced, and the (...) completeness theorems with respect to these semantics are proved. The cut-elimination theorems for SPL and DPL are proved in two ways: One is a syntactical way which is based on the embedding theorems of SPL and DPL into Gentzen’s LK, and the other is a semantical way which is based on the completeness theorems. (shrink)

In this paper, a way of constructing many-valued paraconsistent logics with weak double negation axioms is proposed. A hierarchy of weak double negation axioms is addressed in this way. The many-valued paraconsistent logics constructed are defined as Gentzen-type sequent calculi. The completeness and cut-elimination theorems for these logics are proved in a uniform way. The logics constructed are also shown to be decidable.

This paper is a reaction to the following remark by grzegorczyk: "the compound sentences are not a product of experiment. they arise from reasoning. this concerns also negations; we see that the lemon is yellow, we do not see that it is not blue." generally, in science the truth is ascertained as indirectly as falsehood. an example: a litmus-paper is used to verify the sentence "the solution is acid." this approach gives rise to a (very intuitionistic indeed) conservative extension of (...) the heyting logic satisfying natural duality laws. (shrink)

One approach to the paradoxes of self-referential languages is to allow some sentences to lack a truth value (or to have more than one). Then assigning truth values where possible becomes a fixpoint construction and, following Kripke, this is usually carried out over a partially ordered family of three-valued truth-value assignments. Some years ago Matt Ginsberg introduced the notion of bilattice, with applications to artificial intelligence in mind. Bilattices generalize the structure Kripke used in a very natural way, while making (...) the mathematical machinery simpler and more perspicuous. In addition, work such as that of Yablo fits naturally into the bilattice setting. What I do here is present the general background of bilattices, discuss why they are natural, and show how fixpoint approaches to truth in languages that allow self-reference can be applied. This is not new work, but rather is a summary of research I have done over many years. (shrink)

This paper sheds light on the relationship between the logic of generalized truth values and the logic of bilattices. It suggests a definite solution to the problem of axiomatizing the truth and falsity consequence relations, \ and \ , considered in a language without implication and determined via the truth and falsity orderings on the trilattice SIXTEEN 3 . The solution is based on the fact that a certain algebra isomorphic to SIXTEEN 3 generates the variety of commutative and distributive (...) bilattices with conflation. (shrink)

In this paper, a family of paraconsistent propositional logics with constructive negation, constructive implication, and constructive co-implication is introduced. Although some fragments of these logics are known from the literature and although these logics emerge quite naturally, it seems that none of them has been considered so far. A relational possible worlds semantics as well as sound and complete display sequent calculi for the logics under consideration are presented.

The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems, which correspond to bilattices in an essential way. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistent data. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. (...) The outcome are paraconsistent logics with a lot of desirable properties.1. (shrink)

In this paper a formalized logic of propositions, PA1, is presented. It is proven consistent and its relationships to traditional logic, to PM ([15]), to subjunctive (including contrary-to-fact) implication and to the “paradoxes” of material and strict implication are developed. Apart from any intrinsic merit it possesses, its chief significance lies in demonstrating the feasibility of a general logic containing theprinciple of subjunctive contrariety, i.e., the principle that ‘Ifpwere true thenqwould be true’ and ‘Ifpwere true thenqwould be false’ are incompatible.

This work treats the problem of axiomatizing the truth and falsity consequence relations, ⊨ t and ⊨ f, determined via truth and falsity orderings on the trilattice SIXTEEN 3 (Shramko and Wansing, 2005). The approach is based on a representation of SIXTEEN 3 as a twist-structure over the two-element Boolean algebra.

The book presents a thoroughly elaborated logical theory of generalized truth-values understood as subsets of some established set of truth values. After elucidating the importance of the very notion of a truth value in logic and philosophy, we examine some possible ways of generalizing this notion. The useful four-valued logic of first-degree entailment by Nuel Belnap and the notion of a bilattice constitute the basis for further generalizations. By doing so we elaborate the idea of a multilattice, and most notably, (...) a trilattice of truth values – a specific algebraic structure with information ordering and two distinct logical orderings, one for truth and another for falsity. Each logical order not only induces its own logical vocabulary, but determines also its own entailment relation. We consider both semantic and syntactic ways of formalizing these relations and construct various logical calculi. (shrink)

In Belnap's useful 4-valued logic, the set 2 = {T, F} of classical truth values is generalized to the set 4 = ������(2) = {Ø, {T}, {F}, {T, F}}. In the present paper, we argue in favor of extending this process to the set 16 = ᵍ (4) (and beyond). It turns out that this generalization is well-motivated and leads from the bilattice FOUR₂ with an information and a truth-and-falsity ordering to another algebraic structure, namely the trilattice SIXTEEN₃ with an (...) information ordering together with a truth ordering and a (distinct) falsity ordering. Interestingly, the logics generated separately by the algebraic operations under the truth order and under the falsity order in SIXTEEN₃ coincide with the logic of FOUR₂, namely first degree entailment. This observation may be taken as a further indication of the significance of first degree entailment. In the present setting, however, it becomes rather natural to consider also logical systems in the language obtained by combining the vocabulary of the logic of the truth order and the falsity order. We semantically define the logics of the two orderings in the extended language and in both cases axiomatize a certain fragment comprising three unary operations: a negation, an involution, and their combination. We also suggest two other definitions of logics in the full language, including a bi-consequence system. In other words, in addition to presenting first degree entailment as a useful 16-valued logic, we define further useful 16-valued logics for reasoning about truth and (non-)falsity. We expect these logics to be an interesting and useful instrument in information processing, especially when we deal with a net of hierarchically interconnected computers. We also briefly discuss Arieli's and Avron's notion of a logical bilattice and state a number of open problems for future research. (shrink)

The paper is a continuation of A deductive-reductive form oflogic: general theory and intuitionistic case and considers the problem of definability of modal operators on the intuitionistic base. Contrary tothe classical case, it seems that the fact whether the connective is Heyting’sor Brouwerian is essential for the intuitionistic logic. The connective of possibility has the classical interpretation, i.e. w |= ✸α iff ∃t, if it is defined on the base of the logicwith Brouwerian connective of coimplication.

This work treats the problem of axiomatizing the truth and falsity consequence relations, $ \vDash _t $ and $ \vDash _f $, determined via truth and falsity orderings on the trilattice SIXTEEN₃. The approach is based on a representation of SIXTEEN₃ as a twist-structure over the two-element Boolean algebra.