Talk:Proof: Difference between revisions

Content added Content deleted
No edit summary
Line 280: 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 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 mentioned to be glanced over, but read thoroughly. —''[[User:Ruud Koot|Ruud]]'' 13:46, 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 intended to be glanced over, but read thoroughly. —''[[User:Ruud Koot|Ruud]]'' 13:46, 14 May 2012 (UTC)


::: 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)
::: 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)
Retrieved from "https://rosettacode.org/wiki/Talk:Proof"