We got into a discussion about this mathematical conundrum at our reading group, and Dave Cock and myself are convinced that it is possible to construct an example relation by following the well-founded recursion along the original ordering. I attach a theory file that shows the construction. The important result, that the bizarre order constructed embeds the original well-founded r, is proven, modulo some missing results I claim are well-known. There's a bunch of trivia to be done as well to show that the lex-product variant I used preserves all the expected rules. All that given, Andrei's approach seems a lot cleaner. Yours, Thomas. ________________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Andrei Popescu [uuomul at yahoo.com] Sent: Tuesday, February 19, 2013 7:29 PM To: Lawrence Paulson; Christian Sternagel Cc: cl-isabelle-users at lists.cam.ac.uk; Andreas Lochbihler Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders 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? >>>> >>>> thanks in advance, >>>> >>>> chris >>>> >>>> >>>> >>> >>> > ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.