0
$\begingroup$

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?

$\endgroup$
3
  • 1
    $\begingroup$ 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? $\endgroup$
    – paul garrett
    Mar 4, 2022 at 1:54
  • $\begingroup$ @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! $\endgroup$
    – Elliott
    Mar 4, 2022 at 2:04
  • 1
    $\begingroup$ 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.) $\endgroup$
    – ryang
    Mar 4, 2022 at 4:51

1 Answer 1

Reset to default
1
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Thanks so much for your answer. Apologies for my ignorance, but why couldn't we write (𝑝∨𝑟, 𝑝→𝑞) → 𝑟∨𝑞 ? $\endgroup$
    – Elliott
    Mar 4, 2022 at 2:12
  • $\begingroup$ Because that is not a well-formed formula. It also does not clearly convey the intent of "it is provable". @Elliott $\endgroup$
    – Graham Kemp
    Mar 4, 2022 at 2:40
  • $\begingroup$ 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. $\endgroup$
    – Elliott
    Mar 4, 2022 at 2:46
  • $\begingroup$ In terms of it not being a well-formed formula, I thought we could convert , to ∧, so its formal equivalent would be ((𝑝 ∨ 𝑟) ∧ (𝑝 → 𝑞)) → (𝑟 ∨ 𝑞). $\endgroup$
    – Elliott
    Mar 4, 2022 at 3:25

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