Email Gateway (Aug 22 2022 at 16:56): Email Gateway (Aug 22 2022 at 16:56):From: Ken Kubota <mail@kenkubota.de>
Thanks, this is what I expected.
Concerning the Axiom of Choice (answering Mario's email, too), its use should
be expressed as a conditional of the form AC => THM (or as a hypothesis) and
not as an axiom in order to make the appeal to it explicit.
An example is the theorem in exercise X5308 in [Andrews, 2002, p. 237]:
"X5308. Prove AC => [...]"
(AC is defined in [Andrews, 2002, p. 236], formal verification of X5308
available at
http://www.owlofminerva.net/files/formulae.pdf, pp. 151 ff.)
For the same reason, language elements embodying the Axiom of Choice (such as
the epsilon operator) should be avoided. For good reason Q0 uses the
description operator instead [cf. Andrews, 2002, p. 211].
Andrews sees, concerning the "Axiom Schema of Choice, an Axiom of Infinity, and
perhaps even the Continuum Hypothesis [...] room for argument whether these are
axioms of pure logic or of mathematics" [Andrews, 2002, p. 204], and I also
clearly regard all of them as non-logical axioms. Note that they are not Axioms
for Q0 [cf. Andrews, 2002, p. 213].
For the references, please see: http://doi.org/10.4444/100.111
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100
Email Gateway (Aug 22 2022 at 16:56):From: Rob Arthan <rda@lemma-one.com>
Due to its simple but elegant treatment of polymorphism, there is a very significant
difference between axioms and hypotheses in Mike Gordon’s formulation of HOL.
An axiom containing a type variable can be instantiated ad lib, but in a hypothesis,
no instantiation is allowed. So you can’t realistically say that uses of the Axiom
of Choice should be expressed as AC => THM. Having to express a theorem
with a hypothesis comprising all the type instances of AC used in its proof would
be unworkable.
Regards,
Rob.
Last updated: Apr 19 2024 at 04:17 UTC