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?


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 Jul 25 '18 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. – Hunan Rostomyan Jul 25 '18 at 15:24
  • Why doesn't mathjax or Latex work in comments? – john Dec 25 '19 at 22:12
  • @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 Dec 25 '19 at 22:16

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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