8
$\begingroup$

This question already has an answer here:

I do not understand the difference between $\rightarrow$ and $\Rightarrow$. Sometimes I see implication truth tables labeled with the former, sometimes with the latter.

Aren't they synonyms of logical implication or is there any difference?

$\endgroup$

marked as duplicate by Asaf Karagila logic Jun 26 '17 at 17:37

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

7
$\begingroup$

There is no universally observed difference between the two symbols.

$\Rightarrow$ tends to be used more often in undergraduate instruction, where the logical symbols are used to explain and elucidate ordinary mathematical arguments -- for example, in real analysis.

$\to$ tends to be favored in formal mathematical logic, where the focus is modeling ordinary mathematical arguments as formal mathematical objects that follow precise rules and can be studied as a subject in themselves.

But this split is not observed by all authors, and you cannot expect that a random text you encounter will be following it.

$\endgroup$
7
$\begingroup$

Usually, $\Rightarrow$ denotes implication in the metalanguage, whereas $\rightarrow$ denotes implication in the formal language that you want to talk about. For example, $$M \models \sigma \rightarrow \tau \ \Rightarrow \ M \models \rho$$ is translated as "if $M$ is a model of $\sigma \rightarrow \tau$, then $M$ is a model of $\rho$".

$\endgroup$
  • 1
    $\begingroup$ this may be a bit clearer if you write "formal language" in place of "language". $\endgroup$ – Mikhail Katz Jun 26 '17 at 17:22
  • $\begingroup$ @MikhailKatz Thank you, I edited my answer. $\endgroup$ – Sumac Jun 26 '17 at 17:25
5
$\begingroup$

As far as I'm aware, these two symbols mean the same thing. In my limited experience, Logicians seem to use "$\rightarrow$", while people not studying logic seem to use $"\implies"$ more often.

$\endgroup$
  • 6
    $\begingroup$ In particular, authors who have call to use $\to$ a lot in reference to functions will often use $\Rightarrow$ to avoid overloading one symbol. $\endgroup$ – Malice Vidrine Jun 26 '17 at 15:31
  • $\begingroup$ Indeed, thanks for the contribution. $\endgroup$ – Antonios-Alexandros Robotis Jun 26 '17 at 15:32
  • 1
    $\begingroup$ @MaliceVidrine: But on the other hand, authors making use of the Curry-Howard correspondence will want to use $\to$ for both function types and implications. $\endgroup$ – Henning Makholm Jun 26 '17 at 15:33
  • $\begingroup$ @HenningMakholm Even with the Curry-Howard correspondence, there's often actual as well as conventional reasons to make the distinction. For example, both Coq and HoTT have an explicit notion of "proposition" distinct from (an arbitrary) type. NuPRL doesn't have this distinction, but still defines notational variants for clarity of intent. $\endgroup$ – Derek Elkins Jun 26 '17 at 21:49
4
$\begingroup$

As others have said, in practice both are used for the material conditional, and I certainly wouldn't want to say that someone is 'wrong' in using the one symbol rather than the other, but personally I have my reasons for separating between the two:

I use $\rightarrow$ for the material conditional, so that I can use the $\Rightarrow$ for logical implication. For example, I would use $P \land Q \Rightarrow P$ to make the meta-logical statement that the logic statement $P$ is logically implied by the logic statement $P \land Q$. Likewise, I use $\leftrightarrow$ for the material biconditional, and $\Leftrightarrow$ to express logical equivalence. For example: $P \leftrightarrow Q \Leftrightarrow Q \leftrightarrow P$ expresses the meta-logical statement that the logic statement $P \leftrightarrow Q$ is logically equivalent to the logic statement $Q \leftrightarrow P$ (of course, some use $\equiv$ to express logical equivalence, but I have also seen $\equiv$ used to express the material conditional ...)

In short: people use different symbols, and that's just fine as long as you make clear what they mean and how you use them, but to me the single horizontal line signals something about the syntax of logic, while the double line to me signals something semantical. Indeed, in my eyes this distinction mirrors the distinction between $\vdash$ and $\vDash$ where $\vdash$ is about purely syntactical derivations, and the $\vDash$ is about semantical implication.

$\endgroup$
3
$\begingroup$

There's a subtle difference. "$P\rightarrow Q$" is the statement that $P$ implies $Q$, which may be a true or false statement. "$P \Rightarrow Q$" is the assertion that $P\rightarrow Q$ is true.

$\endgroup$
  • $\begingroup$ But what's the difference? Any assertion may be a true or false statement. $\endgroup$ – Dan Brumleve Jun 26 '17 at 15:52
  • 1
    $\begingroup$ @DanBrumleve When you say $P\Rightarrow Q$, you're saying it's not false. $\endgroup$ – B. Goddard Jun 26 '17 at 15:59
  • $\begingroup$ Then what are you saying when you say $P \rightarrow Q$? Maybe you are saying $P \rightarrow Q$ should be used as a term rather than a formula, so it's not something you can say or assert, but I don't think this is very clear. $\endgroup$ – Dan Brumleve Jun 26 '17 at 22:08
  • $\begingroup$ @DanBrumleve I said it was a subtle difference. "$P\rightarrow Q$" can be part of a more complex statement. The $\rightarrow$ is a connective like AND and OR, eve though we read it as a verb. The $\Rightarrow$ is a verb. $\endgroup$ – B. Goddard Jun 26 '17 at 22:34

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