Email Gateway (Aug 22 2022 at 18:28): Email Gateway (Aug 22 2022 at 18:28):From: Askar Safin via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
"refl" from HOL.HOL can be proved from other axioms declared near it, i. e. from the_eq_trivial and subst. Look:
lemma refl: "t = t"
proof -
have "(THE x. x = t) = t" by (rule the_eq_trivial)
from this and this show "t = t" by (rule subst)
qed
==
Askar Safin
http://vk.com/safinaskar
Email Gateway (Aug 22 2022 at 18:29):From: Makarius <makarius@sketis.net>
What can we learn from that?
The usual way to characterize equality is via refl and subst,
independently of later add-ons to the logic.
The axiomatization of Isabelle/HOL is somewhat historic and accidental,
following a report by Mike Gordon from 1986, which in turn followed the
paper by Alonzo Church from 1940.
In this distance past logicians where still following a bad habit to
make the textual representation of the foundations as small as possible,
without taking care about clarity. Who in his right mind would base the
EX quantifier on Hilbert's Choice operator, for example? There are other
historical oddities and tidbits to be (re)discovered.
Here is also my own version of Higher-Order Logic for illustrative
purposes: $ISABELLE_HOME/src/HOL/Isar_Examples/Higher_Order_Logic.thy --
it introduces Hilbert's "Eps" late in the theory, but omits the definite
description operator "The".
Many more variations on the theme are possible, but they have no
practical relevance of using the HOL logic in applications: definitional
packages and proof tools are much more important than axiomatizations.
That is the main lesson learned after decades of trying to make logics
work in Interactive Theorem Proving.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC