Notation Question: What does $\vdash$ mean in logic?

In a "math structures" class at the community college I'm attending (uses the book Discrete Math by Epp, and is basically a discrete math "light" edition), we've been covering some basic logic.

I've been reading some of the logic questions on here to get used to notation, etc. However, when I came across the question Visualizing Concepts in Mathematical Logic, I didn't understand what the $\vdash$ symbol means.

It's not in Discrete Math by Epp, nor is it in my mom's old logic book from when she went to college.

Wikipedia's Math Symbols page says it means "can be derived from" when used in a logic context. However, that doesn't make any sense in the above question, as there is nothing on the left of the $\vdash$.

So, what does $\vdash$ mean, especially in the context of the question linked above?

Solution 1:

Let $S$ be a set of (logical) formulae and $\psi$ be a formula. Then $S \vdash \psi$ means that $\psi$ can be derived from the formulae in $S$. Intuitively, $S$ is a list of assumptions, and $S \vdash \psi$ if we can prove $\psi$ from the assumptions in $S$.

$\vdash \psi$ is shorthand for $\varnothing \vdash \psi$. That is, $\psi$ can be derived with no assumptions, so that in some sense, $\psi$ is 'true').

More precisely, systems of logic consist of certain axioms and rules of inference (one such rule being "from $\phi$ and $\phi \to \psi$ we can infer $\psi$"). What it means for $\psi$ to be 'derivable' from a set $S$ of formulae is that in a finite number of steps you can work with (i) the formulae in $S$, (ii) the axioms of your logical system, and (iii) the rules of inference, and end up with $\psi$.

In particular, if $\vdash \psi$ then $\psi$ can be derived solely from the axioms by using the rules of inference in your logical system.

Solution 2:

⊢ means "can be derived from" or "proves", and denotes syntactic entailment. For example, let G be a set of sentences in logic, and A be any sentence in logic. G ⊢ A (read: G proves A) iff A can be derived using only the sentences in G as assumptions. Thus, if for a certain A we have ⊢ A, then A can be derived without any open assumptions.

Note that ⊢ is different than ⊨, which stands for semantic entailment.

Solution 3:

It's called a 'turnstile'. See here: http://en.wikipedia.org/wiki/Turnstile_(symbol)

Solution 4:

We should attend to a distinction between "$\vdash$" and "$\models$". The notation $A\vdash B$ means $B$ can be deduced from $A$ in some reasonable system of deduction, and "reasonable" should mean at the very least

• There is an algorithm for deciding which deductions are valid ("effectiveness"); and
• If $B$ can be deduced from $A$ then $B$ is true in every structure in which $A$ is true (soundness).

One may also have

• If $B$ is true in every structure in which $A$ is true, then $A\vdash B$ (completeness).

(The word "completeness" here should not be confused with the "completeness" referred to in Gödel's incompleteness theorem; that is different.)

The notation $A\models B$ means simply that $B$ is true in every structure in which $A$ is true.