Sections 1, 2 and 3 contain the main result, the strong finite axiomatizability of all 2-valued matrices. Since non-strongly finitely axiomatizable 3-element matrices are easily constructed the result reveals once again the gap between 2-valued and multiple-valued logic. Sec. 2 deals with the basic cases which include the important F i from Post's classification. The procedure in Sec. 3 reduces the general problem to these cases. Sec. 4 is a study of basic algebraic properties of 2-element algebras. In particular, we (...) show that equational completeness is equivalent to the Stone-property and that each 2-element algebra generates a minimal quasivariety. The results of Sec. 4 will be applied in Sec. 5 to maximality questions and to a matrix free characterization of 2-valued consequences in the lattice of structural consequences in any language. Sec. 6 takes a look at related axiomatization. problems for finite algebras and matrices. We study the notion of a propositional consequence with equality and, among other things, present explicit axiomatizations of 2-valued consequences with equality. (shrink)

In Section 1 we show that the De Morgan type rules (= sequential rules in L(, ) which remain correct if and are interchanged) are finitely based. Section 2 contains a similar result for L(). These results are essentially based on special properties of some equational theories.

Matthew Spinks [35] introduces implicative BCSK-algebras, expanding implicative BCK-algebras with an additional binary operation. Subdirectly irreducible implicative BCSK-algebras can be viewed as flat posets with two operations coinciding only in the 1- and 2-element cases, each, in the latter case, giving the two-valued implication truth-function. We introduce the resulting logic (for the general case) in terms of matrix methodology in §1, showing how to reformulate the matrix semantics as a Kripke-style possible worlds semantics, thereby displaying the distinction between the two (...) implications in the more familiar language of modal logic. In §§2 and 3 we study, from this perspective, the fragments obtained by taking the two implications separately, and – after a digression (in §4) on the intuitionistic analogue of the material in §3 – consider them together in §5, closing with a discussion in §6 of issues in the theory of logical rules. Some material is treated in three appendices to prevent §§1–6 from becoming overly distended. (shrink)

We recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 we (...) show that for the pure logic of one of these implicational connectives two-in general distinct-consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the 'propositional operations' associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives. (shrink)

Die vorliegenden Untersuchungen haben sich aus solchen entwickelt, die ich an andrer Stelle früher veröffentlichte. Die Kenntnis dieser früheren Arbeit wird in keiner Weise hier vorausgesetzt und ist für das folgende unwesentlich. Es sei mir jedoch gestattet, für den Kenner der früheren Arbeit einige Bemerkungen voraufzuschicken. In der genannten Arbeit hatte ich, angeregt ursprünglich durch Gedankengänge von Herrn Behmann, ein typenfreies System der Logik aufgebaut, das allein auf dem Gedanken fußte, daß der Definitionsbereich der Prädikate im allgemeinen beschränkt ist, sodaß (...) nur bestimmte Zusammenstellungen von Prädikaten und Dingen sinnvolle, d.h. wahre oder falsche Aussagen ergeben, und das diesen Gesichtspunkt meiner Meinung nach konsequent durchführte. Eine anschließende Arbeit sollte dann die Widerspruchsfreiheit des Systems untersuchen. Diese Untersuchung ist inzwischen geschehen. Es zeigte sich, daß sich die Widerspruchsfreiheit des Systems nur dann beweisen ließ, falls die in ihm enthaltene Vollständigkeit von → die sich durch das Bestehen eines Deduktionstheorems zeigte, fallen gelassen wurde. Die Grundformeln (13) und (14) mußten wegbleiben. Die Widerspruchsfreiheit des restlichen Systems ließ sich dann durch eine dem System eigentümliche Methode der Beweistransformation zeigen.Diese anschließienden Untersuchungen, die ihrer Zeit nicht mehr veröffentlicht werden konnten, sind inzwischen durch die vorliegenden überholt. Es war das Unbefriedigende bei dem genannten Aufbau, daß hinterher doch wieder eine Einschränkung gemacht werden mußte, die sich nicht aus den zugrunde gelegten Prinzipien ergab, sondern von ihnen aus unvorhergesehen war. Diese Einschränkung bewirkte übrigens, daß keine volle Zahlentheorie in dem System zu gewinnen war. (shrink)

Reviewed Works:Gaisi Takeuti, Proof Theory.Georg Kreisel, Proof Theory: Some Personal Recollections.Wolfram Pohlers, Contributions of the Schutte School in Munich to Proof Theory.Stephen G. Simpson, Subsystems of $\mathbf{Z}_2$ and Reverse Mathematics.Solomon Feferman, Proof Theory: A Personal Report.

The framework of natural deduction is extended by permitting rules as assumptions which may be discharged in the course of a derivation. this leads to the concept of rules of higher levels and to a general schema for introduction and elimination rules for arbitrary n-ary sentential operators. with respect to this schema, (functional) completeness "or", "if..then" and absurdity is proved.

Let V be a s.f.b. (strongly finitely based, see below) variety of algebras. The central result is Theorem 2 saying that the logic defined by all matrices (A, d) with d A V is finitely based iff the A V have 1st order definable cosets for their congruences. Theorem 3 states a similar axiomatization criterion for the logic determined by all matrices (A, A), A V, a term which is constant in V. Applications are given in a series of examples.

We recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 we (...) show that for the pure logic of one of these implicational connectives two – in general distinct – consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the ‘propositional operations’ associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives. (shrink)

W. J. Blok and Don Pigozzi set out to try to answer the question of what it means for a logic to have algebraic semantics. In this seminal book they transformed the study of algebraic logic by giving a general framework for the study of logics by algebraic means. The Dutch mathematician W. J. Blok (1947-2003) received his doctorate from the University of Amsterdam in 1979 and was Professor of Mathematics at the University of Illinois, Chicago until his death in (...) an automobile accident. Don Pigozzi (1935- ) grew up in Oakland, California, received his doctorate from the University of California, Berkeley in 1970, and was Professor of Mathematics at Iowa State University until his retirement in 2002. The Advanced Reasoning Forum is pleased to make available in its Classic Reprints series this exact reproduction of the 1989 text, with a new errata sheet prepared by Don Pigozzi. (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 provide five semantic preservation properties which apply to the various rules -- primitive, derived and admissible -- of Hilbert-style axiomatizations of relevant logics. These preservation properties are with respect to the Routley-Meyer semantics, and consist of various truth- preservations and validity-preservations from the premises to the conclusions of these rules. We establish some deduction theorems, some persistence theorems and some soundness and completeness theorems, for these preservation properties. We then apply the above ideas, as best we can, to the (...) classical sentential and predicate calculi, to normal and non- normal modal logics, and to many- valued logics. (shrink)

Die vorliegenden Untersuchungen haben sich aus solchen entwickelt, die ich an andrer Stelle früher veröffentlichte. Die Kenntnis dieser früheren Arbeit wird in keiner Weise hier vorausgesetzt und ist für das folgende unwesentlich. Es sei mir jedoch gestattet, für den Kenner der früheren Arbeit einige Bemerkungen voraufzuschicken. In der genannten Arbeit hatte ich, angeregt ursprünglich durch Gedankengänge von Herrn Behmann, ein typenfreies System der Logik aufgebaut, das allein auf dem Gedanken fußte, daß der Definitionsbereich der Prädikate im allgemeinen beschränkt ist, sodaß (...) nur bestimmte Zusammenstellungen von Prädikaten und Dingen sinnvolle, d.h. wahre oder falsche Aussagen ergeben, und das diesen Gesichtspunkt meiner Meinung nach konsequent durchführte. Eine anschließende Arbeit sollte dann die Widerspruchsfreiheit des Systems untersuchen. Diese Untersuchung ist inzwischen geschehen. Es zeigte sich, daß sich die Widerspruchsfreiheit des Systems nur dann beweisen ließ, falls die in ihm enthaltene Vollständigkeit von → die sich durch das Bestehen eines Deduktionstheorems zeigte, fallen gelassen wurde. Die Grundformeln (13) und (14) mußten wegbleiben. Die Widerspruchsfreiheit des restlichen Systems ließ sich dann durch eine dem System eigentümliche Methode der Beweistransformation zeigen.Diese anschließienden Untersuchungen, die ihrer Zeit nicht mehr veröffentlicht werden konnten, sind inzwischen durch die vorliegenden überholt. Es war das Unbefriedigende bei dem genannten Aufbau, daß hinterher doch wieder eine Einschränkung gemacht werden mußte, die sich nicht aus den zugrunde gelegten Prinzipien ergab, sondern von ihnen aus unvorhergesehen war. Diese Einschränkung bewirkte übrigens, daß keine volle Zahlentheorie in dem System zu gewinnen war. (shrink)

We define a property for varieties V, the f.r.p. . If it applies to a finitely based V then V is strongly finitely based in the sense of [14], see Theorem 2. Moreover, we obtain finite axiomatizability results for certain propositional logics associated with V, in its generality comparable to well-known finite base results from equational logic. Theorem 3 states that each variety generated by a 2-element algebra has the f.r.p. Essentially this implies finite axiomatizability of a 2-valued logic in (...) any finite language. (shrink)