Email Gateway (Aug 22 2022 at 15:58): Email Gateway (Aug 22 2022 at 15:58):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
Dear Isabelle community,
is there a particular reason for having "iff" as an axiom in HOL?
As far as I can see it follows from the other axioms, in particular
"True_or_False", "mp" and "refl", using the various elimination rules of
"False", "disj" and "iff" (which do not depend on axiom "iff" themselves).
Or am I mistaken?
Best regards,
Alexander Maletzky
Email Gateway (Aug 22 2022 at 15:58):From: David Cock <david.cock@inf.ethz.ch>
Have you tried removing the axiom and reproving it from the others?
David
Email Gateway (Aug 22 2022 at 15:59):From: Makarius <makarius@sketis.net>
The axiomatic basis of Isabelle/HOL goes back to the paper on HOL by
Mike Gordon (1985) and ultimately to Alonzo Church (1940). Over the
decades, better understanding of varieties of HOL has emerged and today
one would certainly do it quite differently as a fresh start.
Here is a recent presentation of mine about "Foundations of Higher-Order
Logic" at Curry Club Augsburg
http://sketis.net/2016/foundations-of-higher-order-logic-at-curry-club-augsburg
with a formalization of HOL based on minimal logic. There is even a
video of the talk (in German): https://www.youtube.com/watch?v=R8pyFwil9KY
This might help to understand the bigger picture. It does not mean
anything at the bottom of Isabelle/HOL needs to be changed.
Makarius
Email Gateway (Aug 22 2022 at 15:59):From: Tobias Nipkow <nipkow@in.tum.de>
If it turns out to be provable, I'll be happy to replace the axiom with a lemma.
I copied it from Mike Gordon's tech report 68.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 15:59):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
I attached a short Isabelle theory containing the proof of "iff" from
the other axioms.
As I didn't want to build directly upon Pure, I simply prefixed all
constants and lemmas by "my" to name them apart from the ones of
"HOL.thy", and totally omitted several constants (like "The", "ex", ..),
since they are not needed for the argument.
Indeed, if "iff" is turned into a lemma, some parts of the theory have
to be slightly re-structured, since the introduction rules of "all" and
"disj" can be proved only after proving "iff", whereas their
elimination rules are needed in the proof ...
Best regards,
Alexander
iff_redundant.thy
Email Gateway (Aug 22 2022 at 15:59):From: Makarius <makarius@sketis.net>
Just formally, a change of the axiomatization is nothing you do without
a very deep understanding of what is there already, together with its
long history.
There is a tradition to keep axiomatics as simple as possible. For
Isabelle/HOL that means to stick close to other HOL systems, which all
go back to Gordon (1985). It does not mean to minimize the constants or
axioms, at the cost of extra complexity in explaining it to other
people, or connecting it to other papers about HOL etc.
In your experiment, you are using the classical axiom True_or_False as a
prerequisite to iff. Church might have welcomed that in 1940, but today
most logicians would consider that very strange. Classical reasoning is
something you normally bring in late, or leave it out altogether.
In my aforementioned presentation
http://sketis.net/wp-content/uploads/2016/11/Curry-Club_Dec-2016.pdf I
derive very late True_or_False from Hilbert Choice, just for the fun of
it. That development is actually in
$ISABELLE_HOME/src/Isar_Examples/Higher_Order.thy (e.g. in current
Isabelle2017-RC3).
Side remark: Isabelle theory names are always capitalized words
separated by underscore. This is important to retain sanity in the name
space qualification wrt. locales, which consist of lowercase words.
Makarius
Email Gateway (Aug 22 2022 at 16:00):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
On 09/26/2017 14:36, Makarius wrote:
Just formally, a change of the axiomatization is nothing you do without
a very deep understanding of what is there already, together with its
long history.There is a tradition to keep axiomatics as simple as possible. For
Isabelle/HOL that means to stick close to other HOL systems, which all
go back to Gordon (1985). It does not mean to minimize the constants or
axioms, at the cost of extra complexity in explaining it to other
people, or connecting it to other papers about HOL etc.
I certainly do not claim that I have a very deep understanding of the
history of HOL, but I just proved that one of the axioms of Isabelle/HOL
is redundant; this does not affect the other axioms / definitions of
basic logical connectives, and should therefore make explanation to
other people even easier -- that's at least my personal view on it.
The other changes I mentioned in my previous email only affect the order
in which lemmas are proved, not their actual contents.
In your experiment, you are using the classical axiom True_or_False as a
prerequisite to iff. Church might have welcomed that in 1940, but today
most logicians would consider that very strange. Classical reasoning is
something you normally bring in late, or leave it out altogether.
OK, I totally agree, but Isabelle/HOL is classical higher-order logic ...
Also, if classical logic should be brought in late, why is
"True_or_False" stated at the very beginning then? For instance, axiom
"eq_reflection" comes later.
So, what I'd like to emphasize is that the current set-up, with "iff"
immediately followed by "True_or_False" in the same "axiomatization"
block, looks a bit strange if one knows that one follows from the other.
Maybe one could at least put a short comment there explaining the
reasons for keeping both axioms.
In my aforementioned presentation
http://sketis.net/wp-content/uploads/2016/11/Curry-Club_Dec-2016.pdf I
derive very late True_or_False from Hilbert Choice, just for the fun of
it. That development is actually in
$ISABELLE_HOME/src/Isar_Examples/Higher_Order.thy (e.g. in current
Isabelle2017-RC3).Side remark: Isabelle theory names are always capitalized words
separated by underscore. This is important to retain sanity in the name
space qualification wrt. locales, which consist of lowercase words.
Sorry, I did not worry about the theory name in this case ... normally I do.
Best regards,
Alexander
Email Gateway (Aug 22 2022 at 16:00):From: Lawrence Paulson <lp15@cam.ac.uk>
Hi Alexander, thanks for your comments. It’s interesting to know that this axiom is redundant and that this fact has been overlooked in the past. Of course, whether we actually adopt your proof or not has no practical impact. I think it happens sometimes that axiomatic presentations contain a little redundancy for the sake of clarity.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:00):From: David Cock <david.cock@inf.ethz.ch>
Agreed. I didn't intend my reply to be dismissive - I was genuinely
curious whether the proof holds up.
David
Email Gateway (Aug 22 2022 at 16:00):From: Tobias Nipkow <nipkow@in.tum.de>
The redundany has only been overlooked by us but not by the HOL4 designers. It
is no longer in their axiomatic basis. Likewise I will remove it from ours. It
is a historic accident. I did certainly not include it for clarity.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:00):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
Same for me. My motivation to ask this question was find out whether
there was some intention for having the axiom.
Of course I'm absolutely fine if the theory stays as it is, since
ultimately it does not make much of a difference -- but then a comment
might still be reasonable.
Best regards,
Alexander
Email Gateway (Aug 22 2022 at 16:00):From: Makarius <makarius@sketis.net>
On 26/09/17 15:17, Alexander Maletzky wrote:
On 09/26/2017 14:36, Makarius wrote:
In your experiment, you are using the classical axiom True_or_False as a
prerequisite to iff. Church might have welcomed that in 1940, but today
most logicians would consider that very strange. Classical reasoning is
something you normally bring in late, or leave it out altogether.OK, I totally agree, but Isabelle/HOL is classical higher-order logic ...
I do recommend to study this material:
In my aforementioned presentation
http://sketis.net/wp-content/uploads/2016/11/Curry-Club_Dec-2016.pdf I
derive very late True_or_False from Hilbert Choice, just for the fun of
it. That development is actually in
$ISABELLE_HOME/src/Isar_Examples/Higher_Order.thy (e.g. in current
Isabelle2017-RC3).
Maybe it helps to get a better idea what Isabelle/HOL really is or could
be. I am generally more in favour of a pure type-theory view, because it
helps to communicate within the greater ITP community. At the same time,
we somehow need to keep common HOL heritage.
Also, if classical logic should be brought in late, why is
"True_or_False" stated at the very beginning then? For instance, axiom
"eq_reflection" comes later.
eq_reflection is in some sense an implementation detail of Isabelle/HOL
on top of Isabelle/Pure. It is an admissible rule, but required
explicitly for technical reasons.
Someone once figured out that using eq_reflection together with Pure
reasoning allows to shrink the axiomatic basis of HOL further. But that
messed up the explanation what happens here. This was also the incident
where I started to develop reservations against arbitrary changes to the
axiomatization.
There are so many things that could be reformed. E.g. how fundamental is
Hilbert Choice? If moved to the bottom, it would mean that the classical
axiom becomes a theorem. But that requires to undo the separation of The
and Eps that we made many years ago.
So, what I'd like to emphasize is that the current set-up, with "iff"
immediately followed by "True_or_False" in the same "axiomatization"
block, looks a bit strange if one knows that one follows from the other.
Maybe one could at least put a short comment there explaining the
reasons for keeping both axioms.
Short comments cannot tell a long story.
In the above slides, I give both an overview and important papers to
study on the subject.
Makarius
Email Gateway (Aug 22 2022 at 16:00):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
I studied the slides and also had a look at
"/src/HOL/Isar_Examples/Higher_Order_Logic.thy", but actually I never
doubted that HOL could be developed differently. All I was saying was
that in the present development one axiom could easily be replaced
by a proved lemma (which has also been confirmed by Tobias in the meantime).
Whether the approach you outline in
http://sketis.net/wp-content/uploads/2016/11/Curry-Club_Dec-2016.pdf
would be more elegant/understandable I cannot and do not want to judge.
Best regards,
Alexander
Last updated: Apr 26 2024 at 08:19 UTC