Talk:Proof: Difference between revisions

:::: But all the languages which ​​are suitable for this task are based on some metatheories. Twelf is based on the [[wp:Logical_framework|LF]], Agda and Omega are based on the [[wp:Intuitionistic_type_theory|MLTT]], Coq is based on the [[wp:Calculus_of_constructions|CIC]] (which is variation of the MLTT), MLes and Haskell usualyusually based on polymorphic lambda calculus ([[wp:Hindley%E2%80%93Milner|HM]] or [[wp:System_F|SystemF]], however, they are ''not'' suitable) and so on. There is also other systems such as Mizar, MetaMath or ACL2 which are based on the set theory rather than on Type Theory.

:In mathematics, when we speak of "a binary operation on S", we mean a function whose domain is S × S and whose codomainco-domain is S. So "addition on the natural numbers" means an addition function that takes two naturals and returns a natural. —[[User:Underscore|Underscore]] 00:42, 6 November 2009 (UTC)

:: I'm sure it was a fun thing to write, but "not much of a proof" is the problem here. I can write any kind of code to prove odd + odd = odd, and I can make it compile, but that proves nothing; only when I run the code, and do a test like "is 1 + 3 odd?" The code will go 1 + 3 = 4-> pred 2 ->pred 0 (BOOM, hopefully, because first element is 1), so that's a counterproofcounter-proof, <i>but</i>, the key is, you <i>have to run your logic in the code to make a proof</i>, merely compiling means nothing. If you aggreeagree to that, now convince me your code can prove even + even = even: I won't likely live long enough to see your program exhastivelyexhaustively test all even numbers. See my point? However fun it was with the axioms and writing the code, I just don't think this code counts as fullfillingfulfilling the task. --[[User:Ledrug|Ledrug]] 23:43, 21 June 2011 (UTC)

: I think the task is quite clear: "prove that the addition of any two even numbers is even". ''Any''. It is not possible with bruteforcingbrute-forcing, since there is a countable many even numbers. Nevertheless, a [[wp:Constructive_proof|constructive proof]] can be given in a suitable logical system (such as ACL2) or in a language with dependent types (Agda, Coq, Twelf to name a few).

: Putting something that looks like "2" in the CPU register, the same "2" in another, performing ADD, and getting something that looks like "4" doesn't help - that is not a proof! :) You need to ''define'' numbers, rules for arithmetic, induction, etc ''in'' the language based on a suitable [http://ncatlab.org/nlab/show/type+theory metatheory] such as [[wp:Intuitionistic_type_theory|MLTT]] or [[wp:Calculus_of_constructions|CoC]]/[[wp:Calculus_of_inductive_constructions|CoIC]], then prove. E.g., in the Agda version <code>even+even=even</code> takes ''any'' two even numbers and returns their sum as an even number, this is a ''type'', i.e. logical ''proposition'', ''algorithm'' itself is a ''proof'' by induction which ''builds'' a required term of a given (inhabited) type, and the typecheckertype-checker ''performs'' that proof (so that this is compile-time verification). &mdash; [[User:Ht|Ht]] 02:44, 12 May 2012 (UTC)

:::: You have overgeneralized my statement. OvergeneralizationsOver-generalizations are, generally speaking: wrong.

::: Finite sets is countable too (well, depending on the terminology, see the wikipediaWikipedia entry on the countable sets).

:: By extension [[User:Rdm|Rdm]] believes that because mathematicainsmathematicians 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. &mdash;''[[User:Ruud Koot|Ruud]]'' 13:11, 14 May 2012 (UTC)