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



Dear Larry,

thanks for the reply. "is trivial" sounds great. Is a formalization also trivial (or even done already)? (Note that I have to extend an existing well-founded partial order, not just obtain any total well-order ... I mention this only because I did not get the comment about the empty relation being well-founded [since I do not start from the empty relation]).

cheers

chris

On 01/17/2013 08:14 PM, Lawrence Paulson wrote:
This obviously requires the axiom of choice (after all, the empty relation is well-founded), and is trivial with it (simply well-order the set of unrelated elements).
Larry Paulson


On 17 Jan 2013, at 06:55, Christian Sternagel <c.sternagel at gmail.com> 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 ;)).

cheers

chris








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