We take Carnap’s problem to be to what extent standard consequence relations in various formal languages fix the meaning of their logical vocabulary, alone or together with additional constraints on the form of the semantics. This paper studies Carnap’s problem for basic modal logic. Setting the stage, we show that neighborhood semantics is the most general form of compositional possible worlds semantics, and proceed to ask which standard modal logics (if any) constrain the box operator to be interpreted as in relational Kripke semantics. Except when restricted to finite domains, no modal logic characterizes exactly the Kripkean interpretations of $\Box $ . Moreover, we show that, in contrast with the case of first-order logic, the obvious requirement of permutation invariance is not adequate in the modal case. After pointing out some known facts about modal logics that nevertheless force the Kripkean interpretation, we focus on another feature often taken to embody the gist of modal logic: locality. We show that invariance under point-generated subframes (properly defined) does single out the Kripkean interpretations, but only among topological interpretations, not in general. Finally, we define a notion of bisimulation invariance—another aspect of locality—that, together with a reasonable closure condition, gives the desired general result. Along the way, we propose a new perspective on normal neighborhood frames as filter frames, consisting of a set of worlds equipped with an accessibility relation, and a free filter at every world.

Satisfaction systems and reductions between them are presented as an appropriate context for analyzing the satisfiability and the validity problems. The notion of reduction is generalized in order to cope with the meet-combination of logics. Reductions between satisfaction systems induce reductions between the respective satisfiability problems and (under mild conditions) also between their validity problems. Sufficient conditions are provided for relating satisfiability problems to validity problems. Reflection results for decidability in the presence of reductions are established. The validity problem in the meet-combination is proved to be decidable whenever the validity problem for the components are decidable. Several examples are discussed, namely, involving modal and intuitionistic logics, as well as the meet-combination of $\textrm {K}$ modal logic and intuitionistic logic.

Frege’s definition of the real numbers, as envisaged in the second volume of Grundgesetze der Arithmetik, is fatally flawed by the inconsistency of Frege’s ill-fated Basic Law V. We restate Frege’s definition in a consistent logical framework and investigate whether it can provide a logical foundation of real analysis. Our conclusion will deem it doubtful that such a foundation along the lines of Frege’s own indications is possible at all.

We study the logic of so-called lexicographic or priority merge for multi-agent plausibility models. We start with a systematic comparison between the logical behavior of priority merge and the more standard notion of pooling through intersection, used to define, for instance, distributed knowledge. We then provide a sound and complete axiomatization of the logic of priority merge, as well as a proof theory in labeled sequents that admits cut. We finally study Moorean phenomena and define a dynamic resolution operator for priority merge for which we also provide a complete set of reduction axioms.

This paper collects and presents unpublished notes of Kurt Gödel concerning the field of many-valued logic. In order to get a picture as complete as possible, both formal and philosophical notes, transcribed from the Gabelsberger shorthand system, are included.

I provide an analysis of sentences of the form ‘To be F is to be G’ in terms of exact truth-maker semantics—an approach that identifies the meanings of sentences with the states of the world directly responsible for their truth-values. Roughly, I argue that these sentences hold just in case that which makes something F also makes it G. This approach is hyperintensional and possesses desirable logical and modal features. In particular, these sentences are reflexive, transitive, and symmetric, and if they are true, then they are necessarily true, and it is necessary that all and only Fs are Gs. I motivate my account over Correia and Skiles’ [11] prominent alternative and close by defining an irreflexive and asymmetric notion of analysis in terms of the symmetric and reflexive notion.

In previous work, the author has shown that $\Pi ^1_1$ -induction along $\mathbb N$ is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of Girard’s dilators, which are particularly uniform transformations of well orders. The present paper works on the next type level and considers uniform transformations of dilators, which are called 2-ptykes. We show that $\Pi ^1_2$ -induction along $\mathbb N$ is equivalent to the existence of fixed points for all 2-ptykes that satisfy a certain normality condition. Beyond this specific result, the paper paves the way for the analysis of further $\Pi ^1_4$ -statements in terms of well ordering principles.

We define a fragment of monadic infinitary second-order logic corresponding to an abstract separation property. We use this to define the concept of a separation subclass. We use model theoretic techniques and games to show that separation subclasses whose axiomatisations are recursively enumerable in our second-order fragment can also be recursively axiomatised in their original first-order language. We pin down the expressive power of this formalism with respect to first-order logic, and investigate some questions relating to decidability and computational complexity. As applications of these results, by showing that certain classes can be straightforwardly defined as separation subclasses, we obtain first-order axiomatisability results for these classes. In particular we apply this technique to graph colourings and a class of partial algebras arising from separation logic.

The Jordan decomposition theorem states that every function $f \colon \, [0,1] \to \mathbb {R}$ of bounded variation can be written as the difference of two non-decreasing functions. Combining this fact with a result of Lebesgue, every function of bounded variation is differentiable almost everywhere in the sense of Lebesgue measure. We analyze the strength of these theorems in the setting of reverse mathematics. Over $\mathsf {RCA}_{0}$ , a stronger version of Jordan’s result where all functions are continuous is equivalent to $\mathsf {ACA}_0$ , while the version stated is equivalent to ${\textsf {WKL}}_{0}$ . The result that every function on $[0,1]$ of bounded variation is almost everywhere differentiable is equivalent to ${\textsf {WWKL}}_{0}$ . To state this equivalence in a meaningful way, we develop a theory of Martin–Löf randomness over $\mathsf {RCA}_0$ .

We prove that the two-variable fragment of first-order logic has the weak Beth definability property. This makes the two-variable fragment a natural logic separating the weak and the strong Beth properties since it does not have the strong Beth definability property.

We prove that the existence of a measurable cardinal is equivalent to the existence of a normal space whose modal logic coincides with the modal logic of the Kripke frame isomorphic to the powerset of a two element set.

We investigate the uniform computational content of the open and clopen Ramsey theorems in the Weihrauch lattice. While they are known to be equivalent to $\mathrm {ATR_0}$ from the point of view of reverse mathematics, there is not a canonical way to phrase them as multivalued functions. We identify eight different multivalued functions (five corresponding to the open Ramsey theorem and three corresponding to the clopen Ramsey theorem) and study their degree from the point of view of Weihrauch, strong Weihrauch, and arithmetic Weihrauch reducibility. In particular one of our functions turns out to be strictly stronger than any previously studied multivalued functions arising from statements around $\mathrm {ATR}_0$ .

We explore the problems that confront any attempt to explain or explicate exactly what a primitive logical rule of inference is, or consists in. We arrive at a proposed solution that places a surprisingly heavy load on the prospect of being able to understand and deal with specifications of rules that are essentially self-referring. That is, any rule $\rho $ is to be understood via a specification that involves, embedded within it, reference to rule $\rho $ itself. Just how we arrive at this position is explained by reference to familiar rules as well as less familiar ones with unusual features. An inquiry of this kind is surprisingly absent from the foundations of inferentialism—the view that meanings of expressions (especially logical ones) are to be characterized by the rules of inference that govern them.

I show that the logic $\textsf {TJK}^{d+}$ , one of the strongest logics currently known to support the naive theory of truth, is obtained from the Kripke semantics for constant domain intuitionistic logic by (i) dropping the requirement that the accessibility relation is reflexive and (ii) only allowing reflexive worlds to serve as counterexamples to logical consequence. In addition, I provide a simplified natural deduction system for $\textsf {TJK}^{d+}$ , in which a restricted form of conditional proof is used to establish conditionals.

We consider the modality “ $\varphi $ is true in every $\sigma $ -centered forcing extension,” denoted $\square \varphi $ , and its dual “ $\varphi $ is true in some $\sigma $ -centered forcing extension,” denoted $\lozenge \varphi $ (where $\varphi $ is a statement in set theory), which give rise to the notion of a principle of $\sigma $ -centered forcing. We prove that if ZFC is consistent, then the modal logic of $\sigma $ -centered forcing, i.e., the ZFC-provable principles of $\sigma $ -centered forcing, is exactly $\mathsf {S4.2}$ . We also generalize this result to other related classes of forcing.

We prove a number of elementary facts about computability in partial combinatory algebras (pca’s). We disprove a suggestion made by Kreisel about using Friedberg numberings to construct extensional pca’s. We then discuss separability and elements without total extensions. We relate this to Ershov’s notion of precompleteness, and we show that precomplete numberings are not 1–1 in general.

In [12], John Stillwell wrote, ‘finding the exact strength of the Brouwer invariance theorems seems to me one of the most interesting open problems in reverse mathematics.’ In this article, we solve Stillwell’s problem by showing that (some forms of) the Brouwer invariance theorems are equivalent to the weak König’s lemma over the base system ${\sf RCA}_0$ . In particular, there exists an explicit algorithm which, whenever the weak König’s lemma is false, constructs a topological embedding of $\mathbb {R}^4$ into $\mathbb {R}^3$ .

Inquisitive modal logic, InqML, is a generalisation of standard Kripke-style modal logic. In its epistemic incarnation, it extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. Technically, InqML fits within the family of logics based on team semantics. From a model-theoretic perspective, it takes us a step in the direction of monadic second-order logic, as inquisitive modal operators involve quantification over sets of worlds. We introduce and investigate the natural notion of bisimulation equivalence in the setting of InqML. We compare the expressiveness of InqML and first-order logic in the context of relational structures with two sorts, one for worlds and one for information states, and characterise inquisitive modal logic as the bisimulation invariant fragment of first-order logic over various natural classes of two-sorted structures.

We prove that the Weihrauch lattice can be transformed into a Brouwer algebra by the consecutive application of two closure operators in the appropriate order: first completion and then parallelization. The closure operator of completion is a new closure operator that we introduce. It transforms any problem into a total problem on the completion of the respective types, where we allow any value outside of the original domain of the problem. This closure operator is of interest by itself, as it generates a total version of Weihrauch reducibility that is defined like the usual version of Weihrauch reducibility, but in terms of total realizers. From a logical perspective completion can be seen as a way to make problems independent of their premises. Alongside with the completion operator and total Weihrauch reducibility we need to study precomplete representations that are required to describe these concepts. In order to show that the parallelized total Weihrauch lattice forms a Brouwer algebra, we introduce a new multiplicative version of an implication. While the parallelized total Weihrauch lattice forms a Brouwer algebra with this implication, the total Weihrauch lattice fails to be a model of intuitionistic linear logic in two different ways. In order to pinpoint the algebraic reasons for this failure, we introduce the concept of a Weihrauch algebra that allows us to formulate the failure in precise and neat terms. Finally, we show that the Medvedev Brouwer algebra can be embedded into our Brouwer algebra, which also implies that the theory of our Brouwer algebra is Jankov logic.

Ramsey’s theorem asserts that every k-coloring of $[\omega ]^n$ admits an infinite monochromatic set. Whenever $n \geq 3$ , there exists a computable k-coloring of $[\omega ]^n$ whose solutions compute the halting set. On the other hand, for every computable k-coloring of $[\omega ]^2$ and every noncomputable set C, there is an infinite monochromatic set H such that $C \not \leq _T H$ . The latter property is known as cone avoidance.

In this article, we design a natural class of Ramsey-like theorems encompassing many statements studied in reverse mathematics. We prove that this class admits a maximal statement satisfying cone avoidance and use it as a criterion to re-obtain many existing proofs of cone avoidance. This maximal statement asserts the existence, for every k-coloring of $[\omega ]^n$ , of an infinite subdomain $H \subseteq \omega $ over which the coloring depends only on the sparsity of its elements. This confirms the intuition that Ramsey-like theorems compute Turing degrees only through the sparsity of its solutions.