On 21 Jan 2010, at 18:07, Roger Bishop Jones wrote:
> On Wednesday 20 January 2010 16:02:10 Roger Bishop Jones wrote:
>
>> On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote:
>>> The only relevant information I have come across is Stewart Shapiro's
>>> statement, in Foundations without Fo
On Wednesday 20 January 2010 16:02:10 Roger Bishop Jones wrote:
> On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote:
> > The only relevant information I have come across is Stewart Shapiro's
> > statement, in Foundations without Foundationalism, that in set theory
> > done with second-orde
I once did a proof of the well-ordering principle and several
other Axiom of Choice equivalents (Zorn's Lemma etc.) in HOL88:
http://www.cl.cam.ac.uk/~jrh13/papers/wellorder-library.html
This proof certainly survives in HOL Light (Examples/wo.ml),
and possibly in other versions of HOL too.
F
Further to my last message on this topic, I did discover the place in Shapiro
where he talks about this (5.1.3 p107).
On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote:
> The only relevant information I have come across is Stewart Shapiro's
> statement, in Foundations without Foundation
On Tuesday 19 January 2010 18:7:32 Lockwood Morris wrote:
> Does anyone know if it is possible to prove the well-ordering theorem in
> HOL for an arbitrary type? That is, using the terminology of
> relationTheory,
>
> ?R:'a->'a->bool. WF R /\ StrongLinearOrder R .
There is a proof in Proof
Does anyone know if it is possible to prove the well-ordering theorem in
HOL for an arbitrary type? That is, using the terminology of
relationTheory,
?R:'a->'a->bool. WF R /\ StrongLinearOrder R .
Or just the StrongLinearOrder part would suit me too. My motivation is
somewhat practical: I
