The Logic of Satisfiability? I am aware of some study into the logic of provability. It is generally taken to be intermediate in strength between S4 and S5 modal logics. Is there corresponding study into something like the logic of satisfiability or (semantic) validity?
The only mention of the topic I have been able to find is in this article by John Burgess, where he calls it "validity logic" (and says it is an S5 modal logic) and doesn't seem to cite any other work on the topic.
Is this subject more widely studied (perhaps under a different name)?
 A: This is a great, and surprisingly subtle, question! Unfortunately the answer is necessarily a bit technical, so let me state the very short version here:

While validity and provability perfectly coincide "in reality," this is nontrivial, and there are non-pathological theories for whom validity logic and provability logic do not coinicide.

And now down the rabbit hole ...
I've written this slightly hastily - apologies in advance for errors!

Preliminaries
In order to talk about validity, we need to either do some serious work or look at richer languages than first-order arithmetic. I'm lazy so I'll do the latter: all theories here are theories in the language of second-order arithmetic, such as $RCA_0$, $WKL_0$, $ACA_0$, etc. Note that despite the name, these are all first-order theories; moreover, they're not all crazily strong, and in particular $ACA_0$ is conservative over $PA$ and both $WKL_0$ and $RCA_0$ is conservative over $I\Sigma_1$.
For $T$ an appropriate theory, I'll write "$PL_T$" and "$VL_T$" for the provability and validity logics associated to $T$ respectively. To avoid pathologies I'll only consider theories which are

*

*at least as strong as $RCA_0$, and


*finitely axiomatizable. (Each of the Big Five is finitely axiomatizable. The key point is the existence of a "universal" formula at each complexity level - namely, $\Sigma^0_1$ for $RCA_0$ through $ATR_0$ and $\Pi^1_1$ for $\Pi^1_1$-$CA_0$. This is something I forget with some regularity, so I'm noting it explicitly here on the grounds that others probably do too.)
Of course that means that the $PL_T$-notation is silly in this context, since it's always just $GL$, but I think its use makes the contrast I'm drawing simpler.

Logical strength (and bivalence in particular)
As Luka Mikec comments, validity and provability coincide. But this does not mean that validity logic and provability logic coincide, even for "reasonable" theories!
The issue is that seemingly-basic properties of structures hide surprising logical strength. The main issue is the definition of "$\mathcal{A}\models\varphi$." In order to capture $\models$ by a single formula, we need to talk about families of Skolem functions - which results in a $\Sigma^1_1$ formula. This should automatically be worrying, and indeed the worry is justified in this case: over $RCA_0$ the scheme (as $\varphi$ ranges over all sentences) "For all $\mathcal{A}$, either $\mathcal{A}\models\varphi$ or $\mathcal{A}\models\neg\varphi$" is equivalent to $ACA_0$, while the single sentence "For all $\mathcal{A}$ and $\varphi$, either $\mathcal{A}\models\varphi$ or $\mathcal{A}\models\neg\varphi$" is equivalent to $ACA_0^+$. Moreover, $ACA_0^+$ is also equivalent to the sentence "For all $\mathcal{A}$, the set $\{\varphi: \mathcal{A}\models\varphi\}$ exists."
So bivalence and theory existence - something we usually take for granted - is actually quite strong. Interestingly, over $RCA_0$ the Soundness and Completeness theorems are much weaker despite being more interesting, being provable in $RCA_0$ and equivalent to $WKL_0$ respectively. However, given the complexity of satisfaction in the first place, we have to be very careful when applying them.
To summarize, over $RCA_0$ we have:

Scheme bivalence is equivalent to $ACA_0$, while all-at-once bivalence is equivalent to $ACA_0^+$ (which is also equivalent to theory existence). Meanwhile, Soundness is outright provable and Completeness is equivalent to $WKL_0$, although in the absence of bivalence they don't necessarily behave as one might expect.


VL is (sometimes) different from PL
This discussion should make it plausible that for theories around the level of $RCA_0$, validity logic and provability logic need not coincide. This is indeed true:

Let $\chi$ be the sentence $$\Box(\Diamond p\rightarrow (\Diamond q\vee\Diamond \neg q)).$$ Then $\chi\in PL_{RCA_0}$ but $\chi\not\in VL_{RCA_0}$.

To see that $\chi\in PL_{RCA_0}$, note that its "provability interpretation" amounts to "$RCA_0$ proves that if $p$ is consistent with $RCA_0$ then either $q$ or $\neg q$ is consistent with $RCA_0$." This is trivial: $RCA_0$ proves that if both $q$ and $\neg q$ are inconsistent with $RCA_0$, then $RCA_0$ itself is inconsistent and so nothing is inconsistent with $RCA_0$.
However, it's not too hard to show that there is a model $M$ of $RCA_0$ and a sentence $\eta$ such that $(i)$ $M$ thinks $RCA_0$ has a model which satisfies some sentence (e.g. "$\forall x(x=x)$") but $(ii)$ $M$ does not think that there is a model $N$ of $RCA_0$ such that $N\models\eta$ or $N\models\neg\eta$. Since this is the most interesting feature of this answer, I've highlighted it:

The key point is that (for $M\models RCA_0$) if $A$ is a structure in $M$ and $M\models (A\models \varphi)$, then in fact $A\models\varphi$. With this in mind, we see that if $A$ is a structure in $M$ and for each sentence $\eta$ we have $M\models (A\models \eta\vee A\models\neg\eta)$ then we have $Th(A)\le_T M^{(3)}$ (here conflating $M$ with its atomic diagram).
Now let $M$ be the $\omega$-model of $RCA_0$ consisting of all sets $\le_T{\bf 0^{(3)}}$ (this is overkill, but meh). Then there is an $\omega$-model $N$ of $RCA_0$ with $N\in M$ (for example, take $N$ to consist of the computable sets). So if $M$ thought "every model of $RCA_0$ is bivalent," then we would have by the point above that $Th(N)\le_T{\bf 0^{(3+3)}}$. But $Th(N)$ has Turing degree ${\bf 0^{(\omega)}}$, and $\omega>6$ (exercise).
Note that in fact all of this is taking place in the realm of $\omega$-models only; there really are no "coding shenanigans" here, this is an entirely computability-theoretic phenomenon.

Building off of this, we can show that $\chi\in VL_T$ iff $T\supseteq ACA_0$ (if we restrict ahead of time to $T\supseteq RCA_0$, as mentioned above). On the other hand, it's not hard to show that this discrepancy goes away eventually:

$VL_{ACA_0}=PL_{ACA_0}$ (and this holds as well for all stronger theories).

So this is an exact dividing line.

Two variations
There are of course various twists we can put on the discussion above. Here are two that I think are particularly interesting:

*

*The idea of validity logic can be expressed in second-order arithmetic. This means that for $M\models RCA_0$ and $T$ appropriate we have "$M$'s version of $VL_T$." This is particularly interesting in case $M$ is a non-$\omega$-model of $T$: this is due to the $ACA_0$ vs. $ACA_0^+$ issue above, one consequence of which is that there is a model $M$ of $ACA_0$ + "$PL_{ACA_0}=GL$" (the latter being added to avoid triviality) such that the standard part of $M$'s version of $VL_{ACA_0}$ does not contain the sentence $\chi$!


*There is also a "concrete" analogue of validity logic which better coincides with provability logic. The idea is to replace the uniform definition of $\models$ with a family of formulas, one for each level of the arithmetic hierarchy: for each $n$ there is a natural way to express "$\mathcal{A}\models\varphi$" for $\mathcal{A}$ a structure and $\varphi$ a $\Sigma_n$ sentence in the language of $\mathcal{A}$. Call this "$\models_n$." Now for each $n$, $RCA_0$ proves bivalence for $\models_n$. We can then define the "schematized" analogue of validity logic, $VL^{scheme}_T$. Then trivially for all $T\supseteq WKL_0$ we get $VL^{scheme}_T=PL_T$. However, this uses the provability of Completeness in $WKL_0$.

Coda
All of the above leaves a few obvious open questions.

*

*(Exact characterizations) What is $VL_{RCA_0}$? What about $VL_{WKL_0}$ or $VL_{RCA_0+RT^2_2}$ - or indeed any interesting theory in the interval $[RCA_0, ACA_0)$?


*(Robustness) Suppose $S,T\in [RCA_0,ACA_0)$. Under what conditions do we have $VL_S=VL_T$?


*(Nonstandardness) Each of the previous two questions can be made nontrivial for $ACA_0$ by looking at nonstandard models as above. What do we get, or how much flexibility do we have, in this broader context (possibly after imposing further "nontriviality" constraints)?


*(Completeness vs. concreteness) Do we have $VL^{scheme}_{RCA_0}=PL_{RCA_0}$? Or is something more (in particular, $WKL_0$) necessary?
As far as I can tell, each of these questions is nontrivial (read: no clue is had by me).
