Anonymous user
Talk:Proof: Difference between revisions
→Quantifiers: re
(→Quantifiers: re) |
|||
Line 204:
:::: It seems, though, that you are saying that you accept as valid a type system where an infinity of the symbolized values are not implemented by the implementation -- where only finitely many values symbolized by the type are implemented. --[[User:Rdm|Rdm]] 21:42, 13 May 2012 (UTC)
::::: Then read my above sentence as "... have an infinite set of distinct values". The "distinct" was already there implicitly (all elements in a set are always distinct), so the statement remains equally true.
::::: I'm not exactly sure what you mean with "accept as valid a type system where an infinity of the symbolized values are not implemented by the implementation", so I can't say if I agree with that or not. As a proof by induction of even + even = even does not rely on actually computing any particularly large objects, it is quite irrelevant if the implementation has any limitations of what the maximum size of the finite representation of these infinite models can be. —''[[User:Ruud Koot|Ruud]]'' 22:12, 13 May 2012 (UTC)
| |||