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