Talk:Proof: Difference between revisions
→Quantifiers
(→Quantifiers: re) |
|||
Line 186:
: The set of natural numbers is countably infinite. They are defined by a finite formal systems (the Peano axioms). A proof about a property holding for all natural numbers can be given in a finite form (using induction). You may indeed not be familiar with these facts, but they are most certainly not novel. —''[[User:Ruud Koot|Ruud]]'' 20:41, 13 May 2012 (UTC)
:: Ok, that's ambiguous terminology. I agree that "countable" in the mathematical sense means aleph null style infinity -- "has a one-to-one correspondence with natural numbers".
:: However, in a computer program, an infinity cannot be implemented. A computer program can only implement a finite set of distinct values. Thus, in the context of a type -- when using the normal meanings of "countable" and "type" -- natural numbers are not countable.
:: That said, if you really mean for a program to implement a "countably infinite" type, that is itself a failure in specification. At the very least, you should be obligated to say what you mean by "type" when the usual meaning of type in programming refers to something which can only enumerate a finite set of values without failure.
:: My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types. --[[User:Rdm|Rdm]] 21:05, 13 May 2012 (UTC)
| |||