Semantic Consequence Definition

Question

"What is the difference between ⊨ (semantic consequence) and ⊢ (syntactic consequence)?" was a question that has been posted, but I am wanting a more specific answer. For example, this video explains what a syntactic consequence is. After watching this video, it is obvious that we say
p ⊢q when p->q is a tautology where p and q are given propositions forming the tautology. What is an easy way to explain what a semantic consequence is? I have been obsessed looking at this question for awhile. Any help would be greatly appreciated.

Answer 1

$\vDash$ means: logical consequence.

The general definition of it is:

A sentence $\varphi$ is said to be a logical consequence of a set of sentences $\Gamma$ (in symbols: $\Gamma \vDash \varphi$) if and only if there is no model $\mathcal {I}$ in which all members of $\Gamma$ are true and $\varphi$ is false.

In the context of propositional logic, this means that:

for every truth assignment (or valuation) $v$, i.e. for every function that assign a truth-value (T or F) to every sentential letter occurring in the formulas in $\Gamma$ or $\varphi$, if $v$ satisfy every formulas in $\Gamma$, then it satisfy also $\varphi$.

Trivial example (where $\Gamma$ has only one formula):

$\{ p \land q \} \vDash p$.

A truth assignment $v$ satisfy $p \land q$ only if $v(p)=v(q)=$ T.

Thus, every truth assignment $v$ that satisfy every formulas in $\Gamma$, i.e. that satisfy $p \land q$, satisfy also $p$.

---

$\Gamma \vdash_{\mathcal S} \varphi$, instead, means that $\varphi$ is derivable (in the proof system $\mathcal S$) from the set of assumptions $\Gamma$.

Answer 2

$\vdash$ is used to make statement about formal proof systems, which include rules of inference, that say:

"If you have a (or two) statement(s) that look like such-and-so, then you can write down a new statement that looks like this-and-that".

For example, many formal proof systems include the following rule of inference called Modus Ponens:

$$\varphi$$

$$\varphi \rightarrow \psi$$

$$\therefore \psi$$

So with this rule, I can, for example, infer $B \land C$ from $A$ and $A \rightarrow (B \land C)$. The fact that I can do this within the proof system we write as: $A, A \rightarrow (B \land C) \vdash B \land C$.

Now, as it so happens, $B \land C$ does in fact logically follow from $A$ and $A \rightarrow (B \land C)$. That is, the way we defined the formal semantics (think truth-tables) is such that whenever $A$ and $A \rightarrow (B \land C)$ are true, $B \land C$ will have to be true as well. And that we write as $A, A \rightarrow (B \land C) \vDash B \land C$.

But maybe the best way to illustrate the difference between $\vdash$ and $\vDash$ is to consider a case where they don't both hold at the same time. So, suppose I write a new logic textbook, and suppose that I develop a very simple system for making formal proofs, in that it has a single rule of inference:

Hokus Ponens

$$\therefore \varphi$$

Now, with Hokus Ponens, I can derive anything from nothing. Thus, for example, it will be true that $P \vdash Q$. Here is the derivation/formal proof:

1. $P$ Premise

2. $Q$ Hokus Ponens!

But obviously, $Q$ does not logically follow from $P$. That is: $P \not \vDash Q$.