The notion of an algebraic semantics of a deductive system was proposed in [3], and a preliminary study was begun. The focus of [3] was the definition and investigation of algebraizable deductive systems, i.e., the deductive systems that possess an equivalent algebraic semantics. The present paper explores the more general property of possessing an algebraic semantics. While a deductive system can have at most one equivalent algebraic semantics, it may have numerous different algebraic (...) semantics. All of these give rise to an algebraic completeness theorem for the deductive system, but their algebraic properties, unlike those of equivalent algebraic semantics, need not reflect the metalogical properties of the deductive system. Many deductive systems that don't have an equivalent algebraic semantics do possess an algebraic semantics; examples of these phenomena are provided. It is shown that all extensions of a deductive system that possesses an algebraic semantics themselves possess an algebraic semantics. Necessary conditions for the existence of an algebraic semantics are given, and an example of a protoalgebraic deductive system that does not have an algebraic semantics is provided. The mono-unary deductive systems possessing an algebraic semantics are characterized. Finally, weak conditions on a deductive system are formulated that guarantee the existence of an algebraic semantics. These conditions are used to show that various classes of non-algebraizable deductive systems of modal logic, relevance logic and linear logic do possess an algebraic semantics. (shrink)

The notion of an algebraic semantics of a deductive system was proposed in [3], and a preliminary study was begun. The focus of [3] was the definition and investigation of algebraizable deductive systems, i.e., the deductive systems that possess an equivalent algebraic semantics. The present paper explores the more general property of possessing an algebraic semantics. While a deductive system can have at most one equivalent algebraic semantics, it may have numerous different algebraic (...) semantics. All of these give rise to an algebraic completeness theorem for the deductive system, but their algebraic properties, unlike those of equivalent algebraic semantics, need not reflect the metalogical properties of the deductive system. Many deductive systems that don't have an equivalent algebraic semantics do possess an algebraic semantics; examples of these phenomena are provided. It is shown that all extensions of a deductive system that possesses an algebraic semantics themselves possess an algebraic semantics. Necessary conditions for the existence of an algebraic semantics are given, and an example of a protoalgebraic deductive system that does not have an algebraic semantics is provided. The mono-unary deductive systems possessing an algebraic semantics are characterized. Finally, weak conditions on a deductive system are formulated that guarantee the existence of an algebraic semantics. These conditions are used to show that various classes of non-algebraizable deductive systems of modal logic, relevance logic and linear logic do possess an algebraic semantics. (shrink)

In this paper we consider the structure of the class FGModS of full generalized models of a deductive system S from a universal-algebraic point of view, and the structure of the set of all the full generalized models of S on a fixed algebra A from the lattice-theoretical point of view; this set is represented by the lattice FACSs A of all algebraic closed-set systems C on A such that (A, C) ε FGModS. We relate some properties of (...) these structures with tipically logical properties of the sentential logic S. The main algebraic properties we consider are the closure of FGModS under substructures and under reduced products, and the property that for any A the lattice FACSs A is a complete sublattice of the lattice of all algebraic closed-set systems over A. The logical properties are the existence of a fully adequate Gentzen system for S, the Local Deduction Theorem and the Deduction Theorem for S. Some of the results are established for arbitrary deductive systems, while some are found to hold only for deductive systems in more restricted classes like the protoalgebraic or the weakly algebraizable ones. The paper ends with a section on examples and counterexamples. (shrink)

The best known algebraizable logics with a conjunction and an implication have the property that the conjunction defines a meet semi-lattice in the algebras of their algebraic counterpart. This property makes it possible to associate with them a semi-lattice based deductive system as a companion. Moreover, the order of the semi-lattice is also definable using the implication. This makes that the connection between the properties of the logic and the properties of its semi-lattice based companion is strong. We (...) introduce a class of algebraizable deductive systems that includes those systems, and study some of their properties and of their semi-lattice based companions. We also study conditions which, when satisfied by a deductive system in the class, imply that it is strongly algebraizable. This brings some information on the open area of research of Abstract Algebraic Logic which consists in finding interesting characterizations of classes of algebraizable logics that are strongly algebraizable. (shrink)

Logics that do not have a deduction-detachment theorem (briefly, a DDT) may still possess a contextual DDT —a syntactic notion introduced here for arbitrary deductive systems, along with a local variant. Substructural logics without sentential constants are natural witnesses to these phenomena. In the presence of a contextual DDT, we can still upgrade many weak completeness results to strong ones, e.g., the finite model property implies the strong finite model property. It turns out that a finitary system has (...) a contextual DDT iff it is protoalgebraic and gives rise to a dually Brouwerian semilattice of compact deductive filters in every finitely generated algebra of the corresponding type. Any such system is filter distributive, although it may lack the filter extension property. More generally, filter distributivity and modularity are characterized for all finitary systems with a local contextual DDT, and several examples are discussed. For algebraizable logics, the well-known correspondence between the DDT and the equational definability of principal congruences is adapted to the contextual case. (shrink)

This paper develops an order-theoretic generalization of Blok and Pigozziʼs notion of an algebraizable logic. Unavoidably, the ordered model class of a logic, when it exists, is not unique. For uniqueness, the definition must be relativized, either syntactically or semantically. In sentential systems, for instance, the order algebraization process may be required to respect a given but arbitrary polarity on the signature. With every deductive filter of an algebra of the pertinent type, the polarity associates a reflexive (...) and transitive relation called a Leibniz order, analogous to the Leibniz congruence of abstract algebraic logic . Some core results of AAL are extended here to sentential systems with a polarity. In particular, such a system is order algebraizable if the Leibniz order operator has the following four independent properties: it is injective, it is isotonic, it commutes with the inverse image operator of any algebraic homomorphism, and it produces anti-symmetric orders when applied to filters that define reduced matrix models. Conversely, if a sentential system is order algebraizable in some way, then the order algebraization process naturally induces a polarity for which the Leibniz order operator has properties –. (shrink)

In a classical paper [15] V. Glivenko showed that a proposition is classically demonstrable if and only if its double negation is intuitionistically demonstrable. This result has an algebraic formulation: the double negation is a homomorphism from each Heyting algebra onto the Boolean algebra of its regular elements. Versions of both the logical and algebraic formulations of Glivenko’s theorem, adapted to other systems of logics and to algebras not necessarily related to logic can be found in the literature (see (...) [2, 9, 8, 14] and [13, 7, 14]). The aim of this paper is to offer a general frame for studying both logical and algebraic generalizations of Glivenko’s theorem. We give abstract formulations for quasivarieties of algebras and for equivalential and algebraizable deductive systems and both formulations are compared when the quasivariety and the deductive system are related. We also analyse Glivenko’s theorem for compatible expansions of both cases. (shrink)

Finitely algebraizable deductive systems were introduced by Blok and Pigozzi to capture the essential properties of those deductive systems that are very tightly connected to quasivarieties of universal algebras. They include the equivalential logics of Czelakowski. Based on Blok and Pigozzi’s work, Herrmann defined algebraizable deductive systems. These are the equivalential deductive systems that are also truth-equational, in the sense that the truth predicate of the class of their reduced matrix (...) models is explicitly definable by some set of unary equations. Raftery undertook the task of characterizing the property of truth-equationality for arbitrary deductive systems. In this paper, following Raftery, we extend the notion of truth-equationality for logics formalized as $\pi$-institutions and abstract several of the results that hold for deductive systems in this more general categorical context. (shrink)

A deductive system \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $$\mathcal{S}$$ \end{document} (in the sense of Tarski) is Fregean if the relation of interderivability, relative to any given theory T, i.e., the binary relation between formulas\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $$\{ \left\langle {\alpha,\beta } \right\rangle :T,\alpha \vdash s \beta and T,\beta \vdash s \alpha \},$$ \end{document}is a congruence relation on the formula algebra. The multiterm deduction-detachment theorem is a natural generalization of (...) the deduction theorem of the classical and intuitionistic propositional calculi (IPC) in which a finite system of possibly compound formulas collectively plays the role of the implication connective of IPC. We investigate the deductive structure of Fregean deductive systems with the multiterm deduction-detachment theorem within the framework of abstract algebraic logic. It is shown that each deductive system of this kind has a deductive structure very close to that of the implicational fragment of IPC. Moreover, it is algebraizable and the algebraic structure of its equivalent quasivariety is very close to that of the variety of Hilbert algebras. The equivalent quasivariety is however not in general a variety. This gives an example of a relatively point-regular, congruence-orderable, and congruence-distributive quasivariety that fails to be a variety, and provides what apparently is the first evidence of a significant difference between the multiterm deduction-detachment theorem and the more familiar form of the theorem where there is a single implication connective. (shrink)

Equivalent deductive systems were introduced in [4] with the goal of treating 1-deductive systems and algebraic 2-deductive systems in a uniform way. Results of [3], appropriately translated and strengthened, show that two deductive systems over the same language type are equivalent if and only if their lattices of theories are isomorphic via an isomorphism that commutes with substitutions. Deductive equivalence of π-institutions [14, 15] generalizes the notion of equivalence of deductive (...) systems. In [15, Theorem 10.26] this criterion for the equivalence of deductive systems was generalized to a criterion for the deductive equivalence of term π-institutions, forming a subclass of all π-institutions that contains those π-institutions directly corresponding to deductive systems. This criterion is generalized here to cover the case of arbitrary π-institutions. (shrink)

This book stands at the intersection of two topics: the decidability and computational complexity of hybrid logics, and the deductive systems designed for them. Hybrid logics are here divided into two groups: standard hybrid logics involving nominals as expressions of a separate sort, and non-standard hybrid logics, which do not involve nominals but whose expressive power matches the expressive power of binder-free standard hybrid logics.The original results of this book are split into two parts. This division reflects the (...) division of the book itself. The first type of results concern model-theoretic and complexity properties of hybrid logics. Since hybrid logics which we call standard are quite well investigated, the efforts focused on hybrid logics referred to as non-standard in this book. Non-standard hybrid logics are understood as modal logics with global counting operators ) whose expressive power matches the expressive power of binder-free standard hybrid logics. The relevant results comprise: 1. Establishing a sound and complete axiomatization for the modal logic K with global counting operators ), which can be easily extended onto other frame classes, 2. Establishing tight complexity bounds, namely NExpTime-completeness for the modal logic with global counting operators defined over the classes of arbitrary, reflexive, symmetric, serial and transitive frames ), MT), MD), MB), MK4) with numerical subscripts coded in binary. Establishing the exponential-size model property for this logic defined over the classes of Euclidean and equivalential frames ), MS5).Results of the second type consist of designing concrete deductive systems for standard and non-standard hybrid logics. More precisely, they include: 1. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for a rich class of binder-free standard hybrid logics. An interesting feature of indicated calculi is the nonbranching character of the rule, 2. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for non-standard hybrid logics. The internalization technique applied to a tableau calculus for the modal logic with global counting operators is novel in the literature, 3. Devising the first hybrid algorithm involving an inequality solver for modal logics with global counting operators. Transferring the arithmetical part of reasoning to an inequality solver turned out to be sufficient in ensuring termination.The book is directed to philosophers and logicians working with modal and hybrid logics, as well as to computer scientists interested in deductive systems and decision procedures for logics. Extensive fragments of the first part of the book can also serve as an introduction to hybrid logics for wider audience interested in logic.The content of the book is situated in the areas of formal logic and theoretical computer science with some elements of the theory of computational complexity. (shrink)

Given a π -institution I , a hierarchy of π -institutions I is constructed, for n ≥ 1. We call I the n-th order counterpart of I . The second-order counterpart of a deductive π -institution is a Gentzen π -institution, i.e. a π -institution associated with a structural Gentzen system in a canonical way. So, by analogy, the second order counterpart I of I is also called the “Gentzenization” of I . In the main result of the paper, (...) it is shown that I is strongly Gentzen , i.e. it is deductively equivalent to its Gentzenization via a special deductive equivalence, if and only if it has the deduction-detachment property. (shrink)

This paper studies, with techniques ofAlgebraic Logic, the effects of putting a bound on the cardinality of the set of side formulas in the Deduction Theorem, viewed as a Gentzen-style rule, and of adding additional assumptions inside the formulas present in Modus Ponens, viewed as a Hilbert-style rule. As a result, a denumerable collection of new Gentzen systems and two new sentential logics have been isolated. These logics are weaker than the positive implicative logic. We have determined their algebraic (...) models and the relationships between them, and have classified them according to several standard criteria of Abstract Algebraic Logic. One of the logics is protoalgebraic but neither equivalential nor weakly algebraizable, a rare situation where very few natural examples were hitherto known. In passing we have found new, alternative presentations of positive implicative logic, both in Hilbert style and in Gentzen style, and have characterized it in terms of the restricted Deduction Theorem: it is the weakest logic satisfying Modus Ponens and the Deduction Theorem restricted to at most 2 side formulas. The algebraic part of the work has lead to the class of quasi-Hilbert algebras, a quasi-variety of implicative algebras introduced by Pla and Verdú in 1980, which is larger than the variety of Hilbert algebras. Its algebraic properties reflect those of the corresponding logics and Gentzen systems. (shrink)

This paper studies, with techniques ofAlgebraic Logic, the effects of putting a bound on the cardinality of the set of side formulas in the Deduction Theorem, viewed as a Gentzen-style rule, and of adding additional assumptions inside the formulas present in Modus Ponens, viewed as a Hilbert-style rule. As a result, a denumerable collection of new Gentzen systems and two new sentential logics have been isolated. These logics are weaker than the positive implicative logic. We have determined their algebraic (...) models and the relationships between them, and have classified them according to several standard criteria of Abstract Algebraic Logic. One of the logics is protoalgebraic but neither equivalential nor weakly algebraizable, a rare situation where very few natural examples were hitherto known. In passing we have found new, alternative presentations of positive implicative logic, both in Hilbert style and in Gentzen style, and have characterized it in terms of the restricted Deduction Theorem: it is the weakest logic satisfying Modus Ponens and the Deduction Theorem restricted to at most 2 side formulas. The algebraic part of the work has lead to the class of quasi-Hilbert algebras, a quasi-variety of implicative algebras introduced by Pla and Verdú in 1980, which is larger than the variety of Hilbert algebras. Its algebraic properties reflect those of the corresponding logics and Gentzen systems. (shrink)

An important part of the theory of algebraizable sentential logics consists of studying the algebraic semantics of these logics. As developed by Czelakowski, Blok, and Pigozzi and Font and Jansana, among others, it includes studying the properties of logical matrices serving as models of deductive systems and the properties of abstract logics serving as models of sentential logics. The present paper contributes to the development of the categorical theory by abstracting some of these model theoretic aspects and (...) results from the level of sentential logics to the level of π-institutions. (shrink)

This paper provides a semantic analysis of admissible rules and associated completeness conditions for arbitrary deductive systems, using the framework of abstract algebraic logic. Algebraizability is not assumed, so the meaning and significance of the principal notions vary with the level of the Leibniz hierarchy at which they are presented. As a case study of the resulting theory, the nonalgebraizable fragments of relevance logic are considered.

In this note, it is shown that, given a π -institution ℐ = 〈Sign, SEN, C 〉, with N a category of natural transformations on SEN, every theory family T of ℐ includes a unique largest theory system equation image of ℐ. equation image satisfies the important property that its N -Leibniz congruence system always includes that of T . As a consequence, it is shown, on the one hand, that the relation ΩN = ΩN characterizes N -protoalgebraicity inside the (...) class of N -prealgebraic π -institutions and, on the other, that all N -Leibniz theory families associated with theory families of a protoalgebraic π -institution ℐ are in fact N -Leibniz theory systems. (shrink)

This important book provides a new unifying methodology for logic. It replaces the traditional view of logic as manipulating sets of formulas with the notion of structured families of labelled formulas with algebraic structures. This approach has far reaching consequences for the methodology of logics and their semantics, and the book studies the main features of such systems along with their applications. It will interest logicians, computer scientists, philosophers and linguists.

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated \(\mathsf {ND}^1_{\mathsf {ISCI}}\) and a semantically motivated \(\mathsf {ND}^2_{\mathsf {ISCI}}\). The formulation of \(\mathsf {ND}^1_{\mathsf {ISCI}}\) is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, but (...) due to the normalization procedure non-subformulas can label only leaves of proofs. In \(\mathsf {ND}^2_{\mathsf {ISCI}}\), we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic. (shrink)

George Boole published the pamphlet The Mathematical Analysis of Logic in 1847. He believed that logic should belong to a universal mathematics that would cover both quantitative and nonquantitative research. With his pamphlet, Boole signalled an important change in symbolic logic: in contrast with his predecessors, his thinking was exclusively extensional. Notwithstanding the innovations introduced he accepted all traditional Aristotelean syllogisms. Nevertheless, some criticisms have been raised concerning Boole’s view of Aristotelean logic as the solution of algebraic equations. In order (...) to circumvent such criticisms, we show here how Boole’s conclusions may be deduced from the axioms and inference rules proposed in his pamphlet, from which Aristotle’s deductions in Prior Analytics (including those that are completed through an impossibility) can be stated as theorems. We clarify his method for dealing with both universal and particular premises by means of his symbol v and demystify some criticisms concerning the way he expressed particular premises. Boole’s conclusions for some of those premises for which according to Aristotle there is no deduction are also discussed. The deductive system presented here has the potential to provide a new perspective on Boole’s approach to logic in The Mathematical Analysis of Logic. (shrink)

This presentation of Aristotle's natural deduction system supplements earlier presentations and gives more historical evidence. Some fine-tunings resulted from conversations with Timothy Smiley, Charles Kahn, Josiah Gould, John Kearns,John Glanvillle, and William Parry.The criticism of Aristotle's theory of propositions found at the end of this 1974 presentation was retracted in Corcoran's 2009 HPL article "Aristotle's demonstrative logic".

Firstly, a natural deduction system in standard style is introduced for Nelson's para-consistent logic N4, and a normalization theorem is shown for this system. Secondly, a natural deduction system in sequent calculus style is introduced for N4, and a normalization theorem is shown for this system. Thirdly, a comparison between various natural deduction systems for N4 is given. Fourthly, a strong normalization theorem is shown for a natural deduction system for a sublogic of N4. Fifthly, a strong normalization theorem (...) is proved for a typed λ-calculus for a neighbor of N4. Finally, it is remarked that the natural deduction frameworks presented can also be adapted for Wansing's basic connexive logic C. (shrink)

Our goal is to develop a syntactical apparatus for propositional logics in which the accepted and rejected propositions have the same status and obeying treated in the same way. The suggested approach is based on the ideas of Łukasiewicz used for the classical logic and in addition, it includes the use of multiple conclusion rules. More precisely, a consequence relation is defined on a set of statements of forms “proposition _A_ is accepted” and “proposition _A_ is rejected”, where _A_ is (...) a proposition,—a unified consequence relation. Accordingly, the rules defining a unified consequence relation,—the unified rules, have statements as premises and as conclusions. A special attention is paid to the logics in which each proposition is either accepted or rejected. If we express this property via unified rules and add them to a unified deductive system, such a unified deductive system defines a reversible unified consequence: a statement “proposition _B_ is accepted” is derived from the statement “proposition _A_ is accepted” if and only if a statement “proposition _A_ is rejected” is derived from the statement “proposition _B_ is rejected”. (shrink)

. This paper continues a systematic approach to build natural deduction calculi and corresponding proof procedures for non-classical logics. Our attention is now paid to the framework of paraconsistent logics. These logics are used, in particular, for reasoning about systems where paradoxes do not lead to the `deductive explosion', i.e., where formulae of the type `A follows from false', for any A, are not valid. We formulate the natural deduction system for the logic PCont, explain its main concepts, (...) define a proof searching technique and illustrate it by examples. The presentation is accompanied by demonstrating the correctness of these developments. (shrink)

A category theoretic generalization of the theory of algebraizable deductive systems of Blok and Pigozzi is developed. The theory of institutions of Goguen and Burstall is used to provide the underlying framework which replaces and generalizes the universal algebraic framework based on the notion of a deductive system. The notion of a term -institution is introduced first. Then the notions of quasi-equivalence, strong quasi-equivalence and deductive equivalence are defined for -institutions. Necessary and sufficient conditions are (...) given for the quasi-equivalence and the deductive equivalence of two term -institutions, based on the relationship between their categories of theories. The results carry over without any complications to institutions, via their associated -institutions. The -institution associated with a deductive system and the institution of equational logic are examined in some detail and serve to illustrate the general theory. (shrink)

Varieties of natural deduction systems are introduced for Wansing’s paraconsistent non-commutative substructural logic, called a constructive sequential propositional logic (COSPL), and its fragments. Normalization, strong normalization and Church-Rosser theorems are proved for these systems. These results include some new results on full Lambek logic (FL) and its fragments, because FL is a fragment of COSPL.

In a fluent, clear, and lively style this translation by two of Maslov's junior colleagues brings the work of the late Soviet scientist S. Yu. Maslov to a wider audience. Maslov was considered by his peers to be a man of genius who was making fundamental contributions in the fields of automatic theorem proving and computational logic. He published little, and those few papers were regarded as notoriously difficult. This book, however, was written for a broad audience of readers and (...) describes elegant examples of applications in such fields as computer science, artificial intelligence, operations research, economic modeling, and biological modeling, among others. The book also brings to light the work by the American mathematician E. L. Post, which inspired Maslov's own work in the development of a general theory and which has been long neglected by mathematicial logicians and systems theorists in the United States. The book's first chapter introduces the Rules of the Game. Part I, Mathematics of Calculi, covers E. L. Post's canonical systems, deductive systems and algorithms, and probabilistic calculi and deductive information. Part II, Horizonal Modeling, takes up a "toy" economy, the calculi of technological possibilities, and the development of rules. Part III, Vertical Modeling, deals with the topics of "to fight and to search" and the consequences of the asymmetry of cognitive mechanisms. Vladimir Lifschitz is affiliated with the Department of Computer Science at Stanford University, and Michael Gelfond with the Department of Electrical Engineering and Computer Science at the University of Texas, El Paso. Theory of Deductive Systems and Its Applicationsis included in the Foundation of Computing Series, edited by Michael Garey. (shrink)

BL-algebras rise as Lindenbaum algebras from many valued logic introduced by Hájek [2]. In this paper Boolean ds and implicative ds of BL-algebras are defined and studied. The following is proved to be equivalent: (i) a ds D is implicative, (ii) D is Boolean, (iii) L/D is a Boolean algebra. Moreover, a BL-algebra L contains a proper Boolean ds iff L is bipartite. Local BL-algebras, too, are characterized. These results generalize some theorems presented in [4], [5], [6] for MV-algebras which (...) are BL-algebras fulfiling an additional double negation law x = x **. (shrink)

We deal with monotone structural deductive systems in an unspecified propositional language \ . These systems fall into several overlapping classes, forming a hierarchy. Along with well-known classes of deductive systems such as those of implicative, Fregean and equivalential systems, we consider new classes of unital and weakly implicative systems. The latter class is auxiliary, while the former is central in our discussion. Our analysis of unital systems leads to the concept of (...) Lindenbaum–Tarski algebra which, under some natural conditions, is a free algebra in a variety closely related to the deductive system in focus. (shrink)

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

A category theoretic generalization of the theory of algebraizable deductive systems of Blok and Pigozzi is developed. The theory of institutions of Goguen and Burstall is used to provide the underlying framework which replaces and generalizes the universal algebraic framework based on the notion of a deductive system. The notion of a term π-institution is introduced first. Then the notions of quasi-equivalence, strong quasi-equivalence and deductive equivalence are defined for π-institutions. Necessary and sufficient conditions are (...) given for the quasi-equivalence and the deductive equivalence of two term π-institutions, based on the relationship between their categories of theories. The results carry over without any complications to institutions, via their associated π-institutions. The π-institution associated with a deductive system and the institution of equational logic are examined in some detail and serve to illustrate the general theory. (shrink)

The promised mathematical system—the Constructibility Theory—is presented as an axiomatized deductive theory formalized in a many‐sorted first‐order logical language. The axioms of the theory are specified and a justification for each of the axioms is given. Objections to the theory are considered.

The author presents a deduction system for Quantum Logic. This system is a combination of a natural deduction system and rules based on the relation of compatibility. This relation is the logical correspondant of the commutativity of observables in Quantum Mechanics or perpendicularity in Hilbert spaces. Contrary to the system proposed by Gibbins and Cutland, the natural deduction part of the system is pure: no algebraic artefact is added. The rules of the system are the rules of Classical Natural Deduction (...) in which is added a control of contexts using the compatibility relation. The author uses his system to prove the following theorem: if propositions of a quantum logical propositional calculus system are mutually compatible, they form a classical subsystem. (shrink)

In this paper two deductive systems associated with relevance logic are studied from an algebraic point of view. One is defined by the familiar, Hilbert-style, formalization of R; the other one is a weak version of it, called WR, which appears as the semantic entailment of the Meyer-Routley-Fine semantics, and which has already been suggested by Wójcicki for other reasons. This weaker consequence is first defined indirectly, using R, but we prove that the first one turns out to (...) be an axiomatic extension of WR. Moreover we provide WR with a natural Gentzen calculus. It is proved that both deductive systems have the same associated class of algebras but different classes of models on these algebras. The notion of model used here is an abstract logic, that is, a closure operator on an abstract algebra; the abstract logics obtained in the case of WR are also the models, in a natural sense, of the given Gentzen calculus. (shrink)

We propose various methods for combining or amalgamating propositional languages and deductive systems. We make heavy use of quantales and quantale modules in the wake of previous works by the present and other authors. We also describe quite extensively the relationships among the algebraic and order-theoretic constructions and the corresponding ones based on a purely logical approach.

A pair of deductive systems (S,S’) is Leibniz-linked when S’ is an extension of S and on every algebra there is a map sending each filter of S to a filter of S’ with the same Leibniz congruence. We study this generalization to arbitrary deductive systems of the notion of the strong version of a protoalgebraic deductive system, studied in earlier papers, and of some results recently found for particular non-protoalgebraic deductive systems. The (...) necessary examples and counterexamples found in the literature are described. (shrink)

Basin-Matthews-Viganò approach to construction of labelled deduction systems for normal modal logics is adapted to „Fitch proof-format“, and it is applied to the language of deontic-praxeological logic. Segerberg's suggestion on how to asses the adequacy of a logic for Kanger's theory of rights is being formally explicated and it is proved that herewith proposed system of labelled deduction satisfies Segerberg's criteria of adequacy. For the purpose of building the proof a semantics is given, which connects „the simplest semantics of (...) action“ with standard semantics of deontic logic. Soundness and completeness of the proposed labelled deduction with respect to aforementioned semantics is proved. (shrink)