Philosophy Stack Exchange is a question and answer site for those interested in logical reasoning. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|improve this question
up vote 6 down vote accepted

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.

share|improve this answer

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.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.