The one-variable fragment of a first-order logic may be viewed as an “S5-like” modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases—notably, the modal counterparts $\mathrm {S5}$ and $\mathrm {MIPC}$ of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively—but a general approach, extending beyond first-order intermediate logics, has been lacking. To this end, a sufficient criterion is given in this paper for the one-variable fragment of a semantically defined first-order logic—spanning families of intermediate, substructural, many-valued, and modal logics—to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property.

We prove that the opposite of the category of coalgebras for the Vietoris endofunctor on the category of compact Hausdorff spaces is monadic over $\mathsf {Set}$. We deliver an analogous result for the upper, lower, and convex Vietoris endofunctors acting on the category of stably compact spaces. We provide axiomatizations of the associated (infinitary) varieties. This can be seen as a version of Jónsson–Tarski duality for modal algebras beyond the zero-dimensional setting.

The Baire algebra of a topological space X is the quotient of the algebra of all subsets of X modulo the meager sets. We show that this Boolean algebra can be endowed with a natural closure operator, resulting in a closure algebra which we denote $\mathbf {Baire}(X)$. We identify the modal logic of such algebras to be the well-known system $\mathsf {S5}$, and prove soundness and strong completeness for the cases where X is crowded and either completely metrizable and continuum-sized or locally compact Hausdorff. We also show that every extension of $\mathsf {S5}$ is the modal logic of a subalgebra of $\mathbf {Baire}(X)$, and that soundness and strong completeness also holds in the language with the universal modality.

A terminating sequent calculus for intuitionistic propositional logic is obtained by modifying the R$\supset $ rule of the labelled sequent calculus $\mathbf {G3I}$. This is done by adding a variant of the principle of a fortiori in the left-hand side of the premiss of the rule. In the resulting calculus, called ${\mathbf {G3I}}_{\mathbf {t}}$, derivability of any given sequent is directly decidable by root-first proof search, without any extra device such as loop-checking. In the negative case, the failed proof search gives a finite countermodel to the sequent on a reflexive, transitive, and Noetherian Kripke frame. As a byproduct, a direct proof of faithfulness of the embedding of intuitionistic logic into Grzegorcyk logic is obtained.

We introduce and study a class of betweenness algebras—Boolean algebras with binary operators, closely related to ternary frames with a betweenness relation. From various axioms for betweenness, we chose those that are most common, which makes our work applicable to a wide range of betweenness structures studied in the literature. On the algebraic side, we work with two operators of possibility and of sufficiency.

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.

Reasoning with quantifier expressions in natural language combines logical and arithmetical features, transcending strict divides between qualitative and quantitative. Our topic is this cooperation of styles as it occurs in common linguistic usage and its extension into the broader practice of natural language plus ‘grassroots mathematics’.

We begin with a brief review of $\mathsf {FO}(\#)$, first-order logic with counting operators and cardinality comparisons. This system is known to be of very high complexity, and drowns out finer aspects of the combination of logic and counting. We therefore move to a small fragment that can represent numerical syllogisms and basic reasoning about comparative size: monadic first-order logic with counting, $\mathsf {MFO}(\#)$. We provide normal forms that allow for axiomatization, determine which arithmetical notions can be defined on finite and on infinite models, and conversely, we discuss which logical notions can be defined out of purely arithmetical ones, and what sort of (non-)classical logics can be induced.

Next, we investigate a series of strengthenings of $\mathsf {MFO}(\#)$, again using normal form methods. The monadic second-order version is close, in a precise sense, to additive Presburger Arithmetic, while versions with the natural device of tuple counting take us to Diophantine equations, making the logic undecidable. We also define a system $\mathsf {ML}(\#)$ that combines basic modal logic over binary accessibility relations with counting, needed to formulate ubiquitous reasoning patterns such as the Pigeonhole Principle. We prove decidability of $\mathsf {ML}(\#)$, and provide a new kind of bisimulation matching the expressive power of the language.

As a complement to the fragment approach pursued here, we also discuss two other ways of lowering the complexity of $\mathsf {FO}(\#)$ by changing the semantics of counting in natural ways. A first approach replaces cardinalities by abstract but well-motivated values of ‘mass’ or other mereological aggregating notions. A second approach keeps the cardinalities but generalizes the meaning of counting to work in models that allow dependencies between variables.

Finally, we return to our starting point in natural language, confronting the architecture of our formal systems with linguistic quantifier vocabulary and syntax, as well as with natural reasoning modules such as the monotonicity calculus. In addition to these encounters with formal semantics, we discuss the role of counting in semantic evaluation procedures for quantifier expressions and determine, for instance, which binary quantifiers are computable by finite ‘semantic automata’. We conclude with some general thoughts on yet further entanglements of logic and counting in formal systems, on rethinking the qualitative/quantitative divide, and on connecting our analysis to empirical findings in cognitive science.

Traditionally, the formulae in modal logic express properties of possible worlds. Prior introduced “egocentric” logics that capture properties of agents rather than of possible worlds. In such a setting, the article proposes the modality “know how to tell apart” and gives a complete logical system describing the interplay between this modality and the knowledge modality. An important contribution of this work is a new matrix-based technique for proving completeness theorems in an egocentric setting.

This paper proves the finite axiomatizability of transitive modal logics of finite depth and finite width w.r.t. proper-successor-equivalence. The frame condition of the latter requires, in a rooted transitive frame, a finite upper bound of cardinality for antichains of points with different sets of proper successors. The result generalizes Rybakov’s result of the finite axiomatizability of extensions of $\mathbf {S4}$ of finite depth and finite width.

In this article we define a logical system called Hybrid Partial Type Theory ($\mathcal {HPTT}$). The system is obtained by combining William Farmer’s partial type theory with a strong form of hybrid logic. William Farmer’s system is a version of Church’s theory of types which allows terms to be non-denoting; hybrid logic is a version of modal logic in which it is possible to name worlds and evaluate expressions with respect to particular worlds. We motivate this combination of ideas in the introduction, and devote the rest of the article to defining, axiomatising, and proving a completeness result for $\mathcal {HPTT}$.

We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.

We develop a method for showing that various modal logics that are valid in their countably generated canonical Kripke frames must also be valid in their uncountably generated ones. This is applied to many systems, including the logics of finite width, and a broader class of multimodal logics of ‘finite achronal width’ that are introduced here.

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.

There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou’s probabilistic bisimilarity, whereas the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator $\mathcal {O}$, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the Zhou ordinal of $\mathbb {S}$, $\mathfrak {Z}(\mathbb {S})$. When $\mathfrak {Z}(\mathbb {S})=0$, $\mathbb {S}$ satisfies the Hennessy–Milner property. The second author proved the existence of an LMP $\mathbb {S}$ with $\mathfrak {Z}(\mathbb {S}) \geq 1$ and Zhou showed that there are LMPs having an infinite Zhou ordinal. In this paper we show that there are LMPs $\mathbb {S}$ over separable metrizable spaces having arbitrary large countable $\mathfrak {Z}(\mathbb {S})$ and that it is consistent with the axioms of $\mathit {ZFC}$ that there is such a process with an uncountable Zhou ordinal.

Sahlqvist theory is extended to the fragments of the intuitionistic propositional calculus that include the conjunction connective. This allows us to introduce a Sahlqvist theory of intuitionistic character amenable to arbitrary protoalgebraic deductive systems. As an application, we obtain a Sahlqvist theorem for the fragments of the intuitionistic propositional calculus that include the implication connective and for the extensions of the intuitionistic linear logic.

We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm {B}$, $\Delta (\mathrm {B})$, and $\Sigma (\mathrm {B})$ of formulas of modal arithmetic and study basic properties of them. Then, we prove several implications between the properties. In particular, among other things, we prove that for any consistent recursively enumerable extension T of $\mathbf {PA}(\mathbf {K})$ with $T \nvdash \Box \bot $, the $\Sigma (\mathrm {B})$-disjunction property, the $\Sigma (\mathrm {B})$-existence property, and the $\mathrm {B}$-existence property are pairwise equivalent. Moreover, we introduce the notion of the $\Sigma (\mathrm {B})$-soundness of theories and prove that for any consistent recursively enumerable extension of $\mathbf {PA}(\mathbf {K4})$, the modal disjunction property is equivalent to the $\Sigma (\mathrm {B})$-soundness.

The aim of this paper is to provide a complete Natural Kind Semantics for an Essentialist Theory of Kinds. The theory is formulated in two-sorted first order monadic modal logic with identity. The natural kind semantics is based on Rudolf Willes Theory of Concept Lattices. The semantics is then used to explain several consequences of the theory, including results about the specificity (species–genus) relations between kinds, the definitions of kinds in terms of genera and specific differences and the existence of negative kinds. First, I show under which conditions the Hierarchy principle, which has been subjected to counterexamples in the literature, holds. I also show that a different principle about the species–genus relations between kinds, namely Kant’s Law, follows from the essentialist theory. Second, I introduce two new operations for kinds and show that they can be used to provide traditional definitions of kinds in terms of genera and specific differences. Finally, I show that these operations of specific difference induce, for each kind, a uniquely specified contrary kind and a uniquely specified subcontrary kind, which can be used as semantic values for non-classical predicate negations of kind terms.

Propositional modal logic over relational frames is naturally extended with propositional quantifiers by letting them range over arbitrary sets of worlds of the relevant frame. This is also known as second-order propositional modal logic. The propositionally quantified modal logic of a class of relational frames is often not axiomatizable, although there are known exceptions, most notably the case of frames validating the strong modal logic $\mathrm {S5}$. Here, we develop new general methods with which many of the open questions in this area can be answered. We illustrate the usefulness of these methods by applying them to a range of examples, which provide a detailed picture of which normal modal logics define classes of relational frames whose propositionally quantified modal logic is axiomatizable. We also apply these methods to establish new results in the multimodal case.

We investigate a recently devised polyhedral semantics for intermediate logics, in which formulas are interpreted in n-dimensional polyhedra. An intermediate logic is polyhedrally complete if it is complete with respect to some class of polyhedra. The first main result of this paper is a necessary and sufficient condition for the polyhedral completeness of a logic. This condition, which we call the Nerve Criterion, is expressed in terms of Alexandrov’s notion of the nerve of a poset. It affords a purely combinatorial characterisation of polyhedrally complete logics. Using the Nerve Criterion we show, easily, that there are continuum many intermediate logics that are not polyhedrally complete but which have the finite model property. We also provide, at considerable combinatorial labour, a countably infinite class of logics axiomatised by the Jankov–Fine formulas of ‘starlike trees’ all of which are polyhedrally complete. The polyhedral completeness theorem for these ‘starlike logics’ is the second main result of this paper.

This is the second part of a two-part series on the logic of hyperlogic, a formal system for regimenting metalogical claims in the object language (even within embedded environments). Part A provided a minimal logic for hyperlogic that is sound and complete over the class of all models. In this part, we extend these completeness results to stronger logics that are sound and complete over restricted classes of models. We also investigate the logic of hyperlogic when the language is enriched with hyperintensional operators such as counterfactual conditionals and belief operators.