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
