Show that "$\Gamma \models S \Rightarrow \Gamma \vdash S$" entails "if $\Gamma \nvdash P \And \sim P$ then $\Gamma$ is satisfiable"

I'm primarily confused with the notation being used here. In particular, I understand that "satisfiable" means there is at least one interpretation that makes $\Gamma$ true, but I'm not sure what $\vdash$ means nor what the statement $\Gamma \models S \Rightarrow \Gamma \vdash S$ means. The first part tells me that $\Gamma$ "makes true" $S$, or that there is no interpretation which makes $\Gamma$ true and $S$ false, but I don't understand how to interpret what comes after this (the "$\Rightarrow \Gamma \vdash S$" part). I'd really appreciate if someone could clear up this notation for me.

  • $\begingroup$ Unless I am mistaken, $\Gamma \models S$ should mean $S$ is satisfied in all models of $\Gamma$ and not just some. Then it is saying if $S$ is true in all models of $\Gamma$ then actually $\Gamma$ proves $S$ (the turnstile is read as "proves"). $\endgroup$ Feb 27, 2014 at 0:57
  • $\begingroup$ This means (usually) there is a finite proof from the sentences of $\Gamma$ where the last line is $S$. $\endgroup$ Feb 27, 2014 at 0:58
  • $\begingroup$ @RyanSullivant how do we make sense of the term "proves?" What does it mean for $\Gamma$ to "prove" $S$? $\endgroup$ Feb 27, 2014 at 1:00
  • $\begingroup$ In general, it means what I just said (of course this depends on your system however). So there is a finite set of sentences $\sigma_1, \ldots, \sigma_n$ where either: $\sigma_i \in \Gamma$ or $\sigma_i$ is a logical axiom or $\sigma_i$ follows from modus ponens from $\sigma_j, \sigma_k$ where $j <k < i$ and $\sigma_n$ is $S$. Perhaps, someone else can explain it better though. $\endgroup$ Feb 27, 2014 at 1:06
  • $\begingroup$ Ah, I see what you mean. It means that $S$ is derivable from $\Gamma$ using a proof that gets us from $\Gamma$ to $S$? So how can we show that $\Gamma$ is satisfiable? If you cannot derive a contradiction from $\Gamma$, how does this show that $\Gamma$ is satisfiable? Also, one more point, what does the $\Rightarrow$ mean in this context? $\endgroup$ Feb 27, 2014 at 1:13

3 Answers 3


The symbol :

$\Gamma \vDash S$

means that the sentence $S$ is a logical consequence of the set of sentences $\Gamma$.

This means, as said in the above comments :

every interpretation that satisfies all sentences $\varphi \in \Gamma$ (i.e. is a model of $\Gamma$), satisfies also $S$.

The symbol :

$\Gamma \vdash S$

means that the sentence $S$ is provable from the set of assumptions $\Gamma$.

This means that the problem implicitly assume that we have in place a proof system, made of (one or more) rules of inference and (zero o more) axioms and a definition of derivation; in this way, the symbol above is defined (as in the comment) as :

there is a finite set of sentences $\sigma_1, … ,\sigma_n$, where either: (i) $\sigma_i \in \Gamma$, or (ii) $\sigma_i$ is a logical axiom or (iii) $\sigma_i$ follows by a rule of inference from some (one or more) $\sigma_k$, where $1 \le k < i$ and $\sigma_n = S$.

Finally, the symbol :

$\Gamma \nvdash P \land \lnot P$

means that form $\Gamma$, with the proof system above, we can derive a contradiction, i.e. $\Gamma$ is inconsistent. So, we say that $\Gamma$ is consistent when it is not inconsistent (i.e.when we cannot derive a contradiction from it).

The statement of the problem boils down to :

show that if $\Gamma$ is consistent, then it is satisfiable.

Now, in order to prove it, procede as suggested by @Ryan Sullivant, i.e. by contradiction, and suppose that $\Gamma$ is not satisfiable. This means that $\Gamma$ has no models.

Now re-read the relation of logical consequence explained above : $\Gamma \vDash \varphi$ iff every model of $\Gamma$ is also a model of $\varphi$.

But we assumed that $\Gamma$ has no models; so the last condition is vacuosly satisfied for every $\varphi$, and also for $P \land \lnot P$.

This means that, if $\Gamma$ is not satisfiable, i.e. if it has no models, than :

$\Gamma \vDash P \land \lnot P$.

At this point, we need the theorem mentioned in the hypotheses of the problem :

if $\Gamma \vDash S$, then $\Gamma \vdash S$

(if $S$ is a logical conseuqnce of $\Gamma$, then $S$ is provable from $\Gamma$; we say that the proof system is complete).

Having proved, form the assumption that $\Gamma$ is unstaisfiable, that $P \land \lnot P$ is a logical consequence of $\Gamma$, we use the above theorem to conclude that $P \land \lnot P$ is provable form $\Gamma$.

In conclusion :

if $\Gamma$ is unsatisfiable, then $\Gamma$ is inconsistent.


So I think this is what we may want to do. Suppose for contradiction that $\Gamma$ is not satisfiable. This means that $\Gamma$ has no models. Now, fix some sentence $P$ and let $S \equiv P \wedge \neg P$. Now, $\Gamma \models S$ will be vacuously true since there are no models of $\Gamma$, (i.e. any model of $\Gamma$ will satisfy $S$). So by the hypothesis, we have that $\Gamma \vdash S$. But this means $\Gamma \vdash P \wedge \neg P$ contradicting the hypothesis that this does not happen.


$\Gamma \models S$ means 'Every model of $\Gamma$ satisfies wff $S$ ' So given statement can be written as follows:

For all wff $S$ on the language of $\Gamma$, if every model of $\Gamma$ satisfies $S$ then $\Gamma$ proves $S$.

Formally, this statement is written as $\forall S[ (\forall \mathcal{M} :\mathcal{M}\models \Gamma \implies \mathcal{M}\models S)\implies \Gamma\vdash S]$. Take contraposition of this statement then we get

For all wff $S$ on the language of $\Gamma$, if $\Gamma$ does not prove $S$ then there is a model of $\Gamma$ that does not satisfy $S$.

(Formally it is written as $\forall S [\Gamma \nvdash S \implies (\exists \mathcal{M} :\mathcal{M}\models\Gamma \,\&\, \mathcal{M}\not\models S)]$.)

Note that if $\mathcal{M}\not\models S$ then $\mathcal{M}\models(\lnot S)$. Take $S=P\land \lnot P$ then you get desired proposition.

  • $\begingroup$ Sorry ... $\Gamma \vDash S$ does not means "$S$ is provable form $\Gamma$", but instead : "$S$ is a logical consequence of $\Gamma$". If you do not define a proof system, and until you do not prove a soundness and completeness theorem, the two relations are not equivalent. $\endgroup$ Feb 27, 2014 at 7:36
  • $\begingroup$ @MauroALLEGRANZA I do not say that $\Gamma\models S$ means '$\Gamma$ proves $S$'. I say that "$\Gamma\models S$ means 'every model $\mathcal{M}$ of $\Gamma$ satisfies $S$'." $\endgroup$
    – Hanul Jeon
    Feb 27, 2014 at 7:45
  • $\begingroup$ @tetori I think Mauro is talking about the first line: you write "$\Gamma \models S$" but I think you mean "$\Gamma \models S \implies \Gamma \vdash S$" $\endgroup$ Feb 27, 2014 at 7:49
  • $\begingroup$ @RyanSullivant Ah... I find problem in my answer. Thanks! $\endgroup$
    – Hanul Jeon
    Feb 27, 2014 at 7:51
  • $\begingroup$ @MauroALLEGRANZA I am sorry for you that misunderstood your claim. $\endgroup$
    – Hanul Jeon
    Feb 27, 2014 at 7:54

You must log in to answer this question.

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