Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
1  
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. –  Michael Hardy Jan 17 '13 at 4:06
add comment

5 Answers

up vote 16 down vote accepted

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.

share|improve this answer
    
What do you mean by "formula"? –  alancalvitti Jan 16 '13 at 23:27
7  
@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. –  Clive Newstead Jan 16 '13 at 23:32
1  
@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. –  Clive Newstead Jan 16 '13 at 23:40
1  
@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. –  Peter LeFanu Lumsdaine Jan 16 '13 at 23:51
1  
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. –  gvv Jan 17 '13 at 0:26
show 14 more comments

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

share|improve this answer
    
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? –  alancalvitti Jan 16 '13 at 23:43
1  
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 –  gvv Jan 16 '13 at 23:48
    
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" –  alancalvitti Jan 16 '13 at 23:59
    
I didn't edit my last line. –  gvv Jan 17 '13 at 0:07
    
no problem, I would partially revise my previous comment but it timed out. –  alancalvitti Jan 17 '13 at 0:16
show 2 more comments

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

share|improve this answer
add comment

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.

share|improve this answer
    
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? –  alancalvitti Jan 18 '13 at 17:51
    
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? –  alancalvitti Jan 18 '13 at 17:55
    
"$B$ can be deduced from $A$" is that logically equivalent to $A$ implies $B$?" –  alancalvitti Jan 18 '13 at 19:01
    
Also note the potential (or actual) consistency issues between the answers and comments to this question versus here: math.stackexchange.com/questions/238872/… –  alancalvitti Jan 18 '13 at 19:05
add comment

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

share|improve this answer
    
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$"? –  alancalvitti Jan 18 '13 at 19:02
    
"$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. –  Code-Guru Jan 18 '13 at 23:58
    
What about the above versus "$A$ implies $B$"? –  alancalvitti Jan 19 '13 at 0:00
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.