In propositional logic, why are there two implies?

104 Views Asked by At

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?

1

There are 1 best solutions below

4
On BEST ANSWER

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