Re: [isabelle] --> vs. ==>



Hi Steve,

You may notice that the two implication operators actually have
different types: "==>" has type "prop => prop => prop", where "prop"
is the type of propositions in Isabelle's logical framework. On the
other hand, "-->" has type "bool => bool => bool", with "bool" being
the type of HOL formulae.

The types "bool" and "prop" are related by a special constant
"Trueprop :: bool => prop", which you can think of as the
"is-a-true-HOL-formula" predicate in the logical framework.
Occurrences of "Trueprop" are automatically inserted by Isabelle's
parser just where they are needed, and hidden by the pretty-printer;
however you are free to write them explicitly if you want to.

Here's the precise sense in which --> and ==> are equivalent: For any
P, Q :: bool, "Trueprop (P --> Q)" and "Trueprop P ==> Trueprop Q" are
logically equivalent as propositions. This means that replacing "-->"
with "==>" should preserve the meaning of your theorems. But as Larry
points out, within HOL formulae only "-->" can be used; only the
outermost "-->" (next to an invisible "Trueprop") can be replaced with
"==>".

- Brian

On Fri, Aug 6, 2010 at 2:47 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> The connective ==> is part of the logical framework, and is not part of higher-order logic at all. Therefore, the expression A ==> B is not a higher-order logic formula and cannot be written where a formula is expected, such as a set comprehension.
>
> Larry Paulson
>
>
> On 6 Aug 2010, at 05:23, Steve W wrote:
>
>>
>> I see that both --> and ==> mean implication, whereas the first is the
>> logical connective and the second is for inference rules. However, can a HOL
>> formula containing --> be proved as one with ==> instead? It seems it
>> doesn't make much difference as impI replaces --> by ==>. My feeling is that
>> it's not safe to replace --> with ==>, but what really are the issues?
>>
>
>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.