8

For $n\in\omega+1$ let $\mathsf{ZFC}_n$ be $\mathsf{ZC}$ + $\{\Sigma_k$-$\mathsf{Rep}: k<n\}$. Let $\widehat{\mathsf{ZFC}}$ be the strongest consistent theory $\mathsf{ZFC}_n$ (so if $\mathsf{ZFC}$ is consistent then $\widehat{\mathsf{ZFC}}=\mathsf{ZFC}$). Note that this definition is entirely "internal" - for example, for every standard natural number $n$ every model of $\mathsf{ZFC}$ thinks that $\widehat{\mathsf{ZFC}}$ has a model and that $\widehat{\mathsf{ZFC}}$ strictly extends $\mathsf{ZFC}_n$ (see here).

I'm interested in the "downward-looking" modal logic this gives rise to. Ignoring set/class issues for simplicity, let our class of worlds $\mathbb{W}$ be the class of models of $\mathsf{ZFC}$, with the accessibility relation $\mathcal{M}\rightarrow\mathcal{N}$ holding whenever $\mathcal{N}$ is a structure in $\mathcal{M}$ such that $\mathcal{M}\models(\mathcal{N}\models\widehat{\mathsf{ZFC}})$. Intuitively $\Diamond \varphi$ expresses that $\varphi$ is "as consistent as possible" with $\mathsf{ZFC}$.

Finally, and as with for example the modal logic of forcing (see Hamkins), we'll restrict attention to "first-order expressible" valuations $\nu$; these are valuations such that for each propositional atom $p$ there is some sentence in first-order set theory $\varphi$ with $\nu(p)=\{\mathcal{M}\in\mathbb{W}: \mathcal{M}\models\varphi\}.$ Basically, we're not just treating $(\mathbb{W},\rightarrow)$ as a pure Kripke frame, we're also restricting attention to "model-theoretically meaningful" ways of assigning truth values to sentences at worlds.

Question 1: What is the corresponding modal logic? That is, what propositional modal sentences are made true at every world with respect to every valuation satisfying the above expressibility criterion?

Since this is rather broad, let me localize things a bit. Note that we can make sense of the definition of the modal logic above - call it "$\mathfrak{D}$" - within the language of set theory itself, so we can ask what a given model of $\mathsf{ZFC}$ thinks about $\mathfrak{D}$. Semantically, this amounts to restricting attention to worlds within a given model of $\mathsf{ZFC}$.

Question 2: Is there a (standard) propositional modal sentence $\varphi$ such that it is independent of $\mathsf{ZFC}$ whether $\varphi\in\mathfrak{D}$?

A positive answer to question 2 would suggest that question 1 does not have a simple answer.

My primary interest is actually in more complicated languages based on the above picture - in particular, when $\mathcal{M}\rightarrow\mathcal{N}$, the starting structure $\mathcal{M}$ thinks that some of the elements of $\mathcal{N}$ are standard and so we get a partial counterpart relation and can start playing with object quantifiers - but the "pure sentential" side of things seems like a good starting point already.

Noah Schweber
  • 18,932
  • If I understood your setup correctly, then $M\Vdash \varphi$ under the first-order valuation $\iota$ iff $M\models \varphi^{\star}\iota$, where $\cdot^{\star}\iota$ replaces $\Box$ with $\mathsf{Prv}_{\hat{\mathsf{ZFC}}}$ and propositional variables with their $\iota$-evaluation. That is your logic is simply the provability logic of $\hat{\mathsf{ZFC}}$. This connection could be established in the fashion of Paula Henk paper "Kripke Models Built from Models of Arithmetic" https://eprints.illc.uva.nl/id/eprint/489/1/PP-2014-01.text.pdf (she done this for $\mathsf{PA}$-provability). – Fedor Pakhomov Feb 08 '23 at 15:49
  • @FedorPakhomov Does this take into account how $\widehat{\mathsf{ZFC}}$ changes from model to model? E.g. every model thinks that $\widehat{\mathsf{ZFC}}$ is consistent, but that's not a feature of "fixed" theories like $\mathsf{ZFC}$. – Noah Schweber Feb 08 '23 at 15:51
  • Next the provability logic of $\hat{\mathsf{ZFC}}$ is basically a variantion of provability logic of Feferman provability in the style of the paper "A Smart Child of Peano" by Vladimir Shavrukov https://projecteuclid.org/journalArticle/Download?urlId=10.1305%2Fndjfl%2F1094061859. Strictly speaking, Shavrukov studied it in the case of $\mathsf{PA}$ (one of the predicate to which his result is applicable is provability for $\hat{\mathsf{PA}}=\mathsf{I}\Sigma_1+{\mathsf{I}\Sigma_n\mid \mathsf{I}\Sigma_n \text{is consistent}}$) but pretty much sure this should be also applicable in your case. – Fedor Pakhomov Feb 08 '23 at 15:55
  • If I understood you correctly, then yes. Since your accessibility relation is $\mathcal{M}$ sees $\mathcal{N}$ if $\mathcal{M}$ thinks that $\mathcal{N}$ is a model of $\hat{\mathsf{ZFC}}$. Hence by formalized completeness theorem inside $\mathcal{M}$ we immediately get that my characterization of modal validity is correct for formulas of the modal depth $1$. And more general case is then covered by induction. – Fedor Pakhomov Feb 08 '23 at 15:59
  • There is a slight gap between what Shavrukov proves and what you ask. Namely, he axiomatizes bi-modal provability logic of ordinary and Feferman provability for $\mathsf{PA}$. While you are simply interested in the logic of the first modality. Likely, one could obtain the axiomatization of the first modality by simply dropping all axioms involving the second one. But, of course, this have to be verified. – Fedor Pakhomov Feb 08 '23 at 16:12
  • @FedorPakhomov It's the induction step (re: your comment two prior) that I'm not seeing right now. If $\mathcal{M}\rightarrow\mathcal{N}\rightarrow\mathcal{O}$ we don't generally have $\mathcal{M}\rightarrow\mathcal{O}$, since $\widehat{\mathsf{ZFC}}$ may have shrunk going from $\mathcal{M}$ to $\mathcal{N}$. Is this not an issue (I may well be being over-cautious here and missing something basic)? – Noah Schweber Feb 08 '23 at 16:56
  • @FedorPakhomov That said, (the $\triangle$-part of) the logic in Shavrukov's paper is definitely the $\mathsf{PA}$-version of this question. – Noah Schweber Feb 08 '23 at 16:58
  • I don't see a problem here: the relation indeed is not transitive, but $\hat{\mathsf{ZFC}}$ is not a $\Sigma_1$-definition of a set of axioms and hence the corresponding provability predicate don't have to be transitive either (by transitivity I mean axiom K4 or equivalently 3-rd Loeb's condition). – Fedor Pakhomov Feb 08 '23 at 17:05
  • @FedorPakhomov OK, I think I'm just overthinking things here. If you turn your comments into an answer, I'll accept it once I've had time to think about it (probably ~ next couple days, I'm a bit busy right now). Thanks a ton as always! – Noah Schweber Feb 08 '23 at 17:07
  • You say that you allow $N$ is a class in $M$, but then I don't know what $M\models N\models T$ means for a theory $T$ such as yours. We don't have the satisfaction relation for classes, only for sets. – Joel David Hamkins Feb 11 '23 at 14:03
  • @JoelDavidHamkins I definitely don't allow $\mathcal{N}$ to be a class in $\mathcal{M}$ - by "$\mathcal{N}$ is a structure in $\mathcal{M}$" I mean "$\mathcal{N}\in\mathcal{M}$." Where does it seem that I do allow this? – Noah Schweber Feb 11 '23 at 18:19
  • Ah, I misunderstood your phrase "ignoring set/class issues" to mean that you would allow it as a class. – Joel David Hamkins Feb 11 '23 at 18:22

1 Answers1

3

First point is that this logic is simply the provability logic of formalized $\widehat{\mathsf{ZFC}}$-provability, i.e. the provability logic of the provability predicate: $$\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}(x)\colon\;\;\;\;\; \exists y(\mathsf{Con}(\mathsf{ZFC}_y)\land \mathsf{Prv}_{\mathsf{ZFC}_y}(x)).$$ This, of course. simply is a variant of Feferman's provability (see [1]) for the case of $\mathsf{ZFC}$. The fact that this provability logic coincides with the one based on the frame of models from the question, could be shown in the fashion of the paper [2] of Paula Henk, whom considered the case of $\mathsf{PA}$ with usual provability and the frame built from $\mathsf{PA}$ models. Basically we simply show by induction on the modal depth of modal formulas $\varphi(\vec{x})$ that for any first-order valuation $[\vec{\psi}/\vec{x}]$ and model $\mathcal{M}\models \mathsf{ZFC}$ we have $$\mathcal{M}\Vdash \varphi(\vec{x})[\vec{\psi}/\vec{x}]\iff \mathcal{M}\models (\varphi(\vec{x})[\vec{\psi}/\vec{x}])^{\star},$$ where $\cdot^\star$ is the provability interpretation mapping $\Box$ to $\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}$.

Hence the question is basically what is the provability logic of this version of Feferman provability. The provability logic of Feferman provability for $\mathsf{PA}$ was studied by Vladimir Shavrukov [3]. Namely his main focus was on the provability predicate $$\exists y (\mathsf{Con}(\mathsf{I}\Sigma_{y})\land \mathsf{Prv}_{\mathsf{I}\Sigma_y}(x))$$ Although, I haven't carefully checked this, I am almost sure, that the result would transfer to $\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}$ without any troubles. For the step of induction we simply use that each $\mathcal{M}\models \mathsf{ZFC}$ satisfies completeness theorem.

So assuming that Shavrukov's result indeed transfers, then the joint provability logic of $\mathsf{Prv}_{\mathsf{ZFC}}$ ($\Box$) and $\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}$ ($\triangle$) is

  1. $\mathsf{GL}$ for $\Box$
  2. $\mathsf{K}$ for $\triangle$
  3. $\Box\varphi\to \Box\triangle \varphi$
  4. $\Box\varphi\to \triangle\Box\varphi$
  5. $\Box\varphi\mathrel{\leftrightarrow} (\triangle \varphi\lor \Box\bot)$
  6. $\triangledown \top$
  7. $\triangle \varphi \to \triangle((\triangle \psi\to\psi)\lor\triangle \varphi)$

The answer to the original Question 1 is the $\triangle$-fragment of this logic.

[1] S. Feferman. Arithmetization of metamathematics in a general setting. Fundamenta mathematicae, vol. 49 no. 1 (1960), pp. 35–92.

[2] Henk, Paula. "Kripke models built from models of arithmetic." Logic, Language, and Computation: 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015. https://eprints.illc.uva.nl/id/eprint/489/1/PP-2014-01.text.pdf

[3] Shavrukov, V. Yu. "A smart child of Peano's." Notre Dame Journal of Formal Logic 35.2 (1994): 161-185. https://projecteuclid.org/journalArticle/Download?urlId=10.1305%2Fndjfl%2F1094061859

Fedor Pakhomov
  • 5,461