Talk:Proof: Difference between revisions
Content added Content deleted
m (better fix) |
(→Quantifiers: new section) |
||
Line 172: | Line 172: | ||
:: The "but" is that fact that Haskell allows general recursion, making the logic unsound, i.e. any theorem - including false ones - can be proven by an expression that would diverge at run-time. The given solution does not use this "feature", however. |
:: The "but" is that fact that Haskell allows general recursion, making the logic unsound, i.e. any theorem - including false ones - can be proven by an expression that would diverge at run-time. The given solution does not use this "feature", however. |
||
:: This is a solution that the task should clearly allow, with the appropriate footnotes, though. —''[[User:Ruud Koot|Ruud]]'' 18:35, 12 May 2012 (UTC) |
:: This is a solution that the task should clearly allow, with the appropriate footnotes, though. —''[[User:Ruud Koot|Ruud]]'' 18:35, 12 May 2012 (UTC) |
||
== Quantifiers == |
|||
The currently phrasing of this task places emphasis on "any" (pair of even natural numbers) and on "every" (use of addition between those numbers). |
|||
But the task also requires that the language implement the natural numbers so represented. |
|||
This is either a contradiction (since every language can only implement a finite set of distinct numbers and there are an infinite number of "Natural Numbers") or a new use of the term "Natural Number" which I am not familiar with (in which case the required definition should be included in the task description). |
|||
--[[User:Rdm|Rdm]] 19:44, 13 May 2012 (UTC) |