Semantic Consequence Definition "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.
 A: $\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$.
A: $\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:


*

*$P$ Premise

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