Recently discovered documents have shown how Gentzen had arrived at the final form of natural deduction, namely by trying out a great number of alternative formulations. What led him to natural deduction in the first place, other than the general idea of studying “mathematical inference as it appears in practice,” is not indicated anywhere in his publications or preserved manuscripts. It is suggested that formal work in axiomatic logic lies behind the birth of Gentzen’s natural deduction, rather than (...) any single decisive influence in the work of others. Various axiomatizations are explored in turn, from the classical axioms of Hilbert and Ackermann to the intuitionistic axiomatization of Heyting. (shrink)

This book provides a systematic and comprehensive description of Non-Axiomatic Logic, which is the result of the author's research for about three decades.Non-Axiomatic Logic is designed to provide a uniform logical foundation for Artificial Intelligence, as well as an abstract description of the “laws of thought” followed by the human mind. Different from “mathematical” logic, where the focus is the regularity required when demonstrating mathematical conclusions, Non-Axiomatic Logic is an attempt to return to (...) the original aim of logic, that is, to formulate the regularity in actual human thinking. To achieve this goal, the logic is designed under the assumption that the system has insufficient knowledge and resources with respect to the problems to be solved, so that the “logical conclusions” are only valid with respect to the available knowledge and resources. Reasoning processes according to this logic covers cognitive functions like learning, planning, decision making, problem solving, etc.This book is written for researchers and students in Artificial Intelligence and Cognitive Science, and can be used as a textbook for courses at graduate level, or upper-level undergraduate, on Non-Axiomatic Logic. (shrink)

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. (shrink)

In this paper we investigate the relation between the axiomatization of a given logical consequence operation and axiom systems defining the class of algebras related to that consequence operation. We show examples which prove that, in general there are no natural relation between both ways of axiomatization.

In the literature, different axiomatizations of Public Announcement Logic (PAL) have been proposed. Most of these axiomatizations share a “core set” of the so-called “reduction axioms”. In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that the proof system based on this core set of axioms does not completely axiomatize PAL without additional axioms and rules. In fact, many of the intuitive axioms and rules we took for granted could not be derived from (...) the core set. Moreover, we also propose and advocate an alternative yet meaningful axiomatization of PAL without the reduction axioms. The completeness is proved directly by a detour method using the canonical model where announcements are treated as merely labels for modalities as in normal modal logics. This new axiomatization and its completeness proof may sharpen our understanding of PAL and can be adapted to other dynamic epistemic logics. (shrink)

A certain type of inference rules in modal logics, generalizing Gabbay's Irreflexivity rule, is introduced and some general completeness results about modal logics axiomatized with such rules are proved.

Boolean connexive logic is an extension of Boolean logic that is closed under Modus Ponens and contains Aristotle’s and Boethius’ theses. According to these theses a sentence cannot imply its negation and the negation of a sentence cannot imply the sentence; and if the antecedent implies the consequent, then the antecedent cannot imply the negation of the consequent and if the antecedent implies the negation of the consequent, then the antecedent cannot imply the consequent. Such a logic (...) was first introduced by Jarmużek and Malinowski, by means of so-called relating semantics and tableau systems. Subsequently its modal extension was determined by means of the combination of possible-worlds semantics and relating semantics. In the following article we present axiomatic systems of some basic and modal Boolean connexive logics. Proofs of completeness will be carried out using canonical models defined with respect to maximal consistent sets. (shrink)

We give a sound and complete axiomatization for the full computation tree logic, CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

Dependence logic, introduced in Väänänen [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem.

1 Choice conjecture In axiomatizing nonclassical extensions of classical sentential logic one tries to make do, if one can, with adding to classical sentential logic a finite number of axiom schemes of the simplest kind and a finite number of inference rules of the simplest kind. The simplest kind of axiom scheme in effect states of a particular formula P that for any substitution of formulas for atoms the result of its application to P is to count as (...) an axiom. The simplest kind of onepremise inference rule in effect states of a particular pair of formulas P and Q that for any substitution of formulas for atoms, if the result of its application to P is a theorem, then the result of its application to Q is to count as a theorem; similarly for many-premise rules. Such are the schemes and rules of all the best-known modal and tense logics, for instance. Sometimes it is difficult to find such simple schemes and rules. In that case one may resort to less simple schemes or less simple rules. There is no generally recognized rigorous definition of "next simplest kind" of scheme. Neither is there any generally recognized definition of "next simplest kind" of rule, and hence there is no fully rigorous enunciation of the choice conjecture, the conjecture that schemes of the next simplest kind can always be avoided in favor of rules of the next simplest kind and vice versa. Nonetheless, there are cases where intuitively one does recognize that the schemes or rules in a given axiomatization are only slightly more complex than the simplest kind, including cases where one does have a choice between adopting slightly-more-complex-than-simplest schemes and adopting slightly-more-complex-than-simplest rules. In tense logic early examples of slightly more complex rules are found in [2] and [3] : there is one example of the embarrassed use of such rules in the former, and many examples of the enthusiastic use of such rules in the latter and its sequels. Accordingly the rules in question have come to be called "Gabbay-style" rules. (shrink)

In a recent paper Berto introduces a semantic system for a logic of imagination, intended as positive conceivability, and aboutness of imaginative acts. This system crucially adopts elements of both the semantics of conditionals and the semantics of analytical implications in order to account for the central logical traits of the notion of truth in an act of imagination based on an explicit input. The main problem left unsolved is to put forward a complete set of axioms for the (...) proposed system. In the present paper I offer a solution to this problem by providing a complete axiomatization of a generalization of the original semantics. The difficulty in proving completeness lies in the fact that the modalities that capture the notion of truth in an act of imagination are neither standard nor minimal, so that the construction of the canonical model and the proof of the truth lemma are to be substantially modified. (shrink)

Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed‐point logic. Inclusion logic is not axiomatisable in full, but its first order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first order consequences in inclusion logic.

This English translation of the author's original work has been thoroughly revised, expanded and updated. The book covers logical systems known as type-free or self-referential . These traditionally arise from any discussion on logical and semantical paradoxes. This particular volume, however, is not concerned with paradoxes but with the investigation of type-free sytems to show that: (i) there are rich theories of self-application, involving both operations and truth which can serve as foundations for property theory and formal semantics; (ii) these (...) theories provide a new outlook on classical topics, such as inductive definitions and predicative mathematics; (iii) they are particularly promising with regard to applications. Research arising from paradoxes has moved progressively closer to the mainstream of mathematical logic and has become much more prominent in the last twenty years. A number of significant developments, techniques and results have been discovered. Academics, students and researchers will find that the book contains a thorough overview of all relevant research in this field. (shrink)

Formal aspects of various ways of description of Jan Łukasiewicz’s four-valued modal logic £ are discussed. The original Łukasiewicz’s description by means of the accepted and rejected theorems, together with the four-valued matrix, is presented. Then the improved E.J. Lemmon’s description based upon three specific axioms, together with the relational semantics, is presented as well. It is proved that Lemmon’s axiomatic is not independent: one axiom is derivable on the base of the remanent two. Several axiomatizations, based on (...) three, two or one single axiom are provided and discussed, including S. Kripke’s axiomatics. It is claimed that (a) all substitutions of classical theorems, (b) the rule of modus ponens, (c) the definition of “◊” and (d) the single specific axiom schema: ⬜A ∧ B → A ∧ ⬜B, called the jumping necessity axiom, constitute an elegant axiomatics of the system £. (shrink)

We formulate a Hilbert-style axiomatic system and a tableau calculus for the STIT-based logic of imagination recently proposed in Wansing. Completeness of the axiom system is shown by the method of canonical models; completeness of the tableau system is also shown by using standard methods.

We investigate under what conditions a given set of collective judgments can arise from a specific voting procedure. In order to answer this question, we introduce a language similar to modal logic for reasoning about judgment aggregation procedures. In this language, the formula expresses that is collectively accepted, or that is a group judgment based on voting. Different judgment aggregation procedures may be underlying the group decision making. Here we investigate majority voting, where holds if a majority of individuals (...) accepts, consensus voting, where holds if all individuals accept, and dictatorship. We provide complete axiomatizations for judgment sets arising from all three aggregation procedures. (shrink)

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.

The paper studies the containment companion of a logic \. This consists of the consequence relation \ which satisfies all the inferences of \, where the variables of the conclusion are contained into those of the set of premises, in case this is not inconsistent. In accordance with the work started in [10], we show that a different generalization of the Płonka sum construction, adapted from algebras to logical matrices, allows to provide a matrix-based semantics for containment logics. In (...) particular, we provide an appropriate completeness theorem for a wide family of containment logics, and we show how to produce a complete Hilbert style axiomatization. (shrink)

The branching-time logic called Peircean by Arthur Prior is considered and given an infinite axiomatization. The axiomatization uses only the standard deduction rules for tense logic.

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 variety \(\mathbb{DHMSH}\) of dually hemimorphic semi-Heyting algebras was introduced in 2011 by the second author as an expansion of semi-Heyting algebras by a dual hemimorphism. In this paper, we focus on the variety \(\mathbb{DHMSH}\) from a logical point of view. The paper presents an extensive investigation of the logic corresponding to the variety of dually hemimorphic semi-Heyting algebras and of its axiomatic extensions, along with an equally extensive universal algebraic study of their corresponding algebraic semantics. Firstly, we (...) present a Hilbert-style axiomatization of a new logic called "Dually hemimorphic semi-Heyting logic" (\(\mathcal{DHMSH}\), for short), as an expansion of semi-intuitionistic logic \(\mathcal{SI}\) (also called \(\mathcal{SH}\)) introduced by the first author by adding a weak negation (to be interpreted as a dual hemimorphism). We then prove that it is implicative in the sense of Rasiowa and that it is complete with respect to the variety \(\mathbb{DHMSH}\). It is deduced that the logic \(\mathcal{DHMSH}\) is algebraizable in the sense of Blok and Pigozzi, with the variety \(\mathbb{DHMSH}\) as its equivalent algebraic semantics and that the lattice of axiomatic extensions of \(\mathcal{DHMSH}\) is dually isomorphic to the lattice of subvarieties of \(\mathbb{DHMSH}\). A new axiomatization for Moisil's logic is also obtained. Secondly, we characterize the axiomatic extensions of \(\mathcal{DHMSH}\) in which the "Deduction Theorem" holds. Thirdly, we present several new logics, extending the logic \(\mathcal{DHMSH}\), corresponding to several important subvarieties of the variety \(\mathbb{DHMSH}\). These include logics corresponding to the varieties generated by two-element, three-element and some four-element dually quasi-De Morgan semi-Heyting algebras, as well as a new axiomatization for the 3-valued Łukasiewicz logic. Surprisingly, many of these logics turn out to be connexive logics, only a few of which are presented in this paper. Fourthly, we present axiomatizations for two infinite sequences of logics namely, De Morgan Gödel logics and dually pseudocomplemented Gödel logics. Fifthly, axiomatizations are also provided for logics corresponding to many subvarieties of regular dually quasi-De Morgan Stone semi-Heyting algebras, of regular De Morgan semi-Heyting algebras of level 1, and of JI-distributive semi-Heyting algebras of level 1. We conclude the paper with some open problems. Most of the logics considered in this paper are discriminator logics in the sense that they correspond to discriminator varieties. Some of them, just like the classical logic, are even primal in the sense that their corresponding varieties are generated by primal algebras. (shrink)

In the paper we analyse the problem of axiomatizing the minimal variant of discussive logic denoted as $$ {\textsf {D}}_{\textsf {0}}$$ D 0. Our aim is to give its axiomatization that would correspond to a known axiomatization of the original discussive logic $$ {\textsf {D}}_{\textsf {2}}$$ D 2. The considered system is minimal in a class of discussive logics. It is defined similarly, as Jaśkowski’s logic $$ {\textsf {D}}_{\textsf {2}}$$ D 2 but with the help of the (...) deontic normal logic $$\textbf{D}$$ D. Although we focus on the smallest discussive logic and its correspondence to $$ {\textsf {D}}_{\textsf {2}}$$ D 2, we analyse to some extent also its formal aspects, in particular its behaviour with respect to rules that hold for classical logic. In the paper we propose a deductive system for the above recalled discussive logic. While formulating this system, we apply a method of Newton da Costa and Lech Dubikajtis—a modified version of Jerzy Kotas’s method used to axiomatize $$ {\textsf {D}}_{\textsf {2}}$$ D 2. Basically the difference manifests in the result—in the case of da Costa and Dubikajtis, the resulting axiomatization is pure modus ponens-style. In the case of $$ {\textsf {D}}_{\textsf {0}}$$ D 0, we have to use some rules, but they are mostly needed to express some aspects of positive logic. $$ {\textsf {D}}_{\textsf {0}}$$ D 0 understood as a set of theses is contained in $$ {\textsf {D}}_{\textsf {2}}$$ D 2. Additionally, any non-trivial discussive logic expressed by means of Jaśkowski’s model of discussion, applied to any regular modal logic of discussion, contains $$ {\textsf {D}}_{\textsf {0}}$$ D 0. (shrink)

In this paper we consider the modal logic with both \ and \ arising from Kripke models with a crisp accessibility and whose propositions are valued over the standard Gödel algebra \. We provide an axiomatic system extending the one from Caicedo and Rodriguez :37–55, 2015) for models with a valued accessibility with Dunn axiom from positive modal logics, and show it is strongly complete with respect to the intended semantics. The axiomatizations of the most usual frame restrictions (...) are given too. We also prove that in the studied logic it is not possible to get \ as an abbreviation of \, nor vice-versa, showing that indeed the axiomatic system we present does not coincide with any of the mono-modal fragments previously axiomatized in the literature. (shrink)

It is known that even seemingly small fragments of the first-order temporal logic over the natural numbers are not recursively enumerable. In this paper we show that the monodic fragment is an exception by constructing its finite Hilbert-style axiomatization. We also show that the monodic fragment with equality is not recursively axiomatizable.

We study the general problem of axiomatizing structures in the framework of modal logic and present a uniform method for complete axiomatization of the modal logics determined by a large family of classes of structures of any signature.

We outline the rather complicated history of attempts at axiomatizing Jaśkowski’s discussive logic $$\mathbf {D_2}$$ D2 and show that some clarity can be had by paying close attention to the language we work with. We then examine the problem of axiomatizing $$\mathbf {D_2}$$ D2 in languages involving discussive conjunctions. Specifically, we show that recent attempts by Ciuciura are mistaken. Finally, we present an axiomatization of $$\mathbf {D_2}$$ D2 in the language Jaśkowski suggested in his second paper on discussive (...) class='Hi'>logic, by following a remark of da Costa and Dubikajtis. We also deal with an interesting variant of $$\mathbf {D_2}$$ D2, introduced by Ciuciura, in which negation is also taken to be discussive. (shrink)

We consider the problem of finding, in the ambit of modal logic, a minimal characterization for finite Kripke frames, i.e., a formula which, given a frame, axiomatizes its theory employing the lowest possible number of variables and implies the other axiomatizations. We show that every finite transitive frame admits a minimal characterization over K4, and that this result can not be extended to K.

We study axiomatic extensions of the propositional constructive logic with strong negation having the disjunction property in terms of corresponding to them varieties of Nelson algebras. Any such varietyV is characterized by the property: (PQWC) ifA,B V, thenA×B is a homomorphic image of some well-connected algebra ofV.We prove:• each varietyV of Nelson algebras with PQWC lies in the fibre –1(W) for some varietyW of Heyting algebras having PQWC, • for any varietyW of Heyting algebras with PQWC the least (...) and the greatest varieties in –1(W) have PQWC, • there exist varietiesW of Heyting algebras having PQWC such that –1(W) contains infinitely many varieties (of Nelson algebras) with PQWC. (shrink)

Since belief revision deals with the interaction of belief and information over time, branching-time temporal logic seems a natural setting for a theory of belief change. We propose two extensions of a modal logic that, besides the next-time temporal operator, contains a belief operator and an information operator. The first logic is shown to provide an axiomatic characterization of the first six postulates of the AGM theory of belief revision, while the second, stronger, logic provides (...) an axiomatic characterization of the full set of AGM postulates. © 2006 Elsevier B.V. All rights reserved. (shrink)

We study the general problem of axiomatizing structures in the framework of modal logic and present a uniform method for complete axiomatization of the modal logics determined by a large family of classes of structures of any signature.

In [STU 00, KUT 03] we introduced a family of ‘modal' languages intended for talking about distances. These languages are interpreted in ‘distance spaces' which satisfy some of the standard axioms of metric spaces. Among other things, we singled out decidable logics of distance spaces and proved expressive completeness results relating classical and modal languages. The aim of this paper is to axiomatize the modal fragments of the semantically defined distance logics of [KUT 03] and give a new proof of (...) their decidability. (shrink)

An axiomatization is presented of the denotational semantics for first order language of Apt [1]. The goal is to obtain a rational reconstruction of the intuitions underlying this semantics. The axiomatization combines ideas about four valued logic with facts about substitutions. Soundness and completeness of the axiomatization are established. From the completeness proof a decision procedure is obtained that shows how four valued logic and order sensitivity of substitution together add up in a natural way to the denotational (...) semantics for the language of first order logic as proposed by Apt. (shrink)

In his book from 1984 Horst Wessel presents the system of strict logical consequence Fs (see also (Wessel, 1979)). The author maintained that this system axiomatized the relation |=s of strict logical consequence between formulas of Classical Propositional Calculi (CPC). Let |= be the classical consequence relation in CPC. The relation |=s is defined as follows: phi |=s psi iff phi |= psi, every variable from psi occurs in phi and neither phi is a contradiction nor psi is a tautology. (...) Clearly, if phi |=s psi, then neither phi is a tautology nor psi is a contradiction. Intuitions connected with the relation |=s were presented in (Wessel, 1984). The analysis of the relation |=s is also carried out in (Pietruszczak, 2004). In the present paper we will show that the system Fs is not a complete axiomatization of the relation |=s. Moreover, we will present the system VF s that is an «extension to completeness» of the Fs. (shrink)

In this paper, a suitable notion of bisimulation is proposed for the bimodal logic with contingency and accident. We obtain several van Benthem Characterization Theorems, and axiomatize the bimodal logic over the class of Eulidean frames and over some more restricted classes, showing their strong completeness via a novel strategy, thereby answering two open questions raised in the literature. With the new bisimulation notion, we also correct an error in the expressivity results in the literature.

In this paper we characterize, classify and axiomatize all axiomatic extensions of the IMT3 logic. This logic is the axiomatic extension of the involutive monoidal t-norm logic given by ¬φ3 ∨ φ. For our purpose we study the lattice of all subvarieties of the class IMT3, which is the variety of IMTL-algebras given by the equation ¬(x 3) ∨ x ≈ ⊤, and it is the algebraic counterpart of IMT3 logic. Since every subvariety of (...) IMT3 is generated by their totally ordered members, we study the structure of all IMT3-chains in order to determine the lattice of all subvarieties of IMT3. Given a family of IMT3-chains the number of elements of the largest odd finite subalgebra in the family and the number of elements of the largest even finite subalgebra in the family turns out to be a complete classifier of the variety generated. We obtain a canonical set of generators and a finite equational axiomatization for each subvariety and, for each corresponding logic, a finite set of characteristic matrices and a finite set of axioms. (shrink)

A sequential axiomatization is given for the 16-valued logic that has been proposed by Shramko-Wansing as a candidate for the basic logic of logical bilattices.

Three-valued (strong-Kleene) modal logic provides the foundation for a new approach to formalizing causal explanation as a relation between partial situations. The approach makes fine-grained distinctions between aspects of events, even between aspects that are equivalent in classical logic. The framework can accommodate a variety of ontologies concerning the relata of causal explanation. I argue, however, for a tripartite ontology of objects corresponding to sentential nominals: facts, tropes (or facta or states of affairs), and situations (or events). I (...) axiomatize the relations and use canonical models to demonstrate completeness. (shrink)

In memoriam José Arrazola Ramírez The logic $\textbf{G}^{\prime}_3$ was introduced by Osorio et al. in 2008; it is a three-valued logic, closely related to the paraconsistent logic $\textbf{CG}^{\prime}_3$ introduced by Osorio et al. in 2014. The logic $\textbf{CG}^{\prime}_3$ is defined in terms of a multi-valued semantics and has the property that each theorem in $\textbf{G}^{\prime}_3$ is a theorem in $\textbf{CG}^{\prime}_3$. Kripke-type semantics has been given to $\textbf{CG}^{\prime}_3$ in two different ways by Borja et al. in 2016. (...) In this work, we continue the study of $\textbf{CG}^{\prime}_3$, obtaining a Hilbert-type axiomatic system and proving a soundness and completeness theorem for this logic. (shrink)

In a recent paper, Negri and Pavlović (Studia Logica 1–35, 2020) have formulated a decidable sequent calculus for the logic of agency, specifically for a deliberative see-to-it-that modality, or dstit. In that paper the adequacy of the system is demonstrated by showing the derivability of the axiomatization of dstit from Belnap et al. (Facing the future: agents and choices in our indeterminist world. Oxford University Press, Oxford, 2001). And while the influence of the latter book on the study of (...) logics of agency cannot be overstated, we note that this is not the only axiomatization of that modality available. In fact, an earlier (and arguably purer) one was offered in Xu (J Philosophical Logic 27(5):505–552, 1998). In this article we fill this lacuna by proving that this alternative axiomatization is likewise readily derivable in the system of Negri and Pavlović (Studia Logica 1–35, 2020). (shrink)

KR is Anderson and Belnap’s relevance logic R with the addition of the axiom of EFQ: \ \rightarrow q\). Since KR is relevantistic as to implication but classical as to negation, it has been dubbed, among many others, a ‘classical relevance logic.’ For KR, there have been known so far just two pretabular normal extensions. For these pretabular logics, no simple axiomatizations have yet been presented. In this paper, we offer some and show that they do the job. (...) We also introduce some Routley–Meyer semantic conditions for these axioms. All these may facilitate realizing our desire to discover other classical pretabular extensions over KR, if such extensions exist. (shrink)

We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for (...) finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers. (shrink)