# Difference between implies and "turnstile" symbols (→ and ⊢) [duplicate]

According to Wikipedia's list of logic symbols:

A → B means A → B is false when A is true and B is false but true otherwise.

A ⊢ B means x ⊢ y means x proves (syntactically entails) y

But for me I can't see how they aren't equivalent. If a set of theorems/lemmas, A, can be used to derive another set of proofs/lemmas, B, then doesn't A imply B?

Googling around on this topic it seems that ⊢ may just be a "stronger" version of →. I know that we often use → for little steps in logic, and it seems that ⊢ is more used for larger steps.

Then I found this part of an answer in a question about symbol standardisation:

Now 'A implies B' gets used in informal talk both as variant on 'if A then B' and as a variant of 'A logically entails B', i.e. as both what we might regiment as 𝐴→𝐵 and as 𝐴⊢𝐵 [or 𝐴⊨𝐵]. And low and behold, we find ⟹ being confusingly used both ways [in the object language, or in the metalanguage]. Conservatism in symbolism is a Good Thing, so I think the use of ⟹ is to be deprecated: I'd say, use → for an object language conditional, and the appropriate turnstile in metalanguage.

(Emphasis mine)

So this would imply to me that → and ⊢ are equivalent, but it's idiomatic to use ⊢ for metamathematics, and → otherwise. Or, more concretely:

(A → B) → (C → D) is the same as (A → B) ⊢ (C → D), but the second option is considered more idiomatic/readable as we differentiate the smaller connections from the larger ones.

Is this right?

• Well, also, $A\to B$ makes sense in propositional logic, which is not rich enough to talk about "entailment": it's just (as you say), an assertion about the four possible combinations of true or false for $A$ and $B$. Not about "proving" anything... The A-proves-B symbol has more depth to it: there's a reason/proof for the truth of one, given the truth of the other (essentially). Is this vaguely responding to your question? Mar 4, 2022 at 1:54
• @paulgarrett, thank you. I'm just getting into learning logic, and felt I couldn't get started without knowing the difference. I think that the strictness of "→" is lost on me at the moment - but you've helped me know where to look next. Thanks! Mar 4, 2022 at 2:04
• This is my understanding/summary; I also like (and upvoted) Peter Smith's answer on the same page. (Caveat: the word "implication" and symbol "⇒" does really have multiple usage agreements.) Mar 4, 2022 at 4:51

So this would imply to me that → and ⊢ are equivalent,

No, it means they are distinct application of a similar concept in different environments.

• $$\to$$ is used as a logical connective in a statement; the material conditional.
• $$\vdash$$ is used to indicate syntactic entailment between sets of statements; a sequent.$$p\vee r, p\to q ~\vdash~ r\lor q$$

The reason the $$\implies$$ symbol is being depreciated, is because using the same symbol for these purposes is quite confusing.

A syntactic entailment means that when given a set of premises, the consequent may be derived using some specified set of axioms and rules of inference.

• Thanks so much for your answer. Apologies for my ignorance, but why couldn't we write (𝑝∨𝑟, 𝑝→𝑞) → 𝑟∨𝑞 ? Mar 4, 2022 at 2:12
• Because that is not a well-formed formula. It also does not clearly convey the intent of "it is provable". @Elliott Mar 4, 2022 at 2:40
• Okay, thanks again. So if I understand you, the difference is that A → B is a function that outputs true if A implies B, but false otherwise; but A ⊢ B is the written claim that A implies B. Is that right? If so, it seems like the syntax is backwards. Mar 4, 2022 at 2:46
• In terms of it not being a well-formed formula, I thought we could convert , to ∧, so its formal equivalent would be ((𝑝 ∨ 𝑟) ∧ (𝑝 → 𝑞)) → (𝑟 ∨ 𝑞). Mar 4, 2022 at 3:25