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)?

  • 2
    $\begingroup$ I don't think "validity logic" is well studied. This sort of reminds me of Hamkin's modal logic of forcing, which is apparently S4.2: arxiv.org/pdf/math/0509616v1.pdf $\endgroup$
    – Matt W-D
    Mar 9, 2013 at 23:44
  • 3
    $\begingroup$ Aren't those two the same? Since FOL is sound & complete, what is valid is exactly what is provable. $\endgroup$
    – Luka Mikec
    Oct 10, 2013 at 13:47
  • 2
    $\begingroup$ @LukaMikec It's more complicated than that for weak theories - see my answer. $\endgroup$ Jan 6, 2020 at 19:57
  • 1
    $\begingroup$ @NoahSchweber agreed, of course. I may have been thinking of informal provability since S4 and S5 were mentioned in the opening post, and GL is incomparable to those. But either way I don't know the precise intended interpretation of $\Box$ for "provable" and "valid" in this post, and my comment could only have potential to make sense if this was very clear. (Fun fact: 7 years later I work in this area :D) $\endgroup$
    – Luka Mikec
    Jan 7, 2020 at 20:33
  • 1
    $\begingroup$ @LukaMikec Yea, looking back at this 7 years later (definitely didn't expect an answer!) I was just very sloppy. What Burgess is talking about is "demonstrability", as he calls it, where being demonstrable is a matter of being recognizable as true by logical considerations alone (or existence of a verifying derivation). Consequently there's no worry of offending against incompleteness and so both $\Box p \rightarrow p$ and $\Box (\Box p \rightarrow p)$ can be admitted as theorems, as in S4/S5 but not in GL/GLS. $\endgroup$
    – Dennis
    Jan 7, 2020 at 21:36

1 Answer 1


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!


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$.


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).

  • $\begingroup$ This is very interesting. Two things: (1) can you spell out in more detail your comment on the need for Skolem functions? (2) I suppose there is a connection with theories which introduce a truth predicate? Perhaps similar to a connection between a predicate and an operator reading of the modalities? $\endgroup$
    – Nagase
    Jan 6, 2020 at 23:43
  • $\begingroup$ @Nagase Not sure about (2). Re: (1), Skolem functions aren't the only way to do it, but the point is that you need to talk about functions or relations on $\mathcal{M}$ in order to talk about satisfaction in general. We could go via Skolem functions, or winning strategies in the corresponding "Tarski truth games," or appropriate subtrees of the corresponding "big" syntax trees ("big" here referring to the fact that we want to unfold quantifiers as conjunctions/disjunctions ranging over the whole model), or etc. $\endgroup$ Feb 6, 2020 at 19:48
  • 1
    $\begingroup$ The best we can do by quantifying over individuals is get "local" truth predicates - e.g. a formula defining truth for $\Sigma_{17}$ formulas, but not applicable to $\Sigma_{18}$ formulas. (And Tarski's undefinability theorem says that this is unavoidable.) $\endgroup$ Feb 6, 2020 at 19:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .