In 2007 (with more work done later), J. Hamkins and B. Löwe found that the ZFC provably valid principles of forcing are the assertions of S4.2. In the introduction, they mention field extension as a sort of algebraic analog of forcing. This got me thinking (perhaps naively)...Is there a similar connection to the theory of fields?

Say we read $\Box \varphi$ as "$\varphi$ holds in every field extension," and we define the provably valid principles of field extensions to be the modal sentences $\psi(p_1, \cdots, p_n)$ such that, for any substitution $\psi(\varphi_1, \cdots, \varphi_n)$ of the letters $p_j$ for first-order formulas in the language of fields, $\psi(\varphi_1, \cdots, \varphi_n)$ holds in every field. What can we say about the provably valid principles of field extensions? Similar question: What if we only care about the valid principles of finite field extensions of $\mathbb Q$ (number fields)? What about in other classes of fields?

In either case, the property "is a field extension of" is transitive and reflexive, so the modal rules $\Box p \to p$ and $\Box p \to \Box\Box p$ both hold. Necessitation holds rather trivially, and rule $K$ holds because if $\varphi_1 \to \varphi_2$ holds in every field and $\varphi$ hold in every field, so should $\varphi_2$. Also, as pointed out in the comments, $\Diamond \Box p \to \Box \Diamond p$ is a valid principle of field extensions as well, since fields have the amalgamation property. (Of course, one could replace "field" with "number field" in this paragraph.)

Here are the links to the papers:

Here is a related discussion

dohave amalgamation in the sense that for any embeddings $f_0\colon k\to K_0$ and $f_1\colon k\to K_1$, there is a field $L$ and embeddings $g_0\colon K_0\to L$ and $g_1\colon K_1\to L$ such that $g_0\circ f_0=g_1\circ f_1$. (Proof: take a sufficiently large algebraically closed field for $L$.) In terms of extensions, this means that if $K_0,K_1\supseteq k$, there are $L_0\supseteq K_0$ and $L_1\supseteq K_1$ such that $L_0\simeq_kL_1$. Since $L_0$ and $L_1$ are then elementarily equivalent, this is enough to make S4.2 valid under your interpretation. $\endgroup$ – Emil Jeřábek Nov 1 '18 at 16:35