Bochvar algebras consist of the quasivariety $\mathsf {BCA}$ playing the role of equivalent algebraic semantics for Bochvar (external) logic, a logical formalism introduced by Bochvar [4] in the realm of (weak) Kleene logics. In this paper, we provide an algebraic investigation of the structure of Bochvar algebras. In particular, we prove a representation theorem based on Płonka sums and investigate the lattice of subquasivarieties, showing that Bochvar (external) logic has only one proper extension (apart from classical logic), algebraized by the subquasivariety $\mathsf {NBCA}$ of $\mathsf {BCA}$. Furthermore, we address the problem of (passive) structural completeness ((P)SC) for each of them, showing that $\mathsf {NBCA}$ is SC, while $\mathsf {BCA}$ is not even PSC. Finally, we prove that both $\mathsf {BCA}$ and $\mathsf {NBCA}$ enjoy the amalgamation property (AP).

In this paper we consider the classes of all continuous $\mathcal {L}$-(pre-)structures for a continuous first-order signature $\mathcal {L}$. We characterize the moduli of continuity for which the classes of finite, countable, or all continuous $\mathcal {L}$-(pre-)structures have the amalgamation property. We also characterize when Urysohn continuous $\mathcal {L}$-(pre)-structures exist, establish that certain classes of finite continuous $\mathcal {L}$-structures are countable Fraïssé classes, prove the coherent EPPA for these classes of finite continuous $\mathcal {L}$-structures, and show that actions by automorphisms on finite $\mathcal {L}$-structures also form a Fraïssé class. As consequences, we have that the automorphism group of the Urysohn continuous $\mathcal {L}$-structure is a universal Polish group and that Hall’s universal locally finite group is contained in the automorphism group of the Urysohn continuous $\mathcal {L}$-structure as a dense subgroup.

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 investigate whether ordinary quantification over objects is an extensional phenomenon, or rather creates non-extensional contexts; each claim having been propounded by prominent philosophers. It turns out that the question only makes sense relative to a background theory of syntax and semantics (here called a grammar) that goes well beyond the inductive definition of formulas and the recursive definition of satisfaction. Two schemas for building quantificational grammars are developed, one that invariably constructs extensional grammars (in which quantification, in particular, thus behaves extensionally) and another that only generates non-extensional grammars (and in which quantification is responsible for the failure of extensionality). We then ask whether there are reasons to favor one of these grammar schemas over the other, and examine an argument according to which the proper formalization of deictic utterances requires adoption of non-extensional grammars.

We study a version of the Craig interpolation theorem formulated in the framework of the theory of institutions. This formulation proved crucial in the development of a number of key results concerning foundations of software specification and formal development. We investigate preservation of interpolation properties under institution extensions by new models and sentences. We point out that some interpolation properties remain stable under such extensions, even if quite arbitrary new models and sentences are permitted. We give complete characterisations of such situations for institution extensions by new models, by new sentences, as well as by new models and sentences, respectively.

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.

This paper initiates the reverse mathematics of social choice theory, studying Arrow’s impossibility theorem and related results including Fishburn’s possibility theorem and the Kirman–Sondermann theorem within the framework of reverse mathematics. We formalise fundamental notions of social choice theory in second-order arithmetic, yielding a definition of countable society which is tractable in ${\mathsf {RCA}}_0$. We then show that the Kirman–Sondermann analysis of social welfare functions can be carried out in ${\mathsf {RCA}}_0$. This approach yields a proof of Arrow’s theorem in ${\mathsf {RCA}}_0$, and thus in $\mathrm {PRA}$, since Arrow’s theorem can be formalised as a $\Pi ^0_1$ sentence. Finally we show that Fishburn’s possibility theorem for countable societies is equivalent to ${\mathsf {ACA}}_0$ over ${\mathsf {RCA}}_0$.

We show that the conceptual distance between any two theories of first-order logic is the same as the generator distance between their Lindenbaum–Tarski algebras of concepts. As a consequence of this, we show that, for any two arbitrary mathematical structures, the generator distance between their meaning algebras (also known as cylindric set algebras) is the same as the conceptual distance between their first-order logic theories. As applications, we give a complete description for the distances between meaning algebras corresponding to structures having at most three elements and show that this small network represents all the possible conceptual distances between complete theories. As a corollary of this, we will see that there are only two non-trivial structures definable on three-element sets up to conceptual equivalence (i.e., up to elementary plus definitional equivalence).

We prove an isomorphism theorem between the canonical denotation systems for large natural numbers and large countable ordinal numbers, linking two fundamental concepts in Proof Theory. The first one is fast-growing hierarchies. These are sequences of functions on $\mathbb {N}$ obtained through processes such as the ones that yield multiplication from addition, exponentiation from multiplication, etc. and represent the canonical way of speaking about large finite numbers. The second one is ordinal collapsing functions, which represent the best-known method of describing large computable ordinals.

We observe that fast-growing hierarchies can be naturally extended to functors on the categories of natural numbers and of linear orders. The isomorphism theorem asserts that the categorical extensions of binary fast-growing hierarchies to ordinals are isomorphic to denotation systems given by cardinal collapsing functions. As an application of this fact, we obtain a restatement of the subsystem $\Pi ^1_1$-${\mathsf {CA_0}}$ of analysis as a higher-type well-ordering principle asserting that binary fast-growing hierarchies preserve well-foundedness.

Due to Gödel’s incompleteness results, the categoricity of a sufficiently rich mathematical theory and the semantic completeness of its underlying logic are two mutually exclusive ideals. For first- and second-order logics we obtain one of them with the cost of losing the other. In addition, in both these logics the rules of deduction for their quantifiers are non-categorical. In this paper I examine two recent arguments—Warren [43] and Murzi and Topey [30]—for the idea that the natural deduction rules for the first-order universal quantifier are categorical, i.e., they uniquely determine its semantic intended meaning. Both of them make use of McGee’s open-endedness requirement and the second one uses in addition Garson’s [19] local models for defining the validity of these rules. I argue that the success of both these arguments is relative to their semantic or infinitary assumptions, which could be easily discharged if the introduction rule for the universal quantifier is taken to be an infinitary rule, i.e., non-compact. Consequently, I reconsider the use of the $\omega $-rule and I show that the addition of the $\omega $-rule to the standard formalizations of first-order logic is categorical. In addition, I argue that the open-endedness requirement does not make the first-order Peano Arithmetic categorical and I advance an argument for its categoricity based on the inferential conservativity requirement.

On the basis of Poincaré and Weyl’s view of predicativity as invariance, we develop an extensive framework for predicative, type-free first-order set theory in which $\Gamma _0$ and much bigger ordinals can be defined as von Neumann ordinals. This refutes the accepted view of $\Gamma _0$ as the “limit of predicativity”.

We investigate degree of satisfiability questions in the context of Heyting algebras and intuitionistic logic. We classify all equations in one free variable with respect to finite satisfiability gap, and determine which common principles of classical logic in multiple free variables have finite satisfiability gap. In particular we prove that, in a finite non-Boolean Heyting algebra, the probability that a randomly chosen element satisfies $x \vee \neg x = \top $ is no larger than $\frac {2}{3}$. Finally, we generalize our results to infinite Heyting algebras, and present their applications to point-set topology, black-box algebras, and the philosophy of logic.

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.

Let $\mathscr {C}$ be a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Łoś–Tarski Theorem from classical model theory implies that $\mathscr {C}$ is definable in first-order logic by a sentence $\varphi $ if and only if $\mathscr {C}$ has a finite set of forbidden induced finite subgraphs. This result provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrub-depth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from $\varphi $ the corresponding forbidden induced subgraphs. This machinery fails on finite graphs as shown by our results:

• – There is a class $\mathscr {C}$ of finite graphs that is definable in first-order logic and closed under induced subgraphs but has no finite set of forbidden induced subgraphs.

• – Even if we only consider classes $\mathscr {C}$ of finite graphs that can be characterized by a finite set of forbidden induced subgraphs, such a characterization cannot be computed from a first-order sentence $\varphi $ that defines $\mathscr {C}$ and the size of the characterization cannot be bounded by $f(|\varphi |)$ for any computable function f.

Besides their importance in graph theory, the above results also significantly strengthen similar known theorems for arbitrary structures.

We present a novel treatment of set theory in a four-valued paraconsistent and paracomplete logic, i.e., a logic in which propositions can be both true and false, and neither true nor false. Our approach is a significant departure from previous research in paraconsistent set theory, which has almost exclusively been motivated by a desire to avoid Russell’s paradox and fulfil naive comprehension. Instead, we prioritise setting up a system with a clear ontology of non-classical sets, which can be used to reason informally about incomplete and inconsistent phenomena, and is sufficiently similar to ${\mathrm {ZFC}}$ to enable the development of interesting mathematics.

We propose an axiomatic system ${\mathrm {BZFC}}$, obtained by analysing the ${\mathrm {ZFC}}$-axioms and translating them to a four-valued setting in a careful manner, avoiding many of the obstacles encountered by other attempted formalizations. We introduce the anti-classicality axiom postulating the existence of non-classical sets, and prove a surprising results stating that the existence of a single non-classical set is sufficient to produce any other type of non-classical set.

Our theory is naturally bi-interpretable with ${\mathrm {ZFC}}$, and provides a philosophically satisfying view in which non-classical sets can be seen as a natural extension of classical ones, in a similar way to the non-well-founded sets of Peter Aczel [1].

Finally, we provide an interesting application concerning Tarski semantics, showing that the classical definition of the satisfaction relation yields a logic precisely reflecting the non-classicality in the meta-theory.

We generalise the properties $\mathsf {OP}$, $\mathsf {IP}$, k-$\mathsf {TP}$, $\mathsf {TP}_{1}$, k-$\mathsf {TP}_{2}$, $\mathsf {SOP}_{1}$, $\mathsf {SOP}_{2}$, and $\mathsf {SOP}_{3}$ to positive logic, and prove various implications and equivalences between them. We also provide a characterisation of stability in positive logic in analogy with the one in full first-order logic, both on the level of formulas and on the level of theories. For simple theories there are the classically equivalent definitions of not having $\mathsf {TP}$ and dividing having local character, which we prove to be equivalent in positive logic as well. Finally, we show that a thick theory T has $\mathsf {OP}$ iff it has $\mathsf {IP}$ or $\mathsf {SOP}_{1}$ and that T has $\mathsf {TP}$ iff it has $\mathsf {SOP}_{1}$ or $\mathsf {TP}_{2}$, analogous to the well-known results in full first-order logic where $\mathsf {SOP}_{1}$ is replaced by $\mathsf {SOP}$ in the former and by $\mathsf {TP}_{1}$ in the latter. Our proofs of these final two theorems are new and make use of Kim-independence.

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.

The smooth development of large parts of mathematics hinges on the idea that some sets are ‘small’ or ‘negligible’ and can therefore be ignored for a given purpose. The perhaps most famous smallness notion, namely ‘measure zero’, originated with Lebesgue, while a second smallness notion, namely ‘meagre’ or ‘first category’, originated with Baire around the same time. The associated Baire category theorem is a central result governing the properties of meagre (and related) sets, while the same holds for Tao’s pigeonhole principle for measure spaces and measure zero sets. In this paper, we study these theorems in Kohlenbach’s higher-order Reverse Mathematics, identifying a considerable number of equivalent and robust theorems. The latter involve most basic properties of semi-continuous and pointwise discontinuous functions, Blumberg’s theorem, Riemann integration, and Volterra’s early work circa 1881. All the aforementioned theorems fall (far) outside of the Big Five of Reverse Mathematics, and we investigate natural restrictions like Baire 1 and quasi-continuity that make these theorems provable again in the Big Five (or similar). Finally, despite the fundamental differences between measure and category, the proofs of our equivalences turn out to be similar.

A field K in a ring language $\mathcal {L}$ is finitely undecidable if $\mbox {Cons}(T)$ is undecidable for every nonempty finite $T \subseteq {\mathtt{Th}}(K; \mathcal {L})$. We extend a construction of Ziegler and (among other results) use a first-order classification of Anscombe and Jahnke to prove every NIP henselian nontrivially valued field is finitely undecidable. We conclude (assuming the NIP Fields Conjecture) that every NIP field is finitely undecidable. This work is drawn from the author’s PhD thesis [48, Chapter 3].