2
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ For those interested in Proof Assistants, there is a new proposed SE site ProofAssistants $\endgroup$
    – Guy Coder
    Nov 28, 2021 at 8:34

1 Answer 1

3
$\begingroup$

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$" (-->).

Further useful reading:

$\endgroup$
11
  • $\begingroup$ Thank you. And why do we have to make this distinction? For example, in Lean Peover there is no such distinction. There is only -> and it performs all functinalities. $\endgroup$
    – user56834
    Dec 13, 2021 at 5:31
  • $\begingroup$ Well, the Lean prover is not a metalogical framework, unlike Isabelle. The goal for having a metalogical framework is that you can "reason in any deductive system". That is to say, a metalogical framework effectively acts like a "functional core" for building a theorem prover (which is why you have Isabelle/X, where X = HOL or ZF or ...). You could have Isabelle/Lean. OTOH, Lean is not a metalogical framework: it's just a theorem prover built atop CoC. $\endgroup$ Dec 13, 2021 at 14:31
  • $\begingroup$ @user56834 Understandably, this doesn't answer the question, "But, why?" Well, if you are familiar with logical frameworks (if not, see (1), (2), (3)), then a natural question is, "Can I do more than just describe and prove results about a deductive system? Can I use it to reason within a deductive system?" A logical framework alone cannot do it. We need more! $\endgroup$ Dec 13, 2021 at 14:39
  • $\begingroup$ 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. $\endgroup$ Dec 14, 2021 at 2:36
  • $\begingroup$ I see. I think then my question becomes, why is it helpful to separate constructs like arrows for the object and meta-language respectively in a theorem prover (given that e.g. Lean works without it)? But perhaps this should be a different post. $\endgroup$
    – user56834
    Dec 14, 2021 at 5:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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