Re: [isabelle] extending well-founded partial orders to total well-founded orders
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:
That was also the first "proof" I found via google... but I did not have
a closer look, since it was "just a blog" :)
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:
Isn't that proved at the and of Zorn.thy, lemmas well_ordering and
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.
On 01/17/2013 07:55 AM, Christian Sternagel wrote:
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