Anonymous user
Talk:Proof: Difference between revisions
m
→Deletion of statement about finite limits from task: gr.
No edit summary |
|||
Line 280:
:: This is not searchable text, it's photographic material and it uses a variety of definitions defined in other places. So it's difficult, at a glance to see if it adequately treats the topic of machine limitations in an implementation. If any of this is relevant to the topics of limits of validity, please restate the relevant constructs in your own words. --[[User:Rdm|Rdm]] 13:17, 14 May 2012 (UTC)
::: 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
::: The section about natural numbers is on 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 operation on lists from [2]). — [[User:Ht|Ht]] 14:06, 14 May 2012 (UTC)
| |||