3
$\begingroup$

I tried looking it up but I lack the English terminology to do so.

I do not understand the difference in $\models$ and $\vdash$ in propositional logic, I thought there was a difference until I saw this theorem: $$\Sigma \models A \iff \Sigma \vdash A$$

But not, unsure.

The $\models$ means that we can for every assignment $M$ that satisfy all the forumlas in $\Sigma$. It means $M$ also satisfy $A$.

The $\vdash$ means that we have a "proof" of $A$ using $\Sigma$, but I really didn't understand what does that mean.

Can someone explain or link a place where I can read and understand the difference?

$\endgroup$
1
  • 1
    $\begingroup$ Basically, syntax is about rules for manipulating symbols, while semantics is concerned with the meaning of the statements. Of course, these different methods for deriving new statements should agree as much as possible $\endgroup$ Aug 15, 2018 at 0:23

1 Answer 1

7
$\begingroup$

$\Sigma\vdash A$ does indeed mean that there is a formal proof of $A$ from the axioms on $\Sigma$.

What a formal proof is, is too big a subject to answer in an MSE answer, but any introductory text in logic ought to present at least one concept of formal proof, where you can see how everything fit together.

The fact that $\vDash$ (defined in terms of models) and $\vdash$ (defined in terms of proofs) are equivalent is not obvious and is a moderately deep result. It is involved enough that the two directions have separate names:

$\Sigma\vdash A \implies \Sigma\vDash A$ is the soundness theorem for the logic you're working with. (In other words, the proof system is "sound" if everything it proves is also actually true in every model).

$\Sigma\vDash A \implies \Sigma\vdash A$ is the completeness theorem for the logic. (A proof system is "complete" if a sentence that is true in every model has a proof).

$\endgroup$
4
  • $\begingroup$ Does the theorem implies that "everything we prove is true" and "everything that is true is provable" ? $\endgroup$
    – Rab
    Aug 14, 2018 at 16:42
  • $\begingroup$ @Rab: Yes, those are terser formulations of the soundness and completeness theorems. (Beware that they can be somewhat misleading unless one is aware that "true" is to be interpreted as "satisfied by every model"). $\endgroup$ Aug 14, 2018 at 16:43
  • $\begingroup$ Is that true for any $\Sigma$ though? because as far as I understand, we can have in $\Sigma$ things like not $\alpha$ and $\alpha$, or do we put a constrain on $\Sigma$ $\endgroup$
    – Rab
    Aug 14, 2018 at 16:45
  • $\begingroup$ @Rab: Yes, that works for any $\Sigma$. If $\Sigma$ contains such a contradiction, then there are no truth assignments that satisfy $\Sigma$, so $\Sigma\vDash A$ holds vacuously no matter what $A$ is. On the other hand, a complete proof system will allow anything to be derived from $\neg\alpha\land\alpha$, so the correspondence still holds. $\endgroup$ Aug 14, 2018 at 16:50

You must log in to answer this question.

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