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](https://mathoverflow.net/a/51786/8133)).


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](https://arxiv.org/abs/math/0509616)), 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.



Modal logic of "mostly-satisfiability"
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>


