Re: [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
> On 12 Mar 2018, at 19:12, Ken Kubota <mail at kenkubota.de> wrote:
> 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 => […]"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and