[FOM] Extension of well-founded relation well-ordering (Gert Smolka)

[Andrei Popescu]

Hi Gert, 

Yes, this is an easy consequence of Zorn, but I don't know of any literature reference on it. We had a recent discussion about this on the Isabelle mailing list: please see the thread "extending well-founded partial orders to total well-founded orders" on the page https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-February/thread.html

There is now an Isabelle formalization by Christian Sternagel:

https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL-Cardinals/Wellorder_Extension.html  
This is HOL (hence uses Hilbert choice), but the proof can be easily adapted to your setting.  

All the best,   Andrei 



-------------------------------------------------

Message: 2
Date: Tue, 10 Feb 2015 07:56:26 +0100
From: Gert Smolka <smolka at ps.uni-saarland.de>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: [FOM] Extension of well-founded relation well-ordering
Message-ID: <E5ED93D1-39B7-4BCD-93C5-3640B9B9646F at ps.uni-saarland.de>
Content-Type: text/plain; charset=us-ascii

Consider the following statement:

Let X be a set with a choice function.  Then every well-founded relation on X can be extended to a well-ordering of X.

Is there a proof of the statement in the literature?

I would expect that a proof of Zermelo's theorem can be extended to a proof of the statement.

Gert Smolka

------------------------------

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


End of FOM Digest, Vol 146, Issue 8
***********************************
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150210/ccf4fca2/attachment.html>