Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Another limitation of HOL: Binding the type va...


view this post on Zulip 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: Mar 28 2024 at 16:17 UTC