I see that the double turnstile ⊨ denotes the semantic consequence of some sentence of logic, and single turnstile ⊢ denotes the syntactic consequence of some model. This seems equivalent to me. Why do we need to make this distinction? Are there cases where P⊢Q but P!⊨(does not entail) Q?

4 Answers 4


Interesting question! You used the word 'model' when describing the turnstile, so I'll start with these:

Syntactic consequence Γ ⊢ φ says: sentence φ is provable from the set of assumptions Γ.

Semantic consequence Γ ⊨ φ says: sentence φ is true in all models of Γ.

Models are a semantical notion, so the use of 'model' needs to be avoided in the characterization of syntactic consequence. Now that we're clearer about the definitions of the two types of consequence, I hope you can see that it's not at all obvious that the notions of provability and truth coincide. Significant effort goes into proving the equivalence between a proof system and a semantics for many logics.

Take propositional logic, for example. It has a proof system, the so-called propositional calculus, and a semantics, the so-called truth-tables. The propositional calculus captures the notion of syntactic consequence, truth-tables the notion of semantic consequence. A routine exercise in introductory logic courses is to show that the propositional calculus, in some presentation, is sound with respect to the truth-tables, i.e. that:

Soundness. If [Γ ⊢ φ] then [Γ ⊨ φ].

Although the proof is easy, it still needs to be shown; otherwise we'd have to take it on faith that our axioms (if we have any) are true and that our rules of inference are truth-preserving. Similarly for the converse direction, which is called completeness:

Completeness. If [Γ ⊨ φ] then [Γ ⊢ φ].

This one is usually much harder to prove, and is important because we want the proof system to capture or prove all the truths our semantics generates. Propositional logic enjoys both properties, but there are logics for which such proofs either have not yet been or cannot be devised.

  • Do you mind clarifying a bit more on your definition of semantic consequence? The phrase 'true in all models of...' is still quite unclear to me. The term 'models' in the present context eludes me. Thank you.
    – Anthony
    Commented Jul 25, 2018 at 7:47
  • What makes semantic different from syntactic consequence is that something, in this case the "model", needs to assign truth-values to the formulas for the relation to hold. I mentioned truth-tables above; that's a model of propositional logic. Commented Jul 25, 2018 at 15:24
  • 1
    Why doesn't mathjax or Latex work in comments?
    – john
    Commented Dec 25, 2019 at 22:12
  • 1
    @Anthony A model of a sentence, or set of sentences, is an interpretation that makes the sentence, or set of sentences, all true. For example a model of the sentence p v q is p= T , q = F since T v F = T.
    – john
    Commented Dec 25, 2019 at 22:16

Syntactic consequence (A ⊢ B): B can be derived from A without even knowing if A is true. For example, 'A implies B' can be converted to 'notA or B', regardless if 'A implies B' was true or false. It's a syntactic consequence. The model (all possible ways to get A to be true) doesn't matter because truth doesn't matter, because A being true doesn't even matter.

Semantic consequence (C |= D): Whenever C is true, then D is true.

What is a model?: A model is just one combination of symbols that make the well-formed formula to be true: we have 3 possible models in A ∨ B, which are A=true,B=false, A=false,B=true and A=true,B=true. If whenever the left side (C) of semantic consequence is true, D is also true, then C semantically entails D.

The symbols are called syntactic turnstile and semantic turnstile respectively, and in Latex they are written with \vdash and \vDash.

  • 2
    This answer is designed for someone new to potentially understand other answers in the future. It took me a while to understand semantic vs syntactic consequence, as the other explanations assume quite a lot of prerequisite knowledge & comfort in using logic words. Commented Apr 30, 2020 at 7:41
  • It’s a good answer! I think the notion of a model can be a bit more intricate than just being about which statements are true (e.g. you can have what we call “non-canonical models” that make the same statements true but have different domains), but from the perspective of logic, especially classical first order logic, what matters for semantic consequence is the assignment of truth values. Commented Apr 30, 2020 at 13:18

We need the distinction because the two concepts are different [see Hunan's explanation].

There are theorems regarding the equivalence between the two concepts both for propositional logic (see : Soundness and completeness of the rules) and first-order logic (see : Gödel's completeness theorem ).

For second-order logic this is not true anymore.

See also this post.

  • There are two ways of explaining that a reasoning is valid .

Consider this reasoning :

(1) If Socrates is a man, then Socrates is mortal.

(2) Socrates is not mortal.

(3) Therefore, Socrates is not a man.

  • In order to explain why this reasoning is valid you could say two things:

(1) First you could say that the conclusion is obtained following mechanically an accepted rule, namely the rule : " From (X --> Y) and not-Y, inder not-X" . This is the syntactic concept of validity : the reasoning is valid, since it is a string of sentences that is correctly constructed, , according to a given rule.

(2) But you could also say that the reasoning is valid because there is no possible case / situation / interpretation / world in which the premises are true and the conclusion is false, or, equivalently, that the reasoning is valid because, given the premises, the negation of the conclusion would be absurd. This is the semantic concept of validity.

  • Other example. Suppose that a, b , c and d can only take values 0, 1 or 2 . In order to show the validity of

(1) X = a+(b+(c+d) )

(2) Therefore X = (a+b) + (c+d)

you could either consider the 81 possibilities of value assignments to a, b, c and d and conclude that whatever number a, b, c and d denote if the premise is true the conclusion holds ( semantic approach) or say that the conclusion is obtained by applying mechanically a reliable syntactic rule of algebra ( namely, the associative property of addition)

You must log in to answer this question.

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