Talk:Proof: Difference between revisions
refactor comments
(→Quantifiers: re) |
(refactor comments) |
||
Line 261:
::: My current inclination is to believe that you cannot get [http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf the point] of dependently-typed programming languages / proof systems. — [[User:Ht|Ht]] 23:00, 13 May 2012 (UTC)
: Your last addition:▼
:: Note also that it's expected that the implementation of the type will fail to satisfy the peano axioms for some values. It's only required that the implementation succeed for values which do not exceed some non-trivial finite limit. The proof is not meant to apply to the implementation for values which exceed that limit.▼
: 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)
Line 275 ⟶ 269:
I'm strongly getting the impression that you've never managed to work out a proof by induction on paper, however, making this beyond you abilities to comprehend. In that case either do the appropriate background research or simply accept this on authority. —''[[User:Ruud Koot|Ruud]]'' 12:04, 14 May 2012 (UTC)
== Deletion of statement about finite limits from task ==
(I moved this from in the middle of some other comments to its own subtopic.)
▲: Your last addition:
▲:: Note also that it's expected that the implementation of the type will fail to satisfy the peano axioms for some values. It's only required that the implementation succeed for values which do not exceed some non-trivial finite limit. The proof is not meant to apply to the implementation for values which exceed that limit.
▲: 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)
| |||