Anonymous user
Talk:Proof: Difference between revisions
no edit summary
No edit summary |
|||
Line 281:
::: This is a seminal early paper in the field of Type Theory (the capital T one, i.e. dependent type theory) and proof assistants. It's indeed not mentioned to be glanced over, but read thoroughly. —''[[User:Ruud Koot|Ruud]]'' 13:46, 14 May 2012 (UTC)
::: Section about natural numbers is on 71 page. That is, the Peano axioms is embeddable into MLTT (even constructive ZF set theory is embeddable), so that the questions should be asked about MLTT itself. There is some free books - [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/], [http://www.cse.chalmers.se/research/group/logic/book/] (see indexes for examples, e.g. the associativity of the append operations on lists from [2]). — [[User:Ht|Ht]] 14:06, 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)
| |||