*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 18 Jan 2013 12:15:45 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <50F8CC55.5010409@gmail.com>*References*: <50F7A068.6070309@gmail.com> <6E9C8989-CC0A-42CD-B8D1-FBC836BB4F93@cam.ac.uk> <50F8CC55.5010409@gmail.com>

I don't recall whether a proof of the well-ordering theorem is already available or not. Even that theorem isn't difficult to prove. Once you've got it, just apply it to the set of all elements not related by your partial order. Then combine the two orderings lexicographically, Larry Paulson On 18 Jan 2013, at 04:15, Christian Sternagel <c.sternagel at gmail.com> wrote: > 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 >>> >> >

**References**:**[isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Lawrence Paulson

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Next by Date: Re: [isabelle] Two questions of a beginner
- Previous by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Next by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list