*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Wed, 20 Feb 2013 15:59:20 +0900*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <1361311441.66182.YahooMailClassic@web120604.mail.ne1.yahoo.com>*References*: <1361311441.66182.YahooMailClassic@web120604.mail.ne1.yahoo.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130110 Thunderbird/17.0.2

Thanks again, for all the hints and comments!

Partial_order W ==> wf (W - Id) ==> EX R0. W <= R0 & Well_order R0 & Field R0 = UNIV

On 02/20/2013 07:04 AM, Andrei Popescu wrote:

Here is something that probably works. It is essentially the breadth-first transfinite recursion cast into Zorn---the main idea is not to skip any element when climbing on W. For a relation R and a set A, define "dclosed A r" to mean that A is an R-downward-closed subset of the field of R, namely, "A <= Field r /\ (ALL a b. a : A /\ (b,a) : R --> b : A)".

Also define, for two relations R1 R2 and a set A, "incl_on A R1 R2" to mean "ALL a b : A. (a,b): R1 --> (a,b) : R2". Now, for the fixed well-founded relation W, consider the set K = {R. well_order R /\ dclosed (Field R) W /\ incl_on (Field R) W R}. Intuition: K consists of wellorders that "totalize" some initial part of W. Since Zorn applies to K (with the initial-segment relation on well-orders), we obtain a maximal element R0 of K.

So far so good. Until here everything works out.

Thanks to "incl_on", it suffices to show Field W <= Field R0. Assuming this does not hold, let a0 be an element in Field W - Field R0. Thanks to "dclosed", if we add a0 to R0 as the top element, we obtain an element of K, hence a contradiction.

Even if that worked, two things remain: - We did never employ well-foundedness of W - How to show "Field R0 = UNIV"? cheers chris

**Follow-Ups**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Andrei Popescu

**References**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] Finite_Set comp_fun_commute
- Next by Date: Re: [isabelle] Finite_Set comp_fun_commute
- 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 February 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