Re: [isabelle] extending well-founded partial orders to total well-founded orders

Dear Andreas,

thanks for the pointer? I will have a look (however, well-foundedness is essential for me).

On 01/17/2013 04:39 PM, Andreas Lochbihler wrote:
Dear Christian,

I haven't seen a formalisation of that proof, but I have formalised a
proof that every partial order can be extended to a total order (in the
appendix, works with Isabelle2012). A preliminary version thereof is
part of JinjaThreads in the AFP (theory MM/Orders), but I have already
removed that from the development version, because I no longer need it.
As you can see there, it is not necessary to modify Zorn.thy from
Isabelle's library, because you can encode the carrier set in the relation.

For the case of well-foundedness, I found the following informal proof
in a blog, though I haven't checked whether it is correct:
That was also the first "proof" I found via google... but I did not have a closer look, since it was "just a blog" :)

It uses the existence of a well-ordering on any set. I don't know
whether that has been proven in Isabelle before. Andrei might have done
so in his Cardinals development; he might tell you more.
Isn't that proved at the and of Zorn.thy, lemmas well_ordering and well_oder_on?




On 01/17/2013 07:55 AM, Christian Sternagel wrote:
Dear all,

is anybody aware of an Isabelle formalization of the (apparently
well-known) fact that every well-founded partial order can be extended
to a total well-founded order (in particular a well-partial-order)?

If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).



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