Let us construct a symbolic formal system with the following elements.
1. An arbitrary axiomatic system which contains Gödel’s axiomatic system together with its rules of inference (Ga)
2. The functions and relations of the system are recursively defined and free from contradiction.
3. We construct an isomorphic representation of the subsystem of non-numerical symbols by a system of positive integers, ascribing natural numbers to the symbols. Therefore, we can express any formula in numerical terms (particularly as a sequence of primes), and proofs as sequences of positive integers.
4. We construct a set of formulas F which are directly deducible within the system and which represent common expressions of our calculus.
For every formula fi ∈ F, there is a numerical formula pi ∈ P, for P⊂ F, such that Ga ⊢ pi.
Construct a fj which expresses “this formula is not deducible”, a valid and meaningful expression of our calculus. Therefore, there is a pj numerical formula that corresponds to fj.
The undecidability theorem says that pj is undecidable. Suppose pj is true. Then pj is not deducible, but pj ∈ F, set of directly deducible formulas, so there is a contradiction. Suppose pj is false. Then ¬ pj is true, id est, pj is deducible, but pj says that it is not deducible, so there is a contradiction.
Ga is not complete.
Is this is similar to the following informal famous logic proof: S="This statement S is False". S cannot be true because it contradicts its definition which is "S is false." S cannot be false because if S was false then, it contradicts Non S "This statement is not false"?
ReplyDelete