This essay proposes a procedural interpretation of negative information in terms of split negation as procedural prohibition. Information frames and models are introduced, with negation defined as the implication of bottom, 0. A method for extracting the procedures prohibited by complex formulas is outlined, and the relationship between types of prohibited procedures is identified. Definitions of negation types in terms of the implication of 0 on an informational interpretation have been criticized. This criticism turns on the definitions creating a purportedly unnatural asymmetry between positive and negative information. It is demonstrated below that a strong asymmetry between positive and negative information is in fact the case. As such, an asymmetry between positive and negative information is natural, and something that we should want an informational interpretation of negation to preserve.

The Generales Inquisitiones de Analysi Notionum et Veritatum is Leibniz’s most substantive work in the area of logic. Leibniz’s central aim in this treatise is to develop a symbolic calculus of terms that is capable of underwriting all valid modes of syllogistic and propositional reasoning. The present paper provides a systematic reconstruction of the calculus developed by Leibniz in the Generales Inquisitiones. We investigate the most significant logical features of this calculus and prove that it is both sound and complete with respect to a simple class of enriched Boolean algebras which we call auto-Boolean algebras. Moreover, we show that Leibniz’s calculus can reproduce all the laws of classical propositional logic, thus allowing Leibniz to achieve his goal of reducing propositional reasoning to algebraic reasoning about terms.

The Quantified argument calculus (Quarc) has received a lot of attention recently as an interesting system of quantified logic which eschews the use of variables and unrestricted quantification, but nonetheless achieves results similar to the Predicate calculus (PC) by employing quantifiers applied directly to predicates instead. Despite this noted similarity, the issue of the relationship between Quarc and PC has so far not been definitively resolved. We address this question in the present paper, and then expand upon that result.

Utilizing recent developments in structural proof theory, we develop a G3-style sequent calculus for Quarc and briefly demonstrate its structural properties. We put these properties to use immediately to construct direct proofs of the meta-theoretical properties of the system. We then incorporate an abstract (and, as we shall see, logical) predicate into the system in a way that preserves all the structural properties. This allows us to identify a system of Quarc which is deductively equivalent to PC, and also yields a constructive method of demonstrating the Craig interpolation theorem (which speaks in favor of the aforementioned predicate being logical). We further generalize this extension to develop a bivalent system of Quarc with defining clauses that still maintains all the desirable properties of a good proof system.

Sedlár and Vigiani [18] have developed an approach to propositional epistemic logics wherein (i) an agent’s beliefs are closed under relevant implication and (ii) the agent is located in a classical possible world (i.e., the non-modal fragment is classical). Here I construct first-order extensions of these logics using the non-Tarskian interpretation of the quantifiers introduced by Mares and Goldblatt [12], and later extended to quantified modal relevant logics by Ferenz [6]. Modular soundness and completeness are proved for constant domain semantics, using non-general frames with Mares–Goldblatt truth conditions. I further detail the relation between the demand that classical possible worlds have Tarskian truth conditions and incompleteness results in quantified relevant logics.

The article looks briefly at Feferman’s most sweeping claims about categorical foundations, focuses on narrower points raised in Berkeley, and asks some questions about Feferman’s own foundations. Among many different senses of foundations, the one that mathematics needs in practice is a recognized body of truths adequate to organize definitions and proofs. Finding concise principles of this kind has been a huge achievement by mathematicians and logicians. We put ZFC and categorical foundations both into this context.

It is customary to expect from a logical system that it can be algebraizable, in the sense that an algebraic companion of the deductive machinery can always be found. Since the inception of da Costa’s paraconsistent calculi, algebraic equivalents for such systems have been sought. It is known, however, that these systems are not self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok–Pigozzi. The same negative results hold for several systems of the hierarchy of paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Because of this, several systems belonging to this class of logics are only characterizable by semantics of a non-deterministic nature. This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs, by extending with rules several LFIs weaker than $C_1$ , thus obtaining the replacement property (that is, such LFIs turn out to be self-extensional). Moreover, these logics become algebraizable in the standard Lindenbaum–Tarski’s sense by a suitable variety of Boolean algebras extended with additional operations. The weakest LFI satisfying replacement presented here is called RmbC, which is obtained from the basic LFI called mbC. Some axiomatic extensions of RmbC are also studied. In addition, a neighborhood semantics is defined for such systems. It is shown that RmbC can be defined within the minimal bimodal non-normal logic $\mathbf {E} {\oplus } \mathbf {E}$ defined by the fusion of the non-normal modal logic E with itself. Finally, the framework is extended to first-order languages. RQmbC, the quantified extension of RmbC, is shown to be sound and complete w.r.t. the proposed algebraic semantics.

We present a new axiomatization of classical mereology in which the three components of the theory—ordering, composition, and decomposition principles—are neatly separated. The equivalence of our axiom system with other, more familiar systems is established by purely deductive methods, along with additional results on the relative strengths of the composition and decomposition axioms of each system.

This article provides an algebraic study of the propositional system $\mathtt {InqB}$ of inquisitive logic. We also investigate the wider class of $\mathtt {DNA}$-logics, which are negative variants of intermediate logics, and the corresponding algebraic structures, $\mathtt {DNA}$-varieties. We prove that the lattice of $\mathtt {DNA}$-logics is dually isomorphic to the lattice of $\mathtt {DNA}$-varieties. We characterise maximal and minimal intermediate logics with the same negative variant, and we prove a suitable version of Birkhoff’s classic variety theorems. We also introduce locally finite $\mathtt {DNA}$-varieties and show that these varieties are axiomatised by the analogues of Jankov formulas. Finally, we prove that the lattice of extensions of $\mathtt {InqB}$ is dually isomorphic to the ordinal $\omega +1$ and give an axiomatisation of these logics via Jankov $\mathtt {DNA}$-formulas. This shows that these extensions coincide with the so-called inquisitive hierarchy of [9].1

In his paper on the incompleteness theorems, Gödel seemed to say that a direct way of constructing a formula that says of itself that it is unprovable might involve a faulty circularity. In this note, it is proved that ‘direct’ self-reference can actually be used to prove his result.

Inferentialism claims that the rules for the use of an expression express its meaning without any need to invoke meanings or denotations for them. Logical inferentialism endorses inferentialism specifically for the logical constants. Harmonic inferentialism, as the term is introduced here, usually but not necessarily a subbranch of logical inferentialism, follows Gentzen in proposing that it is the introduction-rules which give expressions their meaning and the elimination-rules should accord harmoniously with the meaning so given. It is proposed here that the logical expressions are those which can be given schematic rules that lie in a specific sort of harmony, general-elimination (ge) harmony, resulting from applying a certain operation, the ge-procedure, to produce ge-rules in accord with the meaning defined by the I-rules. Griffiths (2014) claims that identity cannot be given such rules, concluding that logical inferentialists are committed to ruling identity a nonlogical expression. It is shown that the schematic rules for identity given in Read (2004), slightly amended, are indeed ge-harmonious, so confirming that identity is a logical notion.

Positive logics are $\{ \wedge , \vee , \to \}$-fragments of intermediate logics. It is clear that the positive fragment of $Int$ is not structurally complete. We give a description of all hereditarily structurally complete positive logics, while the question whether there is a structurally complete positive logic which is not hereditarily structurally complete, remains open.

This paper is a study of the opening section of Gentzen’s first publication of 1932, Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen, a text which shows the relevance of Hertz’s work of the 1920’s for the young Gentzen. In fact, Gentzen borrowed from Hertz the analysis of the notion of consequence, which was given in terms of the rules of thinning (Verdünnung) and cut (Schnitt) on sequents (there called “sentences”(Sätze)). Moreover, following Hertz again, he also judged it necessary to justify the forms of inference of the system by providing a semantics for them, so that it became possible to make precise the informal notion of consequence, and to show that the inference rules adopted are correct and sufficient.

We add propositional quantifiers to the propositional modal logic S4 and to the propositional intuitionistic logic H, introducing axiom schemes that are the natural analogs to axiom schemes typically used for first-order quantifiers in classical and intuitionistic logic. We show that the resulting logics are sound and complete for a topological semantics extending, in a natural way, the topological semantics for S4 and for H.

One way to study and understand the notion of truth is to examine principles that we are willing to associate with truth, often because they conform to a pre-theoretical or to a semi-formal characterization of this concept. In comparing different collections of such principles, one requires formally precise notions of inter-theoretic reduction that are also adequate to compare these conceptual aspects. In this work I study possible ways to make precise the relation of conceptual equivalence between notions of truth associated with collections of principles of truth. In doing so, I will consider refinements and strengthenings of the notion of relative truth-definability proposed by Fujimoto (2010): in particular I employ suitable variants of notions of equivalence of theories considered in Visser (2006) and Friedman & Visser (2014) to show that there are better candidates than mutual truth-definability for the role of sufficient condition for conceptual equivalence between the semantic notions associated with the theories. In the concluding part of the paper, I extend the techniques introduced in the first and show that there is a precise sense in which ramified truth (either disquotational or compositional) does not correspond to iterations of comprehension.

Admissible rules are shown to be conservatively preserved by the meet-combination of a wide class of logics. A basis is obtained for the resulting logic from bases given for the component logics, under mild conditions. A weak form of structural completeness is proved to be preserved by the combination. Decidability of the set of admissible rules is also shown to be preserved, with no penalty on the time complexity. Examples are provided for the meet-combination of intermediate and modal logics.

In this paper, using a propositional modal language extended with the window modality, we capture the first-order properties of various mereological theories. In this setting, $\Box \varphi $ reads all the parts (of the current object) are $\varphi $, interpreted on the models with a whole-part binary relation under various constraints. We show that all the usual mereological theories can be captured by modal formulas in our language via frame correspondence. We also correct a mistake in the existing completeness proof for a basic system of mereology by providing a new construction of the canonical model.

Stephen Read (2002, 2006) has recently discussed Bradwardine's theory of truth and defended it as an appropriate way to treat paradoxes such as the liar. In this paper, I discuss Read's formalisation of Bradwardine's theory of truth and provide a class of models for this theory. The models facilitate comparison of Bradwardine's theory with contemporary theories of truth.

Under a proper translation, the languages of propositional (and quantified relevant logic) with an absurdity constant are characterized as the fragments of first order logic preserved under (world-object) relevant directed bisimulations. Furthermore, the properties of pointed models axiomatizable by sets of propositional relevant formulas have a purely algebraic characterization. Finally, a form of the interpolation property holds for the relevant fragment of first order logic.

We introduce unification in first-order logic. In propositional logic, unification was introduced by S. Ghilardi, see Ghilardi (1997, 1999, 2000). He successfully applied it in solving systematically the problem of admissibility of inference rules in intuitionistic and transitive modal propositional logics. Here we focus on superintuitionistic predicate logics and apply unification to some old and new problems: definability of disjunction and existential quantifier, disjunction and existential quantifier under implication, admissible rules, a basis for the passive rules, (almost) structural completeness, etc. For this aim we apply modified specific notions, introduced in propositional logic by Ghilardi, such as projective formulas, projective unifiers, etc.

Unification in predicate logic seems to be harder than in the propositional case. Any definition of the key concept of substitution for predicate variables must take care of individual variables. We allow adding new free individual variables by substitutions (contrary to Pogorzelski & Prucnal (1975)). Moreover, since predicate logic is not as close to algebra as propositional logic, direct application of useful algebraic notions of finitely presented algebras, projective algebras, etc., is not possible.

This paper presents a proof system for discourse representation theoretic reasoning and dynamic predicate logical inference. It gives a sound and complete characterization of the dynamic declaration of discourse referents and the essentially indexical means to refer back to them. The indexical outlook upon discourse reference is argued to further our understanding of some issues deemed relevant both theoretically (philo-logically) and practically (computationally).