*To*: Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic*From*: Rob Arthan <rda at lemma-one.com>*Date*: Mon, 12 Mar 2018 20:20:25 +0000*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, HOL-info list <hol-info at lists.sourceforge.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <12653651-0951-4152-9D84-83060FAF2576@kenkubota.de>*References*: <03F02375-13E2-4E53-83E3-435F94EE5A5A@kenkubota.de> <B603330D-8B7B-4E2C-83AD-4952419953CE@cam.ac.uk> <12653651-0951-4152-9D84-83060FAF2576@kenkubota.de>

> 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 be unworkable. Regards, Rob.

**Follow-Ups**:

**References**:**[isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic***From:*Ken Kubota

**Re: [isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic***From:*Lawrence Paulson

**[isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic***From:*Ken Kubota

- Previous by Date: [isabelle] Mathematical Logics and Logical Frameworks
- Next by Date: [isabelle] New in the AFP: Weight-Balanced Trees by Tobias Nipkow and Stefan Dirix
- Previous by Thread: [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Next by Thread: [isabelle] Binding the type variable in the Axiom of Choice – Re: Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list