Email Gateway (Aug 18 2022 at 15:46): Email Gateway (Aug 18 2022 at 15:46):From: Steve W <s.wong.731@gmail.com>
Hi,
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?
Thanks
Steve
Email Gateway (Aug 18 2022 at 15:47):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 15:47):From: Brian Huffman <brianh@cs.pdx.edu>
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
"==>".
Last updated: Nov 21 2024 at 12:39 UTC