# Semantical and syntactical derivation notation [duplicate]

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.

• Does this answer your question? Implies ($\Rightarrow$) vs. Entails ($\models$) vs. Provable ($\vdash$) Apr 21, 2020 at 5:34
• @YuiToCheng - Thank you for the link. In my opinion, the two questions are clearly related but this one is not a duplicate of that one. Here the focus is the notion of contradiction, there the focus is on the notion of entailment. Apr 21, 2020 at 6:24
• @YuiToCheng It does not. I know what these two symbols mean, I am asking about the shorthand (where the right side of it is left blank). Apr 21, 2020 at 7:17
• For $A \vDash$, yes: it is a "sloppy" version of $A \vDash \bot$. See also Double turnstile (logic). Apr 21, 2020 at 8:27
• For $A ⊢$, no; to say that $A$ is not a theorem, we have to use $\nvdash A$. See Turnstile (logic). Apr 21, 2020 at 8:29

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

• Regarding $A\vdash$, I wouldn't say it to mean that "you can derive everything" because I think that would implicitly assume the Principle of Exclusion.
– user170039
Apr 21, 2020 at 5:12
• @user170039 - Right, thank you for the comment, but I think that this kind of clarifications are off-topic here. The principle of explosion is accepted in classical logic but also in constructive logics such as intuitionistic logic; only in minimal logic it does not hold. The OP clearly refers to a context where the principle of explosion holds, since it uses the word "contradiction". Apr 21, 2020 at 6:18
• There is also Paraconsistent Logic where it doesn't hold cf. this but where the talk of contradiction makes sense nevertheless.
– user170039
Apr 21, 2020 at 6:56
• I'm not sure to agree... :_) Can you provide some good textbook with a ref to $A \vdash$ ? (except for textbook about sequent calclus, where $A \to$ is used) ? IMO, we have to start from the "canonical" $\Gamma \vdash A$ where $\Gamma$ is a set of formulas (assumptions, axioms) and $A$ a formula, that means that $A$ is derivable from assumptions in $\Gamma$. Then we have $\vdash A$, that is a shorthand for $\emptyset \vdash A$, meaning that $A$ is provable with no assumptions at all (matching with the semantical notion of valid formula, i.e. an "unconditionally" true formula). Apr 21, 2020 at 7:30
• If so, following the above syntax, what $A \vdash$ stand for ? At the right of the $\vdash$ symbol we have to imagine $\emptyset$ ? But to say that from $A$ we cannot derive anything is nosense (at least $A \vdash A$ is reasonable)... The canonical syntax has a formula to the right of $\vdash$: thus, what we mean is the "empty fomula" ? Apr 21, 2020 at 7:32

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

• What does it mean then? $\models A$ is a shorthand for tautology. What do these stand for? Apr 20, 2020 at 20:22
• @SlowerPhoton Just added that to my Post Apr 20, 2020 at 20:27