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> 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
be unworkable.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.