Re: [isabelle] extending well-founded partial orders to total well-founded orders



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


On 18 Jan 2013, at 04:15, Christian Sternagel <c.sternagel at gmail.com> wrote:

> 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 Paulson
>> 
>> 
>> On 17 Jan 2013, at 06:55, Christian Sternagel <c.sternagel at 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
>>> 
>> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.