> On 12 Mar 2018, at 19:12, Ken Kubota <m...@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. ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
