Anonymous user
Talk:Proof: Difference between revisions
no edit summary
No edit summary |
No edit summary |
||
Line 222:
::::: > This is trivially false, since every computer has a finite amount of memory
::::: Real computers are not even Turing complete, that is why the word "potentially" was used. But this is not a problem because of [[wp:Mathematical_constructivism|constructivism]]/[[wp:Finitism|finitism]].
::::: Just as you can prove `even + even = even` (for ''all'' natural numbers) by using a finite amount of paper and in finite number of steps, computer (proof system) can do this using a finite amount of memory in a finite time.
Line 238:
::: > My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types
::: By "you" you mean anybody who "believe" in Agda/Coq/Epigram/Twelf/ATS/NuPRL/ALF/DML/LEGO/HOL/Isabele/ACL2/Mizar/MetaMath/etc. proofs? Did you believe in 4-color theorem proof? Did you reject implementations of the homotopy type theory in Coq/Agda?
:::: If your description here is correct, then these implementations of homotopy type theory have weaknesses in their treatment of upper bounds. No big deal, perhaps, except that you seem rather intolerant of other implementations with the same kind of limitation. --[[User:Rdm|Rdm]] 01:53, 14 May 2012 (UTC)
| |||