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

```I had a look at theorem well_ordering from Zorn, and it is not clear how to adapt its proof to this case. The set of wellorders disjoint from W^-1, with the initial-segment relation, does satisfy the hypothesis of Zorn, yielding a maximal element R.  But then it is not apparent whether W <= R.  Or maybe use a stronger notion of consistency with W?

I confess I did not try too hard though, being happily married with my proof which traverses W breadth-first.

Regards,
Andrei

--- On Mon, 2/18/13, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

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

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?
>>>
>>> thanks in advance,
>>>
>>> chris
>>>
>>>
>>>
>>
>>

```

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