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



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





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