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.

  • 1
    $\begingroup$ Does this answer your question? Implies ($\Rightarrow$) vs. Entails ($\models$) vs. Provable ($\vdash$) $\endgroup$ Apr 21, 2020 at 5:34
  • 2
    $\begingroup$ @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. $\endgroup$ Apr 21, 2020 at 6:24
  • 1
    $\begingroup$ @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). $\endgroup$ Apr 21, 2020 at 7:17
  • 1
    $\begingroup$ For $A \vDash$, yes: it is a "sloppy" version of $A \vDash \bot$. See also Double turnstile (logic). $\endgroup$ Apr 21, 2020 at 8:27
  • 1
    $\begingroup$ For $A ⊢$, no; to say that $A$ is not a theorem, we have to use $\nvdash A$. See Turnstile (logic). $\endgroup$ Apr 21, 2020 at 8:29

2 Answers 2


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

  • $\begingroup$ 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. $\endgroup$
    – user170039
    Apr 21, 2020 at 5:12
  • 1
    $\begingroup$ @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". $\endgroup$ Apr 21, 2020 at 6:18
  • $\begingroup$ There is also Paraconsistent Logic where it doesn't hold cf. this but where the talk of contradiction makes sense nevertheless. $\endgroup$
    – user170039
    Apr 21, 2020 at 6:56
  • $\begingroup$ 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). $\endgroup$ Apr 21, 2020 at 7:30
  • $\begingroup$ 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" ? $\endgroup$ 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$.

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

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