20
$\begingroup$

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?

$\endgroup$
2
  • 2
    $\begingroup$ I see you've accepted an answer. But before you go away, you should look at my answer, since it addresses some points that the others don't that are worth being aware of. $\endgroup$
    – Michael Hardy
    Jan 17, 2013 at 4:06
  • $\begingroup$ I too am using this textbook and I will bookmark this post for that chapter when I get there. I've used other Discrete Math books but this one in particular is good at forming the picture so I don't forget things. However, there are accounts, such as you have described, where they are a bit vague and I have to look elsewhere to find the answers I want. $\endgroup$
    – bjd2385
    Jan 22, 2015 at 14:28

5 Answers 5

Reset to default
23
$\begingroup$

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.

$\endgroup$
19
  • $\begingroup$ What do you mean by "formula"? $\endgroup$
    – alancalvitti
    Jan 16, 2013 at 23:27
  • 9
    $\begingroup$ @alancalvitti: I don't really get what you're saying. I'm trying to explain syntactic entailment to someone with little grounding in formal logic, so I don't want to get hung up on technical definitions or philosophical points. $\endgroup$
    – Clive Newstead
    Jan 16, 2013 at 23:32
  • 1
    $\begingroup$ @alancalvitti: I was referring to the question-asker, not yourself $-$ I thought you were asking these questions on their behalf (because of shortcomings in my answer). The comment box isn't really a place for these questions though. If you want to learn about these things, there are plenty of good resources, websites and textbooks on the subject, or you could ask a new question here. $\endgroup$
    – Clive Newstead
    Jan 16, 2013 at 23:40
  • 1
    $\begingroup$ @alancalvitti: both are correct and (in standard systems) synonymous, but at least in my experience, entailment is used more often for the analogous semantic notion (usually denoted $\vDash$), while implication and provability are more common for this syntactic notion. $\endgroup$
    – Peter LeFanu Lumsdaine
    Jan 16, 2013 at 23:51
  • 1
    $\begingroup$ Derivations depend on the logical calculus you are using. For example, if you're using an axiomatic calculus, you can derive formulas by just following the axioms, thus you have derived something without any assumptions. However, if you are using another calculus, for example Natural Deduction Calculus, ⊢ A iff you can derive A without any open assumptions. $\endgroup$
    – ggg
    Jan 17, 2013 at 0:26
10
$\begingroup$

⊢ 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.

$\endgroup$
7
  • $\begingroup$ You wrote "syntactic implication" whereas Newstead wrote "syntactic entailment". Which is correct? Or can either one be syntactically derived from the other? Or perhaps semantically? $\endgroup$
    – alancalvitti
    Jan 16, 2013 at 23:43
  • 1
    $\begingroup$ Honestly, I don't think we meant anything different. I think syntactic entailment/consequence would be better, and will edit my answer now. This could help clarify though: en.wikipedia.org/wiki/Logical_consequence $\endgroup$
    – ggg
    Jan 16, 2013 at 23:48
  • $\begingroup$ I want you to acknowledge that you edited your answer (first line) from "syntactic implication" to "syntactic entailment" and (last line) from "syntactic implication" to "semantic entailment" $\endgroup$
    – alancalvitti
    Jan 16, 2013 at 23:59
  • $\begingroup$ I didn't edit my last line. $\endgroup$
    – ggg
    Jan 17, 2013 at 0:07
  • $\begingroup$ no problem, I would partially revise my previous comment but it timed out. $\endgroup$
    – alancalvitti
    Jan 17, 2013 at 0:16
6
$\begingroup$

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

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ How would one know if $A\models B$ in case there is an open-ended or unbounded list of models? Wouldn't there have to be an algorithm for deciding (presumably based on some reasonable system of deduction) when $A$ and $B$ are true (or false) in all model instances? $\endgroup$
    – alancalvitti
    Jan 18, 2013 at 17:51
  • $\begingroup$ Also, when you write "at the very least..there is an algorithm for deciding which deductions are valid: ('effectiveness')" does this mean that $A\vdash B$ only applies to constructive math systems, typically characterized, eg by McLarty as having: no Choice, no Excluded Middle, exhibit specific instances of solutions? $\endgroup$
    – alancalvitti
    Jan 18, 2013 at 17:55
  • $\begingroup$ "$B$ can be deduced from $A$" is that logically equivalent to $A$ implies $B$?" $\endgroup$
    – alancalvitti
    Jan 18, 2013 at 19:01
  • 1
    $\begingroup$ Also note the potential (or actual) consistency issues between the answers and comments to this question versus here: math.stackexchange.com/questions/238872/… $\endgroup$
    – alancalvitti
    Jan 18, 2013 at 19:05
4
$\begingroup$

I usually read $\vdash$ as "entails". You can also use "proves".

$\endgroup$
3
  • $\begingroup$ Is your interpretation consistent with Michael Hardy's? He wrote "$A \vdash B$ means $B$ can be deduced from $A$". Is that logically equivalent to "$A$ proves $B$"? $\endgroup$
    – alancalvitti
    Jan 18, 2013 at 19:02
  • $\begingroup$ "$A$ proves $B$ uses the word "proves" loosely. I believe it conveys the same meaning and is less wordy than "$B$ can be deduced from $A$" which is more technically accurate. Of course, "$A$ entails $B$" is also technically accurate, but uses a word which is unfamiliar to many. $\endgroup$
    – Code-Guru
    Jan 18, 2013 at 23:58
  • $\begingroup$ What about the above versus "$A$ implies $B$"? $\endgroup$
    – alancalvitti
    Jan 19, 2013 at 0:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .