C.Sternagel answered your title question "How?", which satisfied your last sentence, but I go ahead and fill in some details based on his answer, to try to "help [you] understand the difference".
It can be confusing that there is ==>
and -->
, meta-implication and HOL-implication, and that they both have the properties of logical implication. (I don't say much about !!
and !
, meta-all and HOL-all, because what's said about ==>
and -->
can be mostly be transferred to them.)
(NOTE: I convert graphical characters to equivalent ASCII when I can, to make sure they display correctly in all browsers.)
First, I give some references:
- [1] Isabelle/Isar Reference manual.
- [2] HOL/HOL.thy
- [3] Logic in Computer Science, by Huth and Ryan
- [4] Wiki sequent entry.
- [5] Wiki intuitionistic logic entry.
If you understand a few basics, there's nothing that confusing about the fact that there is both ==>
and -->
. Much of the confusion departs, and what's left is just the work of digging through the details about what particular source statements mean, such as the formula of C.Sternagel's first lemma.
"(!!x. P x ==> P y) == (Trueprop (!x. P x --> P y))"
C.Sternagel stopped taking the time to give me important answers, but the formula he gives you above is similar to one he gave me a while ago, to convince me that all free variables in a formula are universally quantified.
Short answer: The difference between ==>
and -->
is that ==>
(somewhat) plays the part of the turnstile symbol, |-
, of a non-generalized sequent in which there is only one conclusion on the right-hand side. That is, ==>
, the meta-logic implication operator of Isabelle/Pure, is used to define the Isabelle/HOL implication object-logic operator -->
, as shown by impI
in the following axiomatization
in HOL.thy
[2].
(*line 56*)
typedecl bool
judgment
Trueprop :: "bool => prop"
(*line 166*)
axiomatization where
impI: "(P ==> Q) ==> P-->Q" and
mp: "[| P-->Q; P |] ==> Q" and
iff: "(P-->Q) --> (Q-->P) --> (P=Q)" and
True_or_False: "(P=True) | (P=False)"
Above, I show the definition of three other axioms: mp
(modus ponuns), iff
, and True_or_False
(law of excluded middle). I do that to repeatedly show how ==>
is used to define the axioms and operators of the HOL logic. I also threw in the judgement
to show that some of the sequent vocabulary is used in the language Isar.
I also show the axiom True_or_False
to show that the Isabelle/HOL logic has an axiom which Isabelle/Pure doesn't have, the law of excluded middle [5]. This is huge in answering your question "what is the difference?"
It was a recent answer by A.Lochbihler that finally gave meaning, for me, to "intuitionistic" [5]. I had repeatedly seen "intuitionistic" in the Isabelle literature, but it didn't sink in.
If you can understand the differences in the next source, then you can see that there's a big difference between ==>
and -->
, and between types prop
and bool
, where prop
is the type of meta-logic propositions, as opposed to bool
, which is the type of the HOL logic proposition. In the HOL object-logic, False
implies any proposition Q::bool
. However, False::bool
doesn't imply any proposition Q::prop
.
The type prop
is a big part of the meta-logic team !!
, ==>
, and ==
.
theorem "(!!P. P::bool) == Trueprop (False::bool)"
by(rule equal_intr_rule, auto)
theorem HOL_False_meta_implies_any_prop_Q:
"(!!P. P::bool) ==> PROP Q"
(*Currently, trying by(auto) will hang my machine due to blast, which is know
to be a problem, and supposedly is fixed in the current repository. With
`Auto methods` on in the options, it tries `auto`, thus it will hang it.*)
oops
theorem HOL_False_meta_implies_any_bool_Q:
"(!!P. P::bool) ==> Q::bool"
by(rule meta_allE)
theorem HOL_False_obj_implies_any_bool_Q:
"(!P. P::bool) --> Q::bool"
by(auto)
When you understand that Isabelle/Pure meta-logic ==>
is used to define the HOL logic, and other differences, such as that the meta-logic is weaker because of no excluded middle, then you understand that there are significant differences between the meta-operators, !!
, ==>
, and ==
, in comparison to the HOL object-logic operators, !
, -->
, and =
.
From here, I put in more details, partly to convince any expert that I'm not totally abusing the word sequent
, where my use here is based primarily on how it's used in reference [3, Huth and Ryan].
Attempting to not write a book
I throw in some quotes and references to show that there's a relationship between sequents and ==>
.
From my research, I can't see that the word "sequent" is standardized. As far as I can tell, in [3.pg 5], Huth and Ryan use "sequent" to mean a sequent which has only has one conclusion on the right-hand side.
...This intention we denote by
phi1, phi2, ..., phiN |- psi
This expression is called a sequent; it is valid if a proof can be found.
A more narrow definition of sequent, in which the right-hand side has only one conclusion, matches up very nicely with the use of ==>
.
We can blame L.Paulson for confusing us by separating the meta-logic from the object-logic, though we can thank him for giving us a larger logical playground.
Maybe to keep from clashing with the common definition of a sequent, as in [4, Wiki], he uses the phrase natural deduction sequent calculus
in various places in the literature. In any case, the use of ==>
is completely related to implementing natural deduction rules in the logic of Isabelle/HOL.
Even with generalized sequents, L.Paulson prefers the ==>
notation:
You asked about differences. I throw in some source related to C.Sternagel's answer, along with the impI
axiomatization again:
(*line 166*)
axiomatization where
impI: "(P ==> Q) ==> P-->Q"
(*706*)
lemma --"atomize_all [atomize]:"
"(!!x. P x) == Trueprop (ALL x. P x)"
by(rule atomize_all)
(*715*)
lemma --"atomize_imp [atomize]:"
"(A ==> B) == Trueprop (A --> B)"
by(rule atomize_imp)
(*line 304*)
lemma --"allI:"
assumes "!!x::'a. P(x)"
shows "ALL x. P(x)"
by(auto simp only: assms allI
I put impI
in structured proof format:
lemma impI_again:
assumes "P ==> Q"
shows "P --> Q"
by(simp add: assms)
Now, consider ==>
to be the use of the sequent turnstile, and shows
to be the sequent notation horizontal bar, then you have the following sequent:
P |- Q
-------
P --> Q
This is the natural deduction implication introduction rule, as the axiom name says, impI
(Cornell Lecture 15).
The Big Guys have been on top of all of this for a long time. See [1, Section 2.1, page 27] for an overview of !!
, ==>
, and ==
. In particular, it says
The Pure logic [38, 39] is an intuitionistic fragment of higher-order logic
[13]. In type-theoretic parlance, there are three levels of lambda-calculus with
corresponding arrows =>
/!!/==>`...
One general significance of the statement is that in the use of Isabelle/HOL, you are using two logics, a meta-logic and an object-logic, where those two terms come from L.Paulson, and where "intuitionistic" is a key defining point of the meta-logic.
See also [1, Section 9.4.1, Simulating sequents by natural deduction, pg 206]. According to M.Wenzel on the IsaUsersList, L.Paulson wrote this section. On page 205, Paulson first takes the definition of a sequent to be the generalized definition. On page 206, he then shows how you can line up one type of sequent with the use of ==>
, which is by negating every proposition on the right-hand side of a sequent, except for one of them.
That, by all appearances, is a horn clause, which I know nothing about.
It seems obvious to me that using ==>
is the use of a limited form of sequents. In any event, that's how I think of it, and thinking that way has given me an understanding of the differences between ==>
and -->
, along with the fact that the meta-logic has no excluded middle.
If A.Lochbhiler wouldn't have pointed out the absence of an excluded middle, I wouldn't have seen an important difference of what's possible with ==>
, and what's possible with -->
.
Maybe C.Sternagel will start back again to give me some of his important answers.
Please pardon the long answer.