How to evaluate the single turnstile symbol ($\vdash$) in propositional logic?

Question

Wikipedia says, that:

$x \vdash y$ means y is provable from x (in some specified formal system).

But what do you actually check or calculate, when you have $(a \land \lnot b) \vdash a$? Has $(a \land \lnot b)$ to be true for at least all combinations of a and b whenever $a$ is true or does this belong to the double turnstile symbol ($\vDash$)?

Answer 1

The "turnstile" symbol, used in the context $\Gamma \vdash \varphi$, means that, relative to the proof system we are working with, there is a derivation of the formula $\varphi$ from the formulae in $\Gamma$ with the rules and logical axioms of the proof system.

In the Natural Deduction proof system, we can build-up this simple derivation :

1) $a \land \lnot b$ --- premise

2) $a$ --- from 1) by Conjunction elimination

showing that : $a \land \lnot b \vdash a$.

If the proof system is complete, i.e. if the Completeness Theorem saying that :

if $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$

applies, as is the case for the "usual" proof systems for propositional and first-order logic, like Natural Deduction, we can take benefit of it proving deducibility from (tauto)logical consequence.

In propositional logic we can show that :

$a \land \lnot b \vDash a$;

with truth-table or through the definition of (tauto)logical consequence, i.e. the conclusion : $a$ must be true for any truth assignment that satisfy the premise : $a \land \lnot b$.

Having done this, we can use the completeness of propositional logic to conclude that there is a derivation of $a$ from $a \land \lnot b$, i.e. that :

$a \land \lnot b \vdash a$.