Re: [isabelle] extending well-founded partial orders to total well-founded orders
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]).
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).
On 17 Jan 2013, at 06:55, Christian Sternagel <c.sternagel at gmail.com> 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