*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Wed, 20 Feb 2013 02:50:25 -0800 (PST)*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*: <51247448.2040902@gmail.com>

Hi Christian, > Partial_order W ==> wf (W - Id) ==> > EX R0. W <= R0 & Well_order R0 & Field R0 = UNIV The partial order assumption is not needed. In what follows, I only assume W to be well-founded, thus not containing the diagonal. (Then of course the inclusion will hold for W Un Id too, since R0 is reflexive.) >>Thanks to "dclosed", if we add a0 to >> R0 as the top >> element, we obtain an element of K, hence a contradiction. > To do that (i.e., "obtain an element of K"), we would have to show "dclosed (Field R0) > W" first, which seems impossible. "dclosed (Field R0) W" holds since R0 is in K. You probably were referring to the extension of R0 with a0---let us call it R1. See below. I forgot to mention: a0 should be taken to be W-minimal in Field W - Field R0. This is where well-foundedness of W is used. Now, with this proviso, we have "dclosed (Field R1) W". As for further extending R0 to have the field UNIV, you can use the well-ordering theorem to obtain a well-order R on UNIV - Field R0, and then perform R0 + R (the ordinal sum:all elements of R0 are smaller than all those of R). Andrei --- On Wed, 2/20/13, Christian Sternagel <c.sternagel at gmail.com> wrote: From: Christian Sternagel <c.sternagel at gmail.com> Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders To: "Andrei Popescu" <uuomul at yahoo.com> Cc: "Lawrence Paulson" <lp15 at cam.ac.uk>, "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch>, cl-isabelle-users at lists.cam.ac.uk Date: Wednesday, February 20, 2013, 8:59 AM Thanks again, for all the hints and comments! Some observations (please correct me if I'm wrong). The statement we want to proof is Partial_order W ==> wf (W - Id) ==> EX R0. W <= R0 & Well_order R0 & Field R0 = UNIV Note that "wf W" as assumption would directly conflict with W being reflexive (as required by "Partial_order W"; sorry I introduced this error earlier since I'm used to work with a definition of partial order that employs irreflexivity). At some point of the proof we have to use the well-foundedness assumption (currently I don't know where), since otherwise the mentioned counterexamples apply. Andrei's suggestion seems to go in the right direction, but still, some things are not clear to me. See below 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)". If we require (A <= Field r) in the definition of "dclosed", we will have "Field R0 <= Field W" later in the proof. After showing "Field W <= Field R0", we would obtain "Field W = Field R0" and thus not "Field R0 = UNIV" in general. > 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. To do that (i.e., "obtain an element of K"), we would have to show "dclosed (Field R0) W" first, which seems impossible. 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:*Christian Sternagel

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

- Previous by Date: [isabelle] 2 postdoc positions at IRIT Toulouse and INRIA Nancy
- 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