Revision as of 14:06, 14 May 2012 (view source) rosettacode>Ht No edit summary ← Older edit		Revision as of 14:11, 14 May 2012 (view source) rosettacode>Ht No edit summary Newer edit →
Line 282: ::: 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~~The section about natural numbers is on 71 page 71. 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~~operation 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)

Talk:Proof (view source)