Talk:Proof: Difference between revisions

This is not a proof, right? — [[User:Ht|Ht]] 13:27, 10 May 2012 (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 bruteforcing, 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 typechecker ''performs'' that proof (so that this is compile-time verification). &mdash; [[User:Ht|Ht]] 02:44, 12 May 2012 (UTC)