# Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?

I haven't been able to find a good explanation of how these are different and relate to each other. I know that $$\to$$ is part of HOL and $$\Rightarrow$$ and $$\Longrightarrow$$ part of Isabelle, but it seems that they are basically doing the same thing and we could just have one object $$\to$$? (Taking into account the CH correspondence). Why does Isabelle/HOL have 3 operators for essentially the same thing? How are they different?

• For those interested in Proof Assistants, there is a new proposed SE site ProofAssistants Nov 28, 2021 at 8:34

I haven't been able to find a good explanation of how these are different and relate to each other. I know that → is part of HOL and ⇒ and ⟹ part of Isabelle, but it seems that they are basically doing the same thing and we could just have one object →? (Taking into account the CH correspondence).

The basic answer is because it depends on whether you want implication in the metalanguage ($$\Longrightarrow$$ or ==>) or the object language (all other arrows), since Isabelle is a "metalogical framework" for reasoning within a specific "object logic".

Curry-Howard is relevant for the metalogic. If you try to use Curry-Howard with the object logic, you get an "object level" correspondence, which is already implicit in the object logic.

According to the documentation:

• $$P\to Q$$ (ascii P --> Q) is for "object language" logical implication "$$P$$ implies $$Q$$", i.e., implication in the object logic (encoding, e.g., implication in HOL); this is not part of the Isabelle's underlying "meta" logic;
• $$\tau_{1}\Rightarrow\tau_{2}$$ (ascii tau => tau) is used in Isabelle/HOL for the [total] function HOL type from HOL type $$\tau_{1}$$ to produce a HOL term of HOL type $$\tau_{2}$$;
• $$\Longrightarrow$$ (ascii ==>) is the "meta-implication", i.e., the implication in the "metalogical framework" [i.e., the Pure language]. It's used for encoding "object logic" inference rules; if used for stating theorems, then those theorems may be used directly with forward or backward chaining (whereas theorems stated using --> needs to invoke implication inference rules), as Paulson tells us.

Really, you should use "$$\Longrightarrow$$" (==>) as much as possible when stating theorems. But there are times when you want to state in the object logic "$$P$$ implies $$Q$$"...and that requires "$$\to$$" (-->).

• But why are there multiple arrows? That's like asking, "Why does French have the verb être when we already have 'to be' in English?" Well, English is the metalanguage, French is the object language; just as ==> is the implication in the metalanguage, the object language has its own arrows...because arrows are useful. Dec 14, 2021 at 2:36