Re: [isabelle] Infinity - infinity = infinity



But this property is still too weak for your purposes. The properties you state in your original message (as necessary for the decision procedure) are first-order and will hold for the non-standard naturals.

Of course I understand that they don't suit all purposes, because they don't give a unique "infinity".

--lcp

> On 2 Dec 2016, at 16:33, Johannes HÃlzl <hoelzl at in.tum.de> wrote:
> 
> 
> Am Freitag, den 02.12.2016, 16:09 +0000 schrieb Lawrence Paulson:
>> As a rule, people should use non-standard analysis rather than the
>> extended naturals or reals. Although the former are more complicated,
>> they preserve all the first order properties of their standard
>> counterparts. In particular, the non-standard naturals are still a
>> semiring. 
> 
> Hm, enat also forms a semiring:
> 
>   instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}"
> 
> 
>> --lcp
> 





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