State spaces are, in the most general sense, sets of entities that contain information. Examples include states of dynamical systems, processes of observations, or possible worlds. We use domain theory to describe the structure of positive and negative information in state spaces. We present examples ranging from the space of trajectories of a dynamical system, over Dunn’s aboutness interpretation of fde, to the space of open sets of a spectral space. We show that these information structures induce so-called hype models which were recently developed by Leitgeb (2019). Conversely, we prove a representation theorem: roughly, hype models can be represented as induced by an information structure. Thus, the well-behaved logic hype is a sound and complete logic for reasoning about information in state spaces.

As application of this framework, we investigate information fusion. We motivate two kinds of fusion. We define a groundedness and a separation property that allow a hype model to be closed under the two kinds of fusion. This involves a Dedekind–MacNeille completion and a fiber-space like construction. The proof-techniques come from pointless topology and universal algebra.

This paper explores relational syllogistic logics, a family of logical systems related to reasoning about relations in extensions of the classical syllogistic. These are all decidable logical systems. We prove completeness theorems and complexity results for a natural subfamily of relational syllogistic logics, parametrized by constructors for terms and for sentences.

Quantum set theory (QST) and topos quantum theory (TQT) are two long running projects in the mathematical foundations of quantum mechanics (QM) that share a great deal of conceptual and technical affinity. Most pertinently, both approaches attempt to resolve some of the conceptual difficulties surrounding QM by reformulating parts of the theory inside of nonclassical mathematical universes, albeit with very different internal logics. We call such mathematical universes, together with those mathematical and logical structures within them that are pertinent to the physical interpretation, ‘Q-worlds’. Here, we provide a unifying framework that allows us to (i) better understand the relationship between different Q-worlds, and (ii) define a general method for transferring concepts and results between TQT and QST, thereby significantly increasing the expressive power of both approaches. Along the way, we develop a novel connection to paraconsistent logic and introduce a new class of structures that have significant implications for recent work on paraconsistent set theory.

This paper contributes to a recent research program that extends arguments supporting elementary conditionalization to arguments supporting conditionalization with general, measure-theoretic conditional probabilities. I begin by suggesting an amendment to the framework that Rescorla (2018) has used to characterize regular conditional probabilities in terms of avoiding Dutch book. If we wish to model learning scenarios in which an agent gains complete membership knowledge about some subcollection of the events of interest to her, then we should focus on updating policies that are what I shall call proper. I go on to characterize regular conditional probabilities in proper learning scenarios using what van Fraassen (1999) calls The General Reflection Principle.

A globally expressivist analysis of the indicative conditional based on the Ramsey Test is presented. The analysis is a form of ‘global’ expressivism in that it supplies acceptance and rejection conditions for all the sentence forming connectives of propositional logic (negation, disjunction, etc.) and so allows the conditional to embed in arbitrarily complex sentences (thus avoiding the Frege–Geach problem). The expressivist framework is semantically characterized in a restrictor semantics due to Vann McGee, and is completely axiomatized in a logic dubbed ICL (‘Indicative Conditional Logic’). The expressivist framework extends the AGM (after Alchourron, Gärdenfors, Makinson) framework for belief revision and so provides a categorical (‘yes’–‘no’) epistemology for conditionals that complements McGee’s probabilistic framework while drawing on the same semantics. The result is an account of the semantics and acceptability conditions of the indicative conditional that fits well with the linguistic data (as pooled by linguists and from psychological experiments) while integrating both expressivist and semanticist perspectives.

We consider the Lambek calculus, or noncommutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an $\omega $ -rule, and prove that the derivability problem in this calculus is $\Pi _1^0$ -hard. This solves a problem left open by Buszkowski (2007), who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a Lambek grammar with unique type assignment, without Lambek’s nonemptiness restriction imposed (cf. Safiullin, 2007).

The 3-valued paraconsistent logic Ciore was developed by Carnielli, Marcos and de Amo under the name LFI2, in the study of inconsistent databases from the point of view of logics of formal inconsistency (LFIs). They also considered a first-order version of Ciore called LFI2*. The logic Ciore enjoys extreme features concerning propagation and retropropagation of the consistency operator: a formula is consistent if and only if some of its subformulas is consistent. In addition, Ciore is algebraizable in the sense of Blok and Pigozzi. On the other hand, the logic LFI2* satisfies a somewhat counter-intuitive property: the universal and the existential quantifier are inter-definable by means of the paraconsistent negation, as it happens in classical first-order logic with respect to the classical negation. This feature seems to be unnatural, given that both quantifiers have the classical meaning in LFI2*, and that this logic does not satisfy the De Morgan laws with respect to its paraconsistent negation. The first goal of the present article is to introduce a first-order version of Ciore (which we call QCiore) preserving the spirit of Ciore, that is, without introducing unexpected relationships between the quantifiers. The second goal of the article is to adapt to QCiore the partial structures semantics for the first-order paraconsistent logic LPT1 introduced by Coniglio and Silvestrini, which generalizes the semantic notion of quasi-truth considered by Mikeberg, da Costa and Chuaqui. Finally, some important results of classical Model Theory are obtained for this logic, such as Robinson’s joint consistency theorem, amalgamation and interpolation. Although we focus on QCiore, this framework can be adapted to other 3-valued first-order LFIs.

We propose a dynamic hyperintensional logic of belief revision for non-omniscient agents, reducing the logical omniscience phenomena affecting standard doxastic/epistemic logic as well as AGM belief revision theory. Our agents don’t know all a priori truths; their belief states are not closed under classical logical consequence; and their belief update policies are such that logically or necessarily equivalent contents can lead to different revisions. We model both plain and conditional belief, then focus on dynamic belief revision. The key idea we exploit to achieve non-omniscience focuses on topic- or subject matter-sensitivity: a feature of belief states which is gaining growing attention in the recent literature.

We show that Dependent Choice is a sufficient choice principle for developing the basic theory of proper forcing, and for deriving generic absoluteness for the Chang model in the presence of large cardinals, even with respect to $\mathsf {DC}$ -preserving symmetric submodels of forcing extensions. Hence, $\mathsf {ZF}+\mathsf {DC}$ not only provides the right framework for developing classical analysis, but is also the right base theory over which to safeguard truth in analysis from the independence phenomenon in the presence of large cardinals. We also investigate some basic consequences of the Proper Forcing Axiom in $\mathsf {ZF}$ , and formulate a natural question about the generic absoluteness of the Proper Forcing Axiom in $\mathsf {ZF}+\mathsf {DC}$ and $\mathsf {ZFC}$ . Our results confirm $\mathsf {ZF} + \mathsf {DC}$ as a natural foundation for a significant portion of “classical mathematics” and provide support to the idea of this theory being also a natural foundation for a large part of set theory.

In his Tractatus, Wittgenstein maintained that arithmetic consists of equations arrived at by the practice of calculating outcomes of operations $\Omega ^{n}(\bar {\xi })$ defined with the help of numeral exponents. Since $Num$ (x) and quantification over numbers seem ill-formed, Ramsey wrote that the approach is faced with “insuperable difficulties.” This paper takes Wittgenstein to have assumed that his audience would have an understanding of the implicit general rules governing his operations. By employing the Tractarian logicist interpretation that the N-operator $N(\bar {\xi })$ and recursively defined arithmetic operators $\Omega ^{n}(\bar {\xi })$ are not different in kind, we can address Ramsey’s problem. Moreover, we can take important steps toward better understanding how Wittgenstein might have imagined emulating proof by mathematical induction.

Numerous learning tasks can be described as the process of extrapolating patterns from observed data. One of the driving intuitions behind the theory of algorithmic randomness is that randomness amounts to the absence of any effectively detectable patterns: it is thus natural to regard randomness as antithetical to inductive learning. Osherson and Weinstein [11] draw upon the identification of randomness with unlearnability to introduce a learning-theoretic framework (in the spirit of formal learning theory) for modelling algorithmic randomness. They define two success criteria—specifying under what conditions a pattern may be said to have been detected by a computable learning function—and prove that the collections of data sequences on which these criteria cannot be satisfied correspond to the set of weak 1-randoms and the set of weak 2-randoms, respectively. This learning-theoretic approach affords an intuitive perspective on algorithmic randomness, and it invites the question of whether restricting attention to learning-theoretic success criteria comes at an expressivity cost. In other words, is the framework expressive enough to capture most core algorithmic randomness notions and, in particular, Martin-Löf randomness—arguably, the most prominent algorithmic randomness notion in the literature? In this article, we answer the latter question in the affirmative by providing a learning-theoretic characterisation of Martin-Löf randomness. We then show that Schnorr randomness, another central algorithmic randomness notion, also admits a learning-theoretic characterisation in this setting.

Gödel’s ontological proof is by now well known based on the 1970 version, written in Gödel’s own hand, and Scott’s version of the proof. In this article new manuscript sources found in Gödel’s Nachlass are presented. Three versions of Gödel’s ontological proof have been transcribed, and completed from context as true to Gödel’s notes as possible. The discussion in this article is based on these new sources and reveals Gödel’s early intentions of a liberal comprehension principle for the higher order modal logic, an explicit use of second-order Barcan schemas, as well as seemingly defining a rigidity condition for the system. None of these aspects occurs explicitly in the later 1970 version, and therefore they have long been in focus of the debate on Gödel’s ontological proof.

Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas.

To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at http://www.phil.cmu.edu/legacy/Proof_Site/.

We must—that is my conviction—take the concept of the specifically mathematical proof as an object of investigation.

Hilbert 1918

In practice, mathematical proofs are most often the result of careful planning by the agents who produced them. As a consequence, each mathematical proof inherits a plan in virtue of the way it is produced, a plan which underlies its “architecture” or “unity.” This paper provides an account of plans and planning in the context of mathematical proofs. The approach adopted here consists in looking for these notions not in mathematical proofs themselves, but in the agents who produced them. The starting point is to recognize that to each mathematical proof corresponds a proof activity which consists of a sequence of deductive inferences—i.e., a sequence of epistemic actions—and that any written mathematical proof is only a report of its corresponding proof activity. The main idea to be developed is that the plan of a mathematical proof is to be conceived and analyzed as the plan of the agent(s) who carried out the corresponding proof activity. The core of the paper is thus devoted to the development of an account of plans and planning in the context of proof activities. The account is based on the theory of planning agency developed by Michael Bratman in the philosophy of action. It is fleshed out by providing an analysis of the notions of intention—the elementary components of plans—and practical reasoning—the process by which plans are constructed—in the context of proof activities. These two notions are then used to offer a precise characterization of the desired notion of plan for proof activities. A fruitful connection can then be established between the resulting framework and the recent theme of modularity in mathematics introduced by Jeremy Avigad. This connection is exploited to yield the concept of modular presentations of mathematical proofs which has direct implications for how to write and present mathematical proofs so as to deliver various epistemic benefits. The account is finally compared to the technique of proof planning developed by Alan Bundy and colleagues in the field of automated theorem proving. The paper concludes with some remarks on how the framework can be used to provide an analysis of understanding and explanation in the context of mathematical proofs.