Anonymous user
Talk:Proof: Difference between revisions
→J version: re
m (→J version) |
(→J version: re) |
||
Line 99:
::::::: More specifically, when dealing with a concept like "Natural Numbers", a computer cannot represent them in their entirety. Instead, we have to accept some symbol which represents them. And, thus, when we deal with a "proof about Natural Numbers" we are really dealing not with natural numbers but with a surrogate. The surrogate can have only a subset of all properties of natural numbers. A question then, in the context of a proof is: does the mechanical implementation represent all relevant properties of natural numbers in the surrogate? In the context of "even" and "odd" all of the relevant properties are present in single digit decimal numbers and their sums (and by this, I mean that you are not going to be able to demonstrate any relevant exceptions, without going outside the bounds of this task).
::::::: Thus, your point seems to be that you want the task to be expressed in a system which expresses the relevant rules using a particular system of symbols, and you want the task to demonstrate that the language uses the "proper sorts of manipulation" of those symbols. But that has problems: (a) the task does not really define what is "proper", and (b) as near as I can tell, a person would have to study the language implementation to determine whether treatment of [for example] induction with excluded middle is handled adequately. --[[User:Rdm|Rdm]]
:::::::: A computer certainly ''can'' represent the natural numbers in their entirety! For example in Agda:
data ℕ : Set where
o : ℕ
1+ : ℕ → ℕ
:::::::: The number of inhabitants of this type is infinite, but its ''representation'' is finite. This type has exactly the same properties as the natural numbers, because it precisely encodes the [[wp:Peano axioms|Peano axioms]].
:::::::: There certainly are different approaches to "solving" this task (e.g. a solution in HOL or Isabelle would look rather different than one in Agda, Coq or Twelf) but there are some reasonable things a solutions/language would have to do/support:
::::::::# State the required theorem (e.g. encoded as a type in the language's type system.)
::::::::# Give the proof of the theorem in such a way that it can be mechanically verified - in a finite amount of time - to be a valid proof by the compiler (e.g. encoded as a program that has the required type encoding the theorem.)
:::::::: The Agda, Coq and Twelf solutions do precisely this. The Omega solution does as well, if one is convinced this solution restricts itself to a sound subset of language. I don't quite follow the J sample but it seems to add a small number of even number and verifies that they are in fact even (one counterexample is enough to disprove a theorem, any finite number of examples are not enough to demonstrate a property holds for all natural numbers.) It doesn't seem to "Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers." as requested by the task. —''[[User:Ruud Koot|Ruud]]'' 16:44, 10 May 2012 (UTC)
| |||