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

Hi Christian,

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.  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.

Andrei

--- On Tue, 2/19/13, Andrei Popescu <uuomul at yahoo.com> wrote:

From: Andrei Popescu <uuomul at yahoo.com>
Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders
To: "Lawrence Paulson" <lp15 at cam.ac.uk>, "Christian Sternagel" <c.sternagel at gmail.com>
Cc: "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch>, cl-isabelle-users at lists.cam.ac.uk
Date: Tuesday, February 19, 2013, 10:29 AM

The statement is definitely not true for any partial order, unless that partial order is well-founded---take the integer order for instance.  Luckily, there is a sorry in your proof, otherwise HOL would have been shown inconsistent. :)

Also, this approach of taking the set of all wellorders that contain W and applying Zorn is not working, since the hypotheses of Zorn a fortiori require that this set is already nonempty, which is what you started out to prove.

Andrei

--- On Tue, 2/19/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:
"Lawrence Paulson" <lp15 at cam.ac.uk>
Cc: "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch>, "Andrei Popescu" <uuomul at yahoo.com>, cl-isabelle-users at lists.cam.ac.uk
Date: Tuesday, February 19, 2013, 6:50 AM

After giving up on the alternative recipe for the moment, I went back to
Larry's suggestion. And indeed, the existing proof could be modified in
a straight-forward way (see the attached theory).

(Note that well-foundedness of the given partial order is irrelevant. So
the actual lemma is: every partial order can be extended to a total
well-order.)

Now, I'll check whether this is also applicable in my setting (with
explicit domains).

Thanks for all your hints and suggestions! (I'm still interested in the
alternative proof ;))

cheers

chris

On 02/19/2013 12:22 AM, Lawrence Paulson wrote:
> I see, it is a little more subtle than I
thought, but I would guess that the proof of the well-ordering theorem itself can be modified to exhibit a well-ordering that is consistent with a given well-founded relation. As I recall, the well-ordering theorem is proved by Zorn's lemma and considers the set of all well orderings of subsets of a given set; one would need to modify the argument to restrict attention to well orderings that were consistent with W.
>
> Surely this theorem has a name and a proof can be found somewhere.
>
> Larry
>
> On 18 Feb 2013, at 14:55, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>
>> Hi Larry,
>>
>> As far as I understand your suggestion, it does not even yield a ordering. For example, suppose that there are three elements a, b, c such that the well ordering <R
obtained by the well-ordering theorems orders them as a <R b <R c. Now, consider the well-founded relation <W which orders c <W a and nothing else. Then, c <TO a as c<W a, and a <TO b and b <TO c as neither a <W b, b <W a, b <W c, nor c <W b. Hence,
>>
>> c <TO a <TO b <TO c
>>
>> which violates the ordering properties. Or am I misunderstanding something?
>>
>> Andreas
>>
>> On 02/18/2013 03:18 PM, Lawrence Paulson wrote:
>>> I still don't see what's wrong with the following approach:
>>>
>>> 1. Prove the well ordering theorem (maybe it has been proved already).
>>>
>>> 2. Obtain the desired total ordering as a lexicographic combination of the partial order with the total well ordering of your type
>>>
>>> [More specifically: given W a well founded
relation and R a well ordering obtained by the well ordering theorem, define TO x y == W x y | (~ W x y & ~W y x & R x y)]
>>>
>>> Larry Paulson
>>>
>>>
>>> On 18 Feb 2013, at 06:32, Christian Sternagel <c.sternagel at gmail.com> wrote:
>>>
>>>> Dear Andrei,
>>>>
>>>> finally deadlines are over for the time being and I found your email again ;)
>>>>
>>>> On 01/19/2013 12:22 AM, Andrei Popescu wrote:
>>>>> My AFP formalization ordinals
>>>>>
>>>>> http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml
>>>>
>>>> I guess since
Isabelle2013 this is now "~~/src/HOL/Cardinals/", right?
>>>>
>>>>> (hopefully) provides the necessary ingredients: Initial segments in
>>>>> Wellorder_Embedding, ordinal sum in theory Constructions_on_Wellorders,
>>>>> and a transfinite recursion combinator (a small adaptation of the
>>>>> wellfounded combinator) in theory Wellorder_Relation.
>>>>
>>>> Could you elaborate on the mentioned finite recursion combinator and how it is used?
>>>>
>>>>
>>>> chris
>>>>
>>>>
>>>>
>>>
>>>
>

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