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

cheers

chris

```

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