Re: [isabelle] extending well-founded partial orders to total well-founded orders
oops :)... sorry for the sorry.
On 02/19/2013 02:43 PM, Thomas Sewell wrote:
I suspect the sorry in this proof is important.
Among other things, I can demonstrate a contradiction from your result,
as shown in the attached theory. This is intuitive - if I begin with a
partial order with an infinite descending chain, all containing orders
must also contain said chain.
On 19/02/13 15:50, Christian Sternagel wrote:
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
Now, I'll check whether this is also applicable in my setting (with
Thanks for all your hints and suggestions! (I'm still interested in
the alternative proof ;))
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.
On 18 Feb 2013, at 14:55, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
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
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)]
On 18 Feb 2013, at 06:32, Christian Sternagel
<c.sternagel at gmail.com> wrote:
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
I guess since Isabelle2013 this is now "~~/src/HOL/Cardinals/",
(hopefully) provides the necessary ingredients: Initial segments in
Wellorder_Embedding, ordinal sum in theory
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and