[net.religion] Conditioning for Reason

franka@mmintl.UUCP (Frank Adams) (01/18/86)

I am moving this discussion to net.math, since it no longer has anything to
do with religion.  The article is cross-posted; followups should be to
net.math only.  (Is this a net first?  Moving a discussion *from*
net.religion *to* net.math?)

In article <1113@cvl.UUCP> harwood@cvl.UUCP (David Harwood) writes:
>In article <1026@mmintl.UUCP> franka@mmintl.UUCP (Frank Adams) writes:
>>In article <368@cisden.UUCP> john@cisden.UUCP (John Woolley) writes:
>>>Goedel showed that there are statements in arithmetic whose truth or
>>>falsity cannot be determined.  He did not (indeed, his whole point was
>>>that he *could not*) say that any particular such statement was true.
>>>But if X is such a statement, then either X or not-X (you don't know
>>>which) is true, but unprovable.  That's what I meant.  It's you who
>>>have misread Goedel.  (Or not read him at all?)
>>
>>This is not quite correct.  Goedel's proof constructs a statement X which
>>is equivalent to the assertion that X is not provable in the formal system.
>>Assuming the system is consistent, it follows that X is true.
>>
>>If one assumes Church's thesis, one can get the further result that there
>>is no algorithm for determining the truth or falsity of statements in
>>arithmetic.  This is closer to the result you want, but still not quite
>>there.  It does not show that there are any statements whose truth cannot
>>be determined at some appropriate level of meta-theory (this gets into
>>ordinal number theory).  I don't know of any results on this question.
>
>		There is really nothing wrong with John Woolley's
>	statement, speaking informally to a solemn net.religion
>	assembly: Goedel did show that that first-order number theory
>	(arithmetic) is (recursively) undecidable, and he did this, not as 
>	you say, but by a general construction of number theoretic BADWFFs
>	themselves representing predicates of their 'proofs' (ie
>	expressing part of the 'meta-theory of number theory' within
>	the theory 'proper'. Specifically, he showed that a consistent
>	FOL number theory becomes inconsistent if *either* a BADWFF
>	or its negation ~BADWFF is added to the usual axioms.
>		Mr. Adams' account is not correct in two respects:
>	first, he misunderstands Goedel's method, which is to construct
>	BADWFF X, assume that it is true, then prove a contradiction!
>	Secondly, furthermore, with greater difficulty, Goedel assumes
>	'not BADWFF X', and also proves a contradiction!

This is just not true.  The contradiction arises not from the assumption
that X is true, but from the assumption that it is provable in the formal
system.  In fact, one can add either X or not X to the formal system, and
neither will give a contradiction.  It is the case that if adding X to the
system would yield a contradiction, then not X is provable in the system.

In fact, it is the case that the statement X generated by Goedel's proof
must be true.  Besides the argument I gave above, there is another way to
see this.  The statement is of the form ~(EX1 EX2 ... EXn P(X1,X2,...,Xn))
[here E is the "there exists" quantifier], where P is a decidable predicate
(that is, given integers X1,...,Xn, one can readily prove whether
P(X1,...,Xn) is true or not).  If the statement were false, one could
actually find the integers X1,...,Xn which falsify it, and use them to prove
it false.

If one adds X to the formal system, one gets a new formal theory, N(1), which
includes all the axioms of the system N plus the one new one.  In that
new theory, one can derive a new statement X(1), which is not decidable
(provable or disprovable) in that theory.  If one adds X(1) as an axiom, one
gets yet another formal theory N(2), for which a statement X(2) can be derived.
Etc.

The series of statements X[=X(0)],X(1),X(2),... are in fact constructable.
That is, one can decide whether a statement is in the list, and one can
generate the list, using a computer program.  This being the case, one can
create a new formal theory N(w) which includes all of them as axioms.  In
this formal theory, one can derive a statement X(w) [w here represents omega,
which is an ordinal number], which is not decidable for the theory.  In
this way, one can associate a theory with each computable ordinal number,
and a statement which is not decidable in each such theory.  (One cannot
proceed past the first uncomputable ordinal, u, because the set of statements
X(a) for a<u is not computable, so N(u) is not a formal theory.)

The question I don't know the answer to is the following: is there any
closed number-theoretic formula X, such that neither X nor not X is provable
in the system N(a) for any computable ordinal a?  (I would guess that
the question is not decidable.)  If there is such an X, then it may be
correct to assert that there are statements of number theory which are
not accessable to reason.  If there is no such X, then the assertion is
false.  (The commonly quoted conclusion that there are true statements
which we cannot know is based on the assumption that we are in fact
equivalent to a Turing machine, and thus limited to the theory N(a) for
some ordinal a < u.  In other words, "not accessible to *our* reason",
not "not accessible to reason".)

(I have, by the way, proved Goedel's theorem; I have even taught a course in
which we worked through Goedel's theorem.  I have a Master's degree in
math from the University of Chicago; I dropped out a PhD program in math
at MIT to pursue other goals.)

Frank Adams                           ihpn4!philabs!pwa-b!mmintl!franka
Multimate International    52 Oakland Ave North    E. Hartford, CT 06108