We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.

Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. With minor (...) restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the logics. (shrink)

We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems.

This paper is concerned with the logical structure of arithmetical theories. We survey results concerning logics and admissible rules of constructive arithmetical theories. We prove a new theorem: the admissible propositional rules of Heyting Arithmetic are the same as the admissible propositional rules of Intuitionistic Propositional Logic. We provide some further insights concerning predicate logical admissible rules for arithmetical theories.

Lemmon and Scott introduced the notion of a modal system's providing the rule of disjunction. No consistent normal extension of KB provides this rule. An alternative rule is defined, which KDB, KTB, and other systems are shown to provide, while K and other systems provide the Lemmon-Scott rule but not the alternative rule. If S provides the alternative rule then either —A is a theorem of S or A is whenever A -> ΠA is a theorem; the converse fails. It (...) is suggested that systems with this property are appropriate for handling sorites paradoxes, where D is read as 'clearly*. The S4 axiom fails in such systems. (shrink)

We present a basis for the admissible rules of intuitionistic propositional logic. Thereby a conjecture by de Jongh and Visser is proved. We also present a proof system for the admissible rules, and give semantic criteria for admissibility.

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

Refutation systems are formal systems for inferring the falsity of formulae. These systems can, in particular, be used to syntactically characterise logics. In this paper, we explore the close connection between refutation systems and admissible rules. We develop technical machinery to construct refutation systems, employing techniques from the study of admissible rules. Concretely, we provide a refutation system for the intermediate logics of bounded branching, known as the Gabbay–de Jongh logics. We show that this gives a characterisation of these logics (...) in terms of their admissible rules. To illustrate the technique, we also provide a refutation system for Medvedev’s logic. (shrink)

We present an algorithm, based both on semantic tableaux and resolution, which is able to check the projectivity of a formula in intuitionistic propositional calculus. Suitably iterated, it also computes projective approximations, thus providing best E-unifiers for the equational theory of Heyting algebras. Applications to admissible inference rules are immediate.

The aim of this book is to present the fundamental theoretical results concerning inference rules in deductive formal systems. Primary attention is focused on: admissible or permissible inference rules the derivability of the admissible inference rules the structural completeness of logics the bases for admissible and valid inference rules. There is particular emphasis on propositional non-standard logics (primary, superintuitionistic and modal logics) but general logical consequence relations and classical first-order theories are also considered. The book is basically self-contained and special (...) attention has been made to present the material in a convenient manner for the reader. Proofs of results, many of which are not readily available elsewhere, are also included. The book is written at a level appropriate for first-year graduate students in mathematics or computer science. Although some knowledge of elementary logic and universal algebra are necessary, the first chapter includes all the results from universal algebra and logic that the reader needs. For graduate students in mathematics and computer science the book is an excellent textbook. (shrink)

in die operative Logik und Mathematik Zweite Auflage Springer-Verlag Berlin Heidelberg New York 1969 Paul Lorenzen o. Prof. der Philosophie an der Universitat Erlangen Geschaftsfilhrende Herausgeber: Prof. Dr. B. Eckmann Eidgenossische Technische Hochschule Zurich Prof. Dr. B. L. van cler Waerclen Mathematisches Institut der Universitat ZUrich ISBN 978-3-642-86519-0 ISBN 978-3-642-86518-3 (eBook) DOl 10.1007/978-3-642-86518-3 Aile Rechte vorbehalten. Kein Teil dieses Buches darf ohne schriftliche Genehmigung des Springer-Verlages ubersetzt oder in irgendeiner Form vervielfaltigt werden © by Springer-Verlag Berlin· Heidelberg 1955 und 1969 (...) Softcover reprint of the hardcover 2nd edition 1969 Library of Congress Catalog Card Number 73-76724 Titel-Nr. 5061 Vorwort zur zweiten Auflage. Fiir die Neuauflage ist der Text nur unwesentlich geandert worden. Es ist - neben der Korrektur einiger Ungenauigkeiten - vor allem die Terminologie und Symbolik an meine spateren Arbeiten angeglichen. Obwohl ich - verstandlicherweise - jetzt die Ansatze der spateren Arbeiten fiir "sachgemaBer" halte, z. B. eine Logik der Dialoge statt einer Logik der Kalkiile, die Verwendung indefiniter Quantoren statt einer expliziten Konstruktion von Sprachschichten, enthalt diese Neu­ auflage den Inhalt der 1. Auflage unverandert. Der Leser kann also einen Vergleich mit meinen spateren Arbeiten (vgl. Literaturverzeichnis) seIber durchfiihren. Mein Dank gilt wiederum dem Verlag fiir seine entgegenkommende Mitarbeit bei der Vorbereitung dieser Neuauflage. Erlangen, den 1. November I968. PAUL LORENZEN. Vorwort zur ersten Auflage. (shrink)

We investigate finitarity of unification types in locally finite varieties of Heyting algebras, giving both positive and negative results. We make essential use of finite dualities within a conceptualization for E-unification theory 733–752) relying on the algebraic notion of a projective object.

Structural completeness properties are investigated for a range of popular t-norm based fuzzy logics—including Łukasiewicz Logic, Gödel Logic, Product Logic, and Hájek's Basic Logic—and their fragments. General methods are defined and used to establish these properties or exhibit their failure, solving a number of open problems.

This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

We show that the variety of equivalential algebras with regularization gives the algebraic semantics for the -fragment of intuitionistic propositional logic. We also prove that this fragment is hereditarily structurally complete.

Visser's rules form a basis for the admissible rules of . Here we show that this result can be generalized to arbitrary intermediate logics: Visser's rules form a basis for the admissible rules of any intermediate logic for which they are admissible. This implies that if Visser's rules are derivable for then has no nonderivable admissible rules. We also provide a necessary and sufficient condition for the admissibility of Visser's rules. We apply these results to some specific intermediate logics and (...) obtain that Visser's rules form a basis for the admissible rules of, for example, De Morgan logic, and that Dummett's logic and the propositional Gödel logics do not have nonderivable admissible rules. (shrink)

Epistemic logics for subjects of bounded rationality are in effect nonnormal modal logics. Admissible rules are of interest in such logics. However, the usual methods for establishing admissibility employ Kripke models and are therefore inappropriate for nonnormal logics. This paper extends syntactic methods for a variety of rules and nonnormal logics. In doing so it answers a question asked by Chellas and Segerberg.

Related Works: Part I: Michael Zakharyaschev. Canonical Formulas for $K4$. Part I: Basic Results. J. Symbolic Logic, Volume 57, Issue 4 , 1377--1402. Project Euclid: euclid.jsl/1183744119 Part II: Michael Zakharyaschev. Canonical Formulas for K4. Part II: Cofinal Subframe Logics. J. Symbolic Logic, Volume 61, Issue 2 , 421--449. Project Euclid: euclid.jsl/1183745008.

We study unification problem and problem of admissibility for inference rules in minimal Johanssonsʼ logic J and positive intuitionistic logic IPC+. This paper proves that the problem of admissibility for inference rules with coefficients is decidable for the paraconsistent minimal Johanssonsʼ logic J and the positive intuitionistic logic IPC+. Using obtained technique we show also that the unification problem for these logics is also decidable: we offer algorithms which compute complete sets of unifiers for any unifiable formula. Checking just unifiability (...) of formulas with coefficients also works via verification of admissibility. (shrink)

Hereditary structural completeness is established for a range of substructural logics, mainly without the weakening rule, including fragments of various relevant or many-valued logics. Also, structural completeness is disproved for a range of systems, settling some previously open questions.

Uniform infinite bases are defined for the single-conclusion and multiple-conclusion admissible rules of the implication–negation fragments of intuitionistic logic and its consistent axiomatic extensions . A Kripke semantics characterization is given for the structurally complete implication–negation fragments of intermediate logics, and it is shown that the admissible rules of this fragment of form a PSPACE-complete set and have no finite basis.

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia (...) theorem and the theory of modal companions to systems of multiple-conclusion rules or (finitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property. (shrink)

The general aim of this book is to provide an elementary exposition of some basic concepts in terms of which both classical and non-dassicallogirs may be studied and appraised. Although quantificational logic is dealt with briefly in the last chapter, the discussion is chiefly concemed with propo gjtional cakuli. Still, the subject, as it stands today, cannot br covered in one book of reasonable length. Rather than to try to include in the volume as much as possible, I have put (...) emphasis on some selected topics. Even these could not be roverrd completely, but for each topic I have attempted to present a detailed and precise t’Xposition of several basic results including some which are non-trivial. The roots of some of the central ideas in the volume go back to J. Luka siewicz’s seminar on mathematicallogi. (shrink)

Related Works: Part I: Michael Zakharyaschev. Canonical Formulas for $K4$. Part I: Basic Results. J. Symbolic Logic, Volume 57, Issue 4 , 1377--1402. Project Euclid: euclid.jsl/1183744119 Part III: Michael Zakharyaschev. Canonical Formulas for K4. Part III: The Finite Model Property. J. Symbolic Logic, Volume 62, Issue 3 , 950--975. Project Euclid: euclid.jsl/1183745306.

The paper considers certain properties of intermediate and moda propositional logics.The first part contains a proof of the theorem stating that each intermediate logic is closed under the Kreisel-Putnam rule xyz/(xy)(xz).

We show that some common varieties of modal K4-algebras have finitary unification type, thus providing effective best solutions for equations in free algebras. Applications to admissible inference rules are immediate.