Difference between $ \therefore $ and $ \vdash $ In mathematical logic, what's the difference between the $ \therefore $ and $ \vdash $ symbols?
 A: From my own limited experience, $\vdash$ tends to be used in situations where the logic is completely defined to the level of algorithmic precision.  $\therefore$ tends to be used informally in cases of general reasoning not specific to any logic.
So you might see
$$\begin{array} {rl}
& \text{Jack is the pilot} \\
& \text{The pilot is 6 feet tall} \\ \hline
\therefore & \text{Jack is 6 feet tall}
\end{array}$$
This is just a general reasoning claim.  On the other hand, if you see:
$$x > 7 \vdash x > 3$$
This is a claim about a specific well defined logic, like Robinson Arithmetic for example.  It is saying "the logic in context is strong enough to establish $x > 3$, starting from $x > 7$".  The truth of the claim of such a deduction can be demonstrated with a proof that could be checked by a computer program.  However $\therefore$ tends to only be used in contexts where it wouldn't even make sense to ask for a formal proof.  There are exceptions where sometimes $\therefore$ is meant formally, especially the further back into the past you go.
A: The logical sign $~\therefore~$, known as the Therefore sign and also read therefore, generally used before a logical consequence, such as the conclusion of a syllogism.
For example, 
$(a)~$All humans are mortal. Socrates is a human. $~~~~~∴$ Socrates is mortal.$(b)~$$x + 1 = 10\\
∴ x = 9$
On the other hand, the logical sign $~\vdash~$, known as the Turnstile and read as provable, stands for provability in a certain proof system.
For example, $~x ⊢ y~$ means $~y~$ is provable from $~x~$ (in some specified formal system).
Note:   The later one is also referred to as tee and is often read as yields or proves or satisfies or entails.
A: In my Introduction to Formal Logic (CUP 2003/2020) I take '$\therefore$' to be a symbol that can belong to a formal logical language (e.g. a language for propositional logic) so that we can directly express inferences in that language, as in e.g. '$\mathsf{P, (P \to Q) \therefore Q}$'. After all, you might say, what's the point of using a formal language if you can't directly regiment inferences in it?!
On the other hand '$\vdash$' is not a symbol of the language of propositional logic (or whatever) but abbreviatory shorthand for a bit of English (or Spanish, or whatever language it is in which you are talking about formal languages).  Thus '$\mathsf{P}$', '$\mathsf{(P \to Q)}$' $\vdash$ '$\mathsf{Q}$' is a metalinguistic claim, short for a bit of English, i.e. the claim that there is a derivation [in the currently relevant proof system] from the premisses  '$\mathsf{P}$' and  '$\mathsf{(P \to Q)}$' to the conclusion '$\mathsf{Q}$'.
Conventionally, we drop the explicit quotation marks either side of '$\vdash$' (as it were, we take that symbol to generate its own quotation marks), so we casually write '$\mathsf{P, (P \to Q) \vdash Q}$'. But no matter: it is still a metalinguistic claim about an inference and does not itself express an inference in the way that that '$\mathsf{P, (P \to Q) \therefore Q}$' does.
Thus (in serious use) '$\mathsf{P, (P \to Q) \therefore Q}$' makes three claims, expressed in our our formal language (which claims these are will depend of course on the glossary for the language), and the use of the '$\therefore$' symbol indicates that the third claim is being inferred from the first two. While '$\mathsf{P, (P \to Q) \vdash Q}$' is not an inference; it makes one claim in logician's augmented English, a claim about what follows from what, a claim that tells us that the inference '$\mathsf{P, (P \to Q) \therefore Q}$' is warranted by a proof.
See also this earlier answer of mine: Difference between $\implies$ and $\;\therefore\;\;$?
