Semantic vs syntactic consequence

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

• 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)