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

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"?



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