Anonymous user
Talk:Proof: Difference between revisions
→Quantifiers: re
(→Quantifiers: re) |
(→Quantifiers: re) |
||
Line 267:
: The "implementation of the type" is the implementation of Martin-Lof type theory (or its extension), [http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf the paper] has a model of natural numbers similar to the system of Peano axioms. — [[User:Ht|Ht]] 12:56, 14 May 2012 (UTC)
:: By extension [[User:Rdm|Rdm]] believes that because mathematicains only have a finite number of sheets of paper they have only been able to prove theorems about the natural numbers which hold up to some non-trivial finite limit. I'm not sure how to argue with someone who is so confused about elementary concepts. —''[[User:Ruud Koot|Ruud]]'' 13:11, 14 May 2012 (UTC)
This will be my final attempt to clarify this to you (please grab a book or article on type theory if you want to know how mathematicians and computer scientists define a type): The only implication of the fact that an actual implementation of a given logic/type theory runs on a machine with a finite amount of memory is that the set of results the compiler can give is extended from "I was able to verify the proof as correct" and "I was able to verify the proof as incorrect" with "I'm unable to verify the proof as either correct or incorrect because I ran out of memory". The third option must not occur here. The compiler should say "I was able to verify the proof as correct", assuring us that the property even + even = even hold for all countably infinite pairs of natural numbers.
| |||