Abstract algebraic logic is a theory that provides general tools for the algebraic study of arbitrary propositional logics. According to this theory, every logic ${\cal L}$ is associated with a matrix semantics $Mo{d^{\rm{*}}}{\cal L}$. This article is a contribution to the systematic study of the so-called truth sets of the matrices in $Mo{d^{\rm{*}}}{\cal L}$. In particular, we show that the fact that the truth sets of $Mo{d^{\rm{*}}}{\cal L}$ can be defined by means of equations with universally quantified parameters is captured by an order-theoretic property of the Leibniz operator restricted to deductive filters of ${\cal L}$. This result was previously known for equational definability without parameters. Similarly, it was known that the truth sets of $Mo{d^{\rm{*}}}{\cal L}$ are implicitly definable if and only if the Leibniz operator is injective on deductive filters of ${\cal L}$ over every algebra. However, it was an open problem whether the injectivity of the Leibniz operator transfers from the theories of ${\cal L}$ to its deductive filters over arbitrary algebras. We show that this is the case for logics expressed in a countable language, and that it need not be true in general. Finally we consider an intermediate condition on the truth sets in $Mo{d^{\rm{*}}}{\cal L}$ that corresponds to the order-reflection of the Leibniz operator.

The paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

We analyze the behaviour of declarations of independence between existential quantifiers in quantifier prefixes of Independence-Friendly (IF) sentences; we give a syntactical criterion to decide whether a sentence beginning with such prefix exists, such that its truth values may be affected by removal of the declaration of independence. We extend the result also to equilibrium semantics values for undetermined IF sentences.

The main theorem defines a schema of sound and recursive inference rules; we show more explicitly what happens for some simple special classes of sentences.

In the last section, we extend the main result beyond the scope of prenex sentences, in order to give a proof of the fact that the fragment of IF sentences with knowledge memory has only first-order expressive power.

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid (i) to which properties of theories result in the presence of which rules of inference, and (ii) to restrictions on the sets of formulas to which the rules may be employed, restrictions determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck.

The large-structure tools of cohomology including toposes and derived categories stay close to arithmetic in practice, yet published foundations for them go beyond ZFC in logical strength. We reduce the gap by founding all the theorems of Grothendieck’s SGA, plus derived categories, at the level of Finite-Order Arithmetic, far below ZFC. This is the weakest possible foundation for the large-structure tools because one elementary topos of sets with infinity is already this strong.

Counterexamples to reassurance relative to a “less inconsistent” relation between models of the logic of paradox are provided. Another relation, designed to fix the problem in logic without equality, is introduced and discussed in connection with the issue of classical recapture.

We consider a simple modal logic whose nonmodal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of (e.g.) T, S4, and S5, such logics are useful, as shown in previous work by Baltag, Coecke, and the first author, for encoding and reasoning about information and misinformation in multiagent systems. For the propositional-only fragment of such a dynamic epistemic logic, we present an algebraic semantics, using lattices with agent-indexed families of adjoint pairs of operators, and a cut-free sequent calculus. The calculus exploits operators on sequents, in the style of “nested” or “tree-sequent” calculi; cut-admissibility is shown by constructive syntactic methods. The applicability of the logic is illustrated by reasoning about the muddy children puzzle, for which the calculus is augmented with extra rules to express the facts of the muddy children scenario.

Modal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics.

Kripke’s theory of truth offered a trivalent semantics for a language which, like English, contains a truth predicate and means of self-reference; but it did so by severely restricting the expressive power of the logic. In Kripke’s analysis, the Liar (e.g., This very sentence is not true) receives the indeterminate truth value, but this fact cannot be expressed in the language; by contrast, it is straightforward to say in English that the Liar is something other than true. Kripke’s theory also fails to handle the Strengthened Liar, which can be expressed in English as: This very sentence is something other than true. We develop a theory which seeks to overcome these difficulties, and is based on a detailed analysis of some of the linguistic means by which the Strengthened Liar can be expressed in English. In particular, we propose to take literally the quantificational form of the negative expression something other than true. Like other quantifiers, it may have different implicit domain restrictions, which give rise to a variety of negations of different strengths (e.g., something other than true among the values {0, 1}, or among {0, 1, 2}, etc). This analysis naturally leads to a logic with as many truth values as there are ordinals—a conclusion reached independently by Cook (2008a). We develop the theory within a generalization of the Strong Kleene Logic, augmented with negations that each have a nonmonotonic semantics. We show that fixed points can be constructed for our logic, and that it enjoys a limited form of ‘expressive completeness’. Finally, we discuss the relation between our theory and various alternatives, including one in which the word true (rather than negation) is semantically ambiguous, and gives rise to a hierarchy of truth predicates of increasing strength.

Mathematicians prove theorems in a semi-formal setting, providing what we’ll call informal proofs. There are various philosophical reasons not to reduce informal provability to formal provability within some appropriate axiomatic theory (Leitgeb, 2009; Marfori, 2010; Tanswell, 2015), but the main worry is that we seem committed to all instances of the so-called reflection schema: B(φ) → φ (where B stands for the informal provability predicate). Yet, adding all its instances to any theory for which Löb’s theorem for B holds leads to inconsistency.

Currently existing approaches (Shapiro, 1985; Horsten, 1996, 1998) to formalizing the properties of informal provability avoid contradiction at a rather high price. They either drop one of the Hilbert-Bernays conditions for the provability predicate, or use a provability operator that cannot consistently be treated as a predicate.

Inspired by (Kripke, 1975), we investigate the strategy which changes the underlying logic and treats informal provability as a partial notion. We use non-deterministic matrices to develop a three-valued logic of informal provability, which avoids some of the above mentioned problems.

We present an extension of the basic revision theory of circular definitions with a unary operator, □. We present a Fitch-style proof system that is sound and complete with respect to the extended semantics. The logic of the box gives rise to a simple modal logic, and we relate provability in the extended proof system to this modal logic via a completeness theorem, using interpretations over circular definitions, analogous to Solovay’s completeness theorem for GL using arithmetical interpretations. We adapt our proof to a special class of circular definitions as well as to the first-order case.

The logic of Conditional Beliefs (CDL) has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. In this article both the semantics and the proof theory for this logic are studied. First, a natural semantics for CDL is defined in terms of neighbourhood models, a multi-agent generalisation of Lewis’ spheres models, and it is shown that the axiomatization of CDL is sound and complete with respect to this semantics. Second, it is shown that the neighbourhood semantics is equivalent to the original one defined in terms of plausibility models, by means of a direct correspondence between the two types of models. On the basis of neighbourhood semantics, a labelled sequent calculus for CDL is obtained. The calculus has strong proof-theoretic properties, in particular admissibility of contraction and cut, and it provides a decision procedure for the logic. Furthermore, its semantic completeness is used to obtain a constructive proof of the finite model property of the logic. Finally, it is shown that other doxastic operators can be easily captured within neighbourhood semantics. This fact provides further evidence of the naturalness of neighbourhood semantics for the analysis of epistemic/doxastic notions.

The prevalent interpretation of Gödel’s Second Theorem states that a sufficiently adequate and consistent theory does not prove its consistency. It is however not entirely clear how to justify this informal reading, as the formulation of the underlying mathematical theorem depends on several arbitrary formalisation choices. In this paper I examine the theorem’s dependency regarding Gödel numberings. I introduce deviant numberings, yielding provability predicates satisfying Löb’s conditions, which result in provable consistency sentences. According to the main result of this paper however, these “counterexamples” do not refute the theorem’s prevalent interpretation, since once a natural class of admissible numberings is singled out, invariance is maintained.

Recent accounts of actual causation are stated in terms of extended causal models. These extended causal models contain two elements representing two seemingly distinct modalities. The first element are structural equations which represent the “(causal) laws” or mechanisms of the model, just as ordinary causal models do. The second element are ranking functions which represent normality or typicality. The aim of this paper is to show that these two modalities can be unified. I do so by formulating two constraints under which extended causal models with their two modalities can be subsumed under so called “counterfactual models” which contain just one modality. These two constraints will be formally precise versions of Lewis’ (1979) familiar “system of weights or priorities” governing overall similarity between possible worlds.

In this note we derive Robinson’s Arithmetic from Hume’s Principle in the context of very weak theories of classes and relations.

We present four classical theories of counterpossibles that combine modalities and counterfactuals. Two theories are anti-vacuist and forbid vacuously true counterfactuals, two are quasi-vacuist and allow counterfactuals to be vacuously true when their antecedent is not only impossible, but also inconceivable. The theories vary on how they restrict the interaction of modalities and counterfactuals. We provide a logical cartography with precise acceptable boundaries, illustrating to what extent nonvacuism about counterpossibles can be reconciled with classical logic.

It is well known that Gödel’s incompleteness theorems hold for ∑1-definable theories containing Peano arithmetic. We generalize Gödel’s incompleteness theorems for arithmetically definable theories. First, we prove that every ∑n+1-definable ∑n-sound theory is incomplete. Secondly, we generalize and improve Jeroslow and Hájek’s results. That is, we prove that every consistent theory having ∏n+1 set of theorems has a true but unprovable ∏n sentence. Lastly, we prove that no ∑n+1-definable ∑n -sound theory can prove its own ∑n-soundness. These three results are generalizations of Rosser’s improvement of the first incompleteness theorem, Gödel’s first incompleteness theorem, and the second incompleteness theorem, respectively.

Although much technical and philosophical attention has been given to relevance logics, the notion of relevance itself is generally left at an intuitive level. It is difficult to find in the literature an explicit account of relevance in formal reasoning. In this article I offer a formal explication of the notion of relevance in deductive logic and argue that this notion has an interesting place in the study of classical logic. The main idea is that a premise is relevant to an argument when it contributes to the validity of that argument. I then argue that the sequents which best embody this ideal of relevance are the so-called perfect sequents—that is, sequents which are valid but have no proper subsequents that are valid. Church’s theorem entails that there is no recursively axiomatizable proof-system that proves all and only the perfect sequents, so the project that emerges from studying perfection in classical logic is not one of finding a perfect subsystem of classical logic, but is rather a comparative study of classifying subsystems of classical logic according to how well they approximate the ideal of perfection.

Some theorists have developed formal approaches to truth that depend on counterexamples to the structural rules of contraction. Here, we study such approaches, with an eye to helping them respond to a certain kind of objection. We define a contractive relative of each noncontractive relation, for use in responding to the objection in question, and we explore one example: the contractive relative of multiplicative-additive affine logic with transparent truth, or maalt.

A typical first stab at explicating the thesis of physicalism is this: physicalism is true iff every fact about the world is entailed by the conjunction of physical facts. The same holds, mutatis mutandis, for other hypotheses about the fundamental nature of our world. But it has been recognized that this would leave such hypotheses without the fighting chance that they deserve: certain negative truths, like the truth (if it is one) that there are no angels, are not entailed by the physical facts, but nonetheless do not threaten physicalism. A plausible remedy that has been suggested by Jackson and Chalmers is that physicalism boils down to the thesis that every truth is entailed by the conjunction of the physical facts prefixed by a “that’s it” or “totality” operator. To evaluate this suggestion, we need to know what that operator means, and—since the truth of physicalism hinges on what is entailed by a totality claim—what its logic is. That is, we need to understand the logic of totality, or total logic. In this paper, I add a totality operator to the language of propositional logic and present a model theory for it, building on a suggestion by Chalmers and Jackson. I then prove determination results for a number of different systems.