Email Gateway (Jan 18 2023 at 21:50): Email Gateway (Jan 18 2023 at 21:50):From: Ken Kubota <mail@kenkubota.de>
Dear Rob,
Thank you for supporting my position here ("However, I agree that there are many useful properties that are best specified using more general quantification over types.").
Let me remind you that you pointed out some time ago the fact that the implicit universal quantification over the free type variables in HOL make certain expressions unworkable, namely that the appeal to the axiom of choice can't be made explicit in the form AC => THM because of the free type variable in the hypothesis: https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2018-03/msg00043.html
With quantification over types this is possible (since the type variable isn't free anymore): https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2018-03/msg00051.html
The proof is still available online: https://www.kenkubota.de/files/ac_instantiation.r0.out.pdf
Note that the Quantified Axiom of Choice (without a free type variable)
∀τ[λt.AC]o
(wff 1388 = QAC)
is to be read as
∀ t . AC
where "t" is the type variable in question here.
Regards,
Ken
Ken Kubota
https://doi.org/10.4444/100
Full thread: https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2023-01/msg00039.html
Last updated: Jan 04 2025 at 20:18 UTC