The modal logic of arithmetic potentialism and the universal algorithm
University of Notre Dame(圣母大学)
Joel David Hamkins
备注:
41 pages. Version v3 has minor revisions, including additional references. Version v4 has further minor revisions and the addition of Chaitin's incompleteness theorem as an easy application of the universal algorithm. v5 makes final publication revisions, including a slight reorganization to place some of the philosophical discussion up front
I investigate the modal commitments of various conceptions of the philosophy of arithmetic potentialism. Specifically, I shall consider the potentialist conceptions arising from a model-theoretic view of the models of arithmetic as possible arithmetic realms of feasibility, considering them under their natural extension concepts, such as end-extensions, arbitrary extensions, conservative extensions and more, which in effect express distinct potentialist ideas. In these potentialist systems, I show, the propositional modal assertions that are valid with respect to all arithmetic assertions with parameters are exactly the assertions of S4. With respect to sentences, however, the validities of a model lie between S4 and S5, and these bounds are sharp in that there are models realizing both endpoints. For a model of arithmetic to validate S5 is precisely to fulfill the arithmetic maximality principle, which asserts that every possibly necessary statement is already true, and these models are equivalently characterized as those satisfying a maximal $Σ_1$ theory. The main S4 analysis makes fundamental use of the universal algorithm, of which this article provides a simplified, self-contained account. The main philosophical point is that fundamentally different potentialist conceptions -- linear inevitability, convergent potentialism and radical branching possibility -- are revealed by the precise modal validities of the corresponding potentialist systems in which those attitudes are expressed, and so it is important to discover them.
We analyze the precise modal commitments of several natural varieties of set-theoretic potentialism, using tools we develop for a general model-theoretic account of potentialism, building on those of Hamkins, Leibman and Löwe, including the use of buttons, switches, dials and ratchets. Among the potentialist conceptions we consider are: rank potentialism (true in all larger $V_β$); Grothendieck-Zermelo potentialism (true in all larger $V_κ$ for inaccessible cardinals $κ$); transitive-set potentialism (true in all larger transitive sets); forcing potentialism (true in all forcing extensions); c…
We define a potentialist system of ZF-structures, that is, a collection of possible worlds in the language of ZF connected by a binary accessibility relation, achieving a potentialist account of the full background set-theoretic universe $V$. The definition involves Berkeley cardinals, the strongest known large cardinal axioms, inconsistent with the Axiom of Choice. In fact, as background theory we assume just ZF. It turns out that the propositional modal assertions which are valid at every world of our system are exactly those in the modal theory S4.2. Moreover, we characterize the worlds sat…
We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm{B}$, $Δ(\mathrm{B})$, and $Σ(\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 $Σ(\mathrm{B})$-disjunction property, the $Σ(\mathrm{B})$-existence property, and the $\mathrm{B}$-exist…
This paper presents the logic QRC$_1$, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. We prove arithmetical soundness of the logic QRC$_1$ with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This paper takes the …
We introduce the $Σ_1$-definable universal finite sequence and prove that it exhibits the universal extension property amongst the countable models of set theory under end-extension. That is, (i) the sequence is $Σ_1$-definable and provably finite; (ii) the sequence is empty in transitive models; and (iii) if $M$ is a countable model of set theory in which the sequence is $s$ and $t$ is any finite extension of $s$ in this model, then there is an end-extension of $M$ to a model in which the sequence is $t$. Our proof method grows out of a new infinitary-logic-free proof of the Barwise extension…
The Gödel translation provides an embedding of the intuitionistic logic $\mathsf{IPC}$ into the modal logic $\mathsf{Grz}$, which then embeds into the modal logic $\mathsf{GL}$ via the splitting translation. Combined with Solovay's theorem that $\mathsf{GL}$ is the modal logic of the provability predicate of Peano Arithmetic $\mathsf{PA}$, both $\mathsf{IPC}$ and $\mathsf{Grz}$ admit arithmetical interpretations. When attempting to 'lift' these results to the monadic extensions $\mathsf{MIPC}$, $\mathsf{MGrz}$, and $\mathsf{MGL}$ of these logics, the same techniques no longer work. Following a…
A semantics for quantified modal logic is presented that is based on Kleene's notion of realizability. This semantics generalizes Flagg's 1985 construction of a model of a modal version of Church's Thesis and first-order arithmetic. While the bulk of the paper is devoted to developing the details of the semantics, to illustrate the scope of this approach, we show that the construction produces (i) a model of a modal version of Church's Thesis and a variant of a modal set theory due to Goodman and Scedrov, (ii) a model of a modal version of Troelstra's generalized continuity principle together …
We define a certain finite set in set theory $\{x\midφ(x)\}$ and prove that it exhibits a universal extension property: it can be any desired particular finite set in the right set-theoretic universe and it can become successively any desired larger finite set in top-extensions of that universe. Specifically, ZFC proves the set is finite; the definition $φ$ has complexity $Σ_2$, so that any affirmative instance of it $φ(x)$ is verified in any sufficiently large rank-initial segment of the universe $V_θ$; the set is empty in any transitive model and others; and if $φ$ defines the set $y$ in som…
In 1994 Jech gave a model theoretic proof of Gödel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano Arithmetic with the role of models being taken by complete consistent extensions. In this note we take another step in the direction of replacing proof-theoretic by model-theoretic arguments. We show, without passing through the arithmetized completeness theorem, that the existence of a model of PA of complexity $Σ^0_2$ is independent of PA, where a model is ide…
The provability logic of a theory $T$ captures the structural behavior of formalized provability in $T$ as provable in $T$ itself. Like provability, one can formalize the notion of relative interpretability giving rise to interpretability logics. Where provability logics are the same for all moderately sound theories of some minimal strength, interpretability logics do show variations. The logic IL(All) is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this paper we raise the previously known lower bound of IL(All) by…
For the Heyting Arithmetic HA, HA* is defined as the theory $\{A\mid {\sf HA}\vdash A^{\Box}\}$, where $A^{\Box}$ is called the box translation of $A$. We characterize the $Σ_1$-provability logic of HA* as a modal theory ${\sf iH}_σ^*$.
In this paper we introduce a modal theory $H_σ$, which is sound and complete for arithmetical $Σ$_1 substitutions in ${\bf HA}$, in other words, we will show that $H_σ$ is the $Σ$_1-provability logic of ${\bf HA}$. Moreover we will show that $H_σ$ is decidable. As a by-product of these results, we show that ${\bf HA} + \Box\bot$ has de Jongh property.
Japan Advanced Institute of Science and Technology(日本北陆先端科学技术大学院大学)
Bayesian reasoning plays a significant role both in human rationality and in machine learning. In this paper, we introduce transfinite modal logic, which combines modal logic with ordinal arithmetic, in order to formalize Bayesian reasoning semi-quantitatively. Technically, we first investigate some nontrivial properties of ordinal arithmetic, which then enable us to expand normal modal logic's semantics naturally and elegantly onto the novel transfinite modal logic, while still keeping the ordinary definition of Kripke models totally intact. Despite all the transfinite mathematical definition…
In 1933, Gödel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's Logic of Proofs LP. In this paper, we study introduced by the author logic GLA, which is a fusion of GL and LP in the union of their languages. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established.
Harvey Friedman shows that, over Peano Arithmetic, the consistency statement for a finitely axiomatised theory $A$ can be characterised as the weakest statement $C$ over Peano Arithmetic such that ${\sf PA}+C$ interprets $A$. We study which base theories $U$ have the property that, for any finitely axiomatised $A$, there is a weakest $C$ such that $U+C$ interprets $A$. We call such theories Friedman-reflexive. We show that a very weak theory, Peano Corto, is Friedman-reflexive. We do not get the usual consistency statements here, but bounded, cut-free or Herbrand consistency statements. We pro…