Email Gateway (Aug 19 2022 at 09:55): Email Gateway (Aug 19 2022 at 09:55):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
is anybody aware of an Isabelle formalization of the (apparently
well-known) fact that every well-founded partial order can be extended
to a total well-founded order (in particular a well-partial-order)?
If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
cheers
chris
Email Gateway (Aug 19 2022 at 09:56):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Christian,
I haven't seen a formalisation of that proof, but I have formalised a
proof that every partial order can be extended to a total order (in the
appendix, works with Isabelle2012). A preliminary version thereof is
part of JinjaThreads in the AFP (theory MM/Orders), but I have already
removed that from the development version, because I no longer need it.
As you can see there, it is not necessary to modify Zorn.thy from
Isabelle's library, because you can encode the carrier set in the relation.
For the case of well-foundedness, I found the following informal proof
in a blog, though I haven't checked whether it is correct:
http://tylerneylon.com/blog/2007/06/every-well-founded-partial-order-can-be.html
It uses the existence of a well-ordering on any set. I don't know
whether that has been proven in Isabelle before. Andrei might have done
so in his Cardinals development; he might tell you more.
Andreas
Extend_Partial_Order.thy
Email Gateway (Aug 19 2022 at 09:57):From: Lawrence Paulson <lp15@cam.ac.uk>
This obviously requires the axiom of choice (after all, the empty relation is well-founded), and is trivial with it (simply well-order the set of unrelated elements).
Larry Paulson
Email Gateway (Aug 19 2022 at 09:57):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Andreas,
thanks for the pointer? I will have a look (however, well-foundedness is
essential for me).
On 01/17/2013 04:39 PM, Andreas Lochbihler wrote:
Dear Christian,
I haven't seen a formalisation of that proof, but I have formalised a
proof that every partial order can be extended to a total order (in the
appendix, works with Isabelle2012). A preliminary version thereof is
part of JinjaThreads in the AFP (theory MM/Orders), but I have already
removed that from the development version, because I no longer need it.
As you can see there, it is not necessary to modify Zorn.thy from
Isabelle's library, because you can encode the carrier set in the relation.For the case of well-foundedness, I found the following informal proof
in a blog, though I haven't checked whether it is correct:
http://tylerneylon.com/blog/2007/06/every-well-founded-partial-order-can-be.html
That was also the first "proof" I found via google... but I did not have
a closer look, since it was "just a blog" :)It uses the existence of a well-ordering on any set. I don't know
whether that has been proven in Isabelle before. Andrei might have done
so in his Cardinals development; he might tell you more.
Isn't that proved at the and of Zorn.thy, lemmas well_ordering and
well_oder_on?
cheers
chris
Andreas
On 01/17/2013 07:55 AM, Christian Sternagel wrote:
Dear all,
is anybody aware of an Isabelle formalization of the (apparently
well-known) fact that every well-founded partial order can be extended
to a total well-founded order (in particular a well-partial-order)?If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
cheers
chris
Email Gateway (Aug 19 2022 at 09:57):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Larry,
thanks for the reply. "is trivial" sounds great. Is a formalization also
trivial (or even done already)? (Note that I have to extend an existing
well-founded partial order, not just obtain any total well-order ... I
mention this only because I did not get the comment about the empty
relation being well-founded [since I do not start from the empty relation]).
cheers
chris
Email Gateway (Aug 19 2022 at 09:58):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Christian,
Yes, you're right, this is exactly the last lemma in Zorn. I must have
missed it when I last looked at that theory.
Andreas
Email Gateway (Aug 19 2022 at 09:58):From: Lawrence Paulson <lp15@cam.ac.uk>
I don't recall whether a proof of the well-ordering theorem is already available or not. Even that theorem isn't difficult to prove. Once you've got it, just apply it to the set of all elements not related by your partial order. Then combine the two orderings lexicographically,
Larry Paulson
Email Gateway (Aug 19 2022 at 09:59):From: Andrei Popescu <uuomul@yahoo.com>
Dear Christian, Andreas and Larry,
I do not think the proof is trivial, since, as far as I see, Larry's proof idea would need to be applied in several steps in order to avoid conflicts.
Andreas's proof does not seem easily adaptable here, since wellfoundedness is not closed under unions of arbitrary chains. The proof from the link Adreas pointed to sounds like a correct implementation of Larry's idea.
Here is my construction, which is a variation of the one from the blog. (I shall only use the fact that the original relation R is wellfounded.)
Imagine R as a forest, having the minimal elements as roots of the trees and having the branches of the trees possibly crossing each other. We traverse this forest in a breadth-first way by transfinite induction and wellorder it "on levels" by performing the following steps on a state consisting of a wellorder W.
1) Start with W = {}
2) In the successor case: Get the set M of minimal elements of R that are not in (the field of) W, and let V be a well-order on M. Take W' to be the concatenation (ordinal sum) of W and V.
3) In the limit case: Take the union: the result is a wellorder, since the chain involved in the union has the property that each element is not only a subset, but also an initial segment of any later one.
The final W has exhausted the whole R, hence it is the desired wellorder.
My AFP formalization ordinals
http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml
(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.
Best regards,
Andrei
--- On Fri, 1/18/13, cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> wrote:
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk>
Subject: Cl-isabelle-users Digest, Vol 91, Issue 14
To: cl-isabelle-users@lists.cam.ac.uk
Date: Friday, January 18, 2013, 8:13 AM
Send Cl-isabelle-users mailing list submissions to
cl-isabelle-users@lists.cam.ac.uk
To subscribe or unsubscribe via the World Wide Web, visit
https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
cl-isabelle-users-request@lists.cam.ac.uk
You can reach the person managing the list at
cl-isabelle-users-owner@lists.cam.ac.uk
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Cl-isabelle-users digest..."
Today's Topics:
1. Re: Trying to use "datatype" to restrict types of formulas
used, getting error (Gottfried Barrow)
2. Re: extending well-founded partial orders to total
well-founded orders (Christian Sternagel)
3. Re: extending well-founded partial orders to total
well-founded orders (Christian Sternagel)
4. Re: Trying to use "datatype" to restrict types of formulas
used, getting error (Gottfried Barrow)
5. Re: Trying to use "datatype" to restrict types of formulas
used, getting error (John Wickerson)
6. TAP 2013: Final Call for Papers (Achim D. Brucker)
7. Re: Trying to use "datatype" to restrict types of formulas
used, getting error (Gottfried Barrow)
Message: 1
Date: Thu, 17 Jan 2013 14:25:04 -0600
From: Gottfried Barrow <gottfried.barrow@gmx.com>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
formulas used, getting error
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <50F85E20.2060301@gmx.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
On 1/17/2013 2:12 PM, Gottfried Barrow wrote:
function sFOLf :: "sFOLdt => bool" where
Please change "function" to "fun".
It still works out the same. Without the "Forall" lines in my "datatype"
and "fun", my sFOLf function terminates correctly with the message
"Found termination order: "{}"".
Thanks,
GB
Message: 2
Date: Fri, 18 Jan 2013 13:12:01 +0900
From: Christian Sternagel <c.sternagel@gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total
well-founded orders
To: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Cc: isabelle-users <isabelle-users@cl.cam.ac.uk>
Message-ID: <50F8CB91.5080003@gmail.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Dear Andreas,
thanks for the pointer? I will have a look (however, well-foundedness is
essential for me).
On 01/17/2013 04:39 PM, Andreas Lochbihler wrote:
Dear Christian,
I haven't seen a formalisation of that proof, but I have formalised a
proof that every partial order can be extended to a total order (in the
appendix, works with Isabelle2012). A preliminary version thereof is
part of JinjaThreads in the AFP (theory MM/Orders), but I have already
removed that from the development version, because I no longer need it.
As you can see there, it is not necessary to modify Zorn.thy from
Isabelle's library, because you can encode the carrier set in the relation.For the case of well-foundedness, I found the following informal proof
in a blog, though I haven't checked whether it is correct:
http://tylerneylon.com/blog/2007/06/every-well-founded-partial-order-can-be.html
That was also the first "proof" I found via google... but I did not have
a closer look, since it was "just a blog" :)It uses the existence of a well-ordering on any set. I don't know
whether that has been proven in Isabelle before. Andrei might have done
so in his Cardinals development; he might tell you more.
Isn't that proved at the and of Zorn.thy, lemmas well_ordering and
well_oder_on?
cheers
chris
Andreas
On 01/17/2013 07:55 AM, Christian Sternagel wrote:
Dear all,
is anybody aware of an Isabelle formalization of the (apparently
well-known) fact that every well-founded partial order can be extended
to a total well-founded order (in particular a well-partial-order)?If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
cheers
chris
Message: 3
Date: Fri, 18 Jan 2013 13:15:17 +0900
From: Christian Sternagel <c.sternagel@gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total
well-founded orders
To: Lawrence Paulson <lp15@cam.ac.uk>
Cc: isabelle-users <isabelle-users@cl.cam.ac.uk>
Message-ID: <50F8CC55.5010409@gmail.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Dear Larry,
thanks for the reply. "is trivial" sounds great. Is a formalization also
trivial (or even done already)? (Note that I have to extend an existing
well-founded partial order, not just obtain any total well-order ... I
mention this only because I did not get the comment about the empty
relation being well-founded [since I do not start from the empty relation]).
cheers
chris
On 01/17/2013 08:14 PM, Lawrence Paulson wrote:
This obviously requires the axiom of choice (after all, the empty relation is well-founded), and is trivial with it (simply well-order the set of unrelated elements).
Larry PaulsonOn 17 Jan 2013, at 06:55, Christian Sternagel <c.sternagel@gmail.com> wrote:
Dear all,
is anybody aware of an Isabelle formalization of the (apparently well-known) fact that every well-founded partial order can be extended to a total well-founded order (in particular a well-partial-order)?
If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
cheers
chris
Message: 4
Date: Thu, 17 Jan 2013 22:35:26 -0600
From: Gottfried Barrow <gottfried.barrow@gmx.com>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
formulas used, getting error
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <50F8D10E.9000502@gmx.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
People can ignore what I was talking about, unless someone wants to give
me a complete "datatype" and "fun/primrec" solution based on the
informal, recursive definition I gave. Or a solution of another form
would be okay.
Trying to figure out how recursion works, I have this experimental code:
typedecl sT
consts inS :: "sT => sT => bool" (infixl "inS" 55)
datatype sFOLdt =
In sT sT
|And bool bool
|Rec bool
primrec sFOLf :: "sFOLdt => bool" where
"sFOLf (In u1 u2) = (u1 inS u2)" |
"sFOLf (And f1 f2) = ((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" |
"sFOLf (Rec f) = True"
which gives the error: Extra variables on rhs: "(sFOLf::(sFOLdt => bool))"
All that to say, trial and error has shown me I haven't understood
certain basic things, but trial and error can be an excellent learning
aid sometimes.
Regards,
GB
Message: 5
Date: Fri, 18 Jan 2013 06:35:10 +0100
From: John Wickerson <jpw48@cam.ac.uk>
Subject: Re: [isabelle] Trying to use "datatype" to restrict types of
formulas used, getting error
To: Gottfried Barrow <gottfried.barrow@gmx.com>
Cc: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <B5EE0B87-2B81-423A-B541-B206AF2AA37E@cam.ac.uk>
Content-Type: text/plain; charset=us-ascii
Hi Gottfried,
The problem is here...
function sFOLf :: "sFOLdt => bool" where
...
"sFOLf (Forall u f) = (!u. f)"
On the left you have free variables u and f, both of the same status. On the right, u is a binder, and any appearances of u inside f are bound to that binder.
I think things might be improved if you change your datatype from
datatype sFOLdt =
...
|Forall sT bool
to something like
datatype sFOLdt =
...
|Forall "sT => bool"
Then you could write something like
function sFOLf :: "sFOLdt => bool" where
.
[message truncated]
Email Gateway (Aug 19 2022 at 10:13):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 10:13):From: Lawrence Paulson <lp15@cam.ac.uk>
I still don't see what's wrong with the following approach:
Prove the well ordering theorem (maybe it has been proved already).
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
Email Gateway (Aug 19 2022 at 10:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 10:13):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 10:14):From: Andrei Popescu <uuomul@yahoo.com>
Hi Larry,
To prevent Andreas's counterexample, there is no way but to choose the well-ordering in a manner that respects W, namely, as follows: The minimal elements of W, say, forming the set M0, should come first. Then should come the minimal elements of what is left in W after removing M0, say, M1, and so on. My transfinite construction does just that: it well-orders each M_i and puts the M_i's together as M0 < M1 < M2 < ...
Andrei
Email Gateway (Aug 19 2022 at 10:14):From: Andrei Popescu <uuomul@yahoo.com>
Hi Christian,
I guess since Isabelle2013 this is now "~~/src/HOL/Cardinals/", right?
Right.
Could you elaborate on the mentioned finite recursion combinator and how it is used?
The worec combinator,
worec :: "(('a => 'b) => 'a => 'b) => 'a => 'b"
(defined in the context of a fixed wellorder r on 'a)
is just a slightly more convenient version of wfrec.
It is used to define a function f :: 'a => 'b by specifying,
for each x :: 'a, the value of f on x in terms of the values of f
on all elements less than x w.r.t. r, i.e., in my notation, all
elements of underS x. This would ideally employ an operator
of type
Prod x : 'a. (underS x => 'b) => 'b
In HOL, the same is achieved by an
"admissible" operator of a less informative type.
The only relevant facts are below:
definition
adm_wo :: "(('a => 'b) => 'a => 'b) => bool"
where
"adm_wo H ≡ ∀f g x. (∀y ∈ underS x. f y = g y) --> H f x = H g x"
lemma worec_fixpoint:
assumes "adm_wo H"
shows "worec H = H (worec H)"
Cheers,
Andrei
--- On Mon, 2/18/13, Christian Sternagel <c.sternagel@gmail.com> wrote:
From: Christian Sternagel <c.sternagel@gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders
To: "Andrei Popescu" <uuomul@yahoo.com>
Cc: cl-isabelle-users@lists.cam.ac.uk
Date: Monday, February 18, 2013, 8:32 AM
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
Email Gateway (Aug 19 2022 at 10:14):From: Andrei Popescu <uuomul@yahoo.com>
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
Email Gateway (Aug 19 2022 at 10:14):From: Christian Sternagel <c.sternagel@gmail.com>
Thanks Andrei,
concerning your proof sketch, I have some problems applying your recipe
(or the one from the blog post, for that matter) in a concrete proof.
Lets first review my setting (please let me know if any of this is
"strange" in any way). I use the following definitions (mostly from
AFP/Well_Quasi_Orders):
definition irreflp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"irreflp_on P A = (∀a∈A. ¬ P a a)"
definition transp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"transp_on P A = (∀x∈A. ∀y∈A. ∀z∈A. P x y ∧ P y z ⟶ P x z)"
definition po_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"po_on P A = (irreflp_on P A ∧ transp_on P A)"
definition total_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"total_on P A = (∀x∈A. ∀y∈A. x = y ∨ P x y ∨ P y x)"
definition wfp_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"wfp_on P A = (¬ (∃f. ∀i. f i ∈ A ∧ P (f (Suc i)) (f i)))"
definition wellorder_on where
"wellorder_on P A = (po_on P A ∧ wfp_on P A ∧ total_on P A)"
definition ext_on where "ext_on P Q A = (∀x∈A. ∀y∈A. Q x y ⟶ P x y)"
For "wfp_on" I derived the following induction schema:
wfp_on_induct:
wfp_on ?P ?A ⟹
?x ∈ ?A ⟹
(⋀y. y ∈ ?A ⟹ (⋀x. x ∈ ?A ⟹ ?P x y ⟹ ?Q x) ⟹ ?Q y) ⟹
?Q ?x
Moreover from Zorn.thy I derived the following variant of the well-order
theorem:
wellorder_on: "∃W. wellorder_on W A"
Let P be the given well-founded partial order on A. Then, we obtain a
well-order W on A by the well-order theorem. Using wfp_on_induct, I can
start a proof
{ fix x
assume "x ∈ A"
with wfp_on W A
have "wellorder_on N {y∈A. W^== x} ∧ ext_on N P {y∈A. W^== y x}"
proof (induct rule: wfp_on_induct)
for some appropriate definition of N (using worec (?)). Is that the
transfinite induction you were referring to?
Even if I would succeed with this proof, I don't see how I could derive
"wellorder_on N A & ext_on N P A" from it.
What am I doing wrong?
cheers
chris
Email Gateway (Aug 19 2022 at 10:14):From: Christian Sternagel <c.sternagel@gmail.com>
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
Well_Order_Extension.thy
Email Gateway (Aug 19 2022 at 10:14):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.
Yours,
Thomas.
False.thy
Email Gateway (Aug 19 2022 at 10:14):From: Christian Sternagel <c.sternagel@gmail.com>
oops :)... sorry for the sorry.
Email Gateway (Aug 19 2022 at 10:14):From: Andrei Popescu <uuomul@yahoo.com>
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
Email Gateway (Aug 19 2022 at 10:15):From: Andrei Popescu <uuomul@yahoo.com>
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@yahoo.com> wrote:
From: Andrei Popescu <uuomul@yahoo.com>
Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders
To: "Lawrence Paulson" <lp15@cam.ac.uk>, "Christian Sternagel" <c.sternagel@gmail.com>
Cc: "Andreas Lochbihler" <andreas.lochbihler@inf.ethz.ch>, cl-isabelle-users@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@gmail.com> wrote:
From: Christian Sternagel <c.sternagel@gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders
To:
"Lawrence Paulson" <lp15@cam.ac.uk>
Cc: "Andreas Lochbihler" <andreas.lochbihler@inf.ethz.ch>, "Andrei Popescu" <uuomul@yahoo.com>, cl-isabelle-users@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@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:
Prove the well ordering theorem (maybe it has been proved already).
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@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
Email Gateway (Aug 19 2022 at 10:15):From: Andrei Popescu <uuomul@yahoo.com>
Hi Christian,
No, this is not what I had in mind. Transfinite recursion does not need Zorn. But I refrain from any further explanations, since hopefully the other route works out for you.
Andrei
Email Gateway (Aug 19 2022 at 10:15):From: Lawrence Paulson <lp15@cam.ac.uk>
I played with a slightly different approach, and completed your "sorry", but there are two more further down :-(
But who knows, perhaps you can use this.
Larry Paulson
Well_Order_Extension.thy
Email Gateway (Aug 19 2022 at 10:16):From: Christian Sternagel <c.sternagel@gmail.com>
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:
cheers
chris
Email Gateway (Aug 19 2022 at 10:16):From: Andrei Popescu <uuomul@yahoo.com>
Hi Christian,
Partial_order W ==> wf (W - Id) ==>
EX R0. W <= R0 & Well_order R0 & Field R0 = UNIV
The partial order assumption is not needed. In what follows, I only assume W to be well-founded, thus not containing the diagonal. (Then of course the inclusion will hold for
W Un Id too, since R0 is reflexive.)
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.
"dclosed (Field R0) W" holds since R0 is in K. You probably were referring to the extension of R0 with a0---let us call it R1. See below.
I forgot to mention: a0 should be taken to be W-minimal in Field W - Field R0. This is where well-foundedness of W is used.
Now, with this proviso, we have "dclosed (Field R1) W".
As for further extending R0 to have the field UNIV, you can use the well-ordering theorem to obtain a well-order R on UNIV - Field R0, and then perform R0 + R (the ordinal sum:all elements of R0 are smaller than all those of R).
Andrei
--- On Wed, 2/20/13, Christian Sternagel <c.sternagel@gmail.com> wrote:
From: Christian Sternagel <c.sternagel@gmail.com>
Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders
To: "Andrei Popescu" <uuomul@yahoo.com>
Cc: "Lawrence Paulson" <lp15@cam.ac.uk>, "Andreas Lochbihler" <andreas.lochbihler@inf.ethz.ch>, cl-isabelle-users@lists.cam.ac.uk
Date: Wednesday, February 20, 2013, 8:59 AM
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:
cheers
chris
Email Gateway (Aug 19 2022 at 10:17):From: Christian Sternagel <c.sternagel@gmail.com>
Hi Andrei,
now it was verbose enough for me ;)
On 02/20/2013 07:50 PM, Andrei Popescu wrote:
"dclosed (Field R0) W" holds since R0 is in K. You probably were
referring to the extension of R0 with a0---let us call it R1. See below.
yes, sorry for that.
I forgot to mention: a0 should be taken to be W-minimal in Field W -
Field R0. This is where well-foundedness of W is used.
Now, with this proviso, we have "dclosed (Field R1) W".
That was the crucial point, thanks!
As for further extending R0 to have the field UNIV, you can use the
well-ordering theorem to obtain a well-order R on UNIV - Field R0, and
then perform R0 + R (the ordinal sum:all elements of R0 are smaller than
all those of R).
Also this easily worked out (thanks to your Cardinals library).
Thus we have:
Every well-founded relation can be extended to a well-order.
And as corollary, every well-founded relation can be extended to a total
well-order.
Find the (not yet polished) proofs attached (I gather that calls to the
smt method are nothing we want in finished proofs, right?).
cheers
chris
Well_Order_Extension.thy
Email Gateway (Aug 19 2022 at 10:18):From: Andrei Popescu <uuomul@yahoo.com>
Hi Christian,
Find the (not yet polished) proofs attached
Nice!
(I gather that calls to
the smt method are nothing we want in finished proofs, right?).
This matters only if you want to contribute the theorem as part of the distribution. IMO, it is a useful theorem and it should be included.
Andrei
Email Gateway (Aug 19 2022 at 10:19):From: Christian Sternagel <c.sternagel@gmail.com>
Hi Andrei,
Just to be clear: That's what I intended with my separate mail on
isabelle-dev (containing a polished theory file).
http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/3865/match=
My rational being that inclusion into the distribution is for developers
rather than users ;)
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC