Semantical and syntactical derivation notation [duplicate]

Question

What do the following two notations mean:

$$A \models$$

$$A \vdash$$

The first one would be saying that A is a contradiction? The second one that A is not a theorem? That doesn't sound right to me.

Answer 1

The notation $ A \models \, $ means that the formula $A$ is not satisfiable, i.e. there is no structure (or assignment in propositional logic) that makes $A$ true. This is a semantical notion.

The notation $A \vdash \, $ means that from the formula $A$ you can derive everything (i.e. any other formula), according to some derivation rules already defined. This is a syntactical notion.

An important theorem in propositional and first-order logic (completeness and soundness) states that the two notions coincide: a formula is unsatisfiable if and only if everything is derivable from it, i.e. $A \models \,$ if and only if $A \vdash\,$.

Because of this equivalence, in the literature you can find some ambiguous terminology. A formula is said contradictory or inconsistent if $A \models \,$ in some textbooks, or if $A \vdash \, $ in other textbooks.

---

The notation used to express that $A$ is not derivable (i.e. it is not a theorem in the considered derivation system) is $\not\vdash A$. This is consistent with the notation $\vdash A$, which says that the formula $A$ is derivable, i.e. that it is a theorem in the considered derivation system. Note that $\not \vdash A$ does not mean $A \vdash\,$: a formula could be non-derivable but still satisfiable.

For the sake of completeness, the notation $\models A$ means that the formula $A$ is valid (a tautology in propositional logic), i.e. every structure makes $A$ true. Again, the notation $\not \models A$ means that $A$ is not valid, i.e. there are some structures that makes $A$ false. Note that $\not \models A$ does not mean $A \models \,$: a formula could be non-valid but still satisfiable.

According to the aforementioned completeness and soundness theorem (in propositional and first-order logic), the notions of validity and derivability coincide: $ \models A$ if and only if $\vdash A$.

Answer 2

For the first one, yes, $A \vDash$ is often used as shorthand for $A \vDash \bot$, i.e. that $A$ is a contradiction.

I have not seen $A \vdash$ ... though I suppose one could likewise use it for $A \vdash \bot$, i.e. that a contradiction can be syntactically derived from $A$ which, assuming the derivational system under consideration is sound, would imply that $A$ is a contradiction.

Note that if we assume we are dealing with a sound derivational system, a statement being a contradiction would imply that it is not a theorem of the derivational system. But the other way around does not. That is, some statement not being a theorem does not mean it is a contradiciton. For example, for any atomic proposition $A$ we have that $A$ is not a theorem, but obviously $A$ is not a contradiction either, as it is a contingency. So, I would never use $A \vdash$ to mean that $A$ is not a theorem. Indeed, to say that $A$ is not a theorem you'd typically do $\not \vdash A$. So, your comment that it didn't sound right to interpreting $A \vdash$ as $A$ not being a theorem, was spot on.

But again, I suppose one could use $A \vdash$ to indicate that a contradiction can be derived from $A$ (especially if $\bot$ is not a proper symbol of the language you are using). And, if you have a complete derivational system, that would also imply that any statement can be derived from $A$.