**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

**weemba@brahms.BERKELEY.EDU (Matthew P. Wiener)** (01/21/86)

>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".) Frank, I think you do know the answer, but got too carried away by the discussion! The consistency of set theories, either stronger or weaker than ZFC, can all be coded into questions about whether or not a certain polynomial has integral solutions, by the Matiyasevich theorem. These Diaphontine problems should answer your question. For further details, see my recent posting in net.{philosophy|ai}, "Re: a halting problem: a meaty response", where a similar question came up with about the same answer. ucbvax!brahms!weemba Matthew P Wiener/UCB Math Dept/Berkeley CA 94720

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

In article <11480@ucbvax.BERKELEY.EDU> weemba@brahms.UUCP (Matthew P. Wiener) writes: >>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. > >Frank, I think you do know the answer, but got too carried away by the >discussion! The consistency of set theories, either stronger or weaker >than ZFC, can all be coded into questions about whether or not a certain >polynomial has integral solutions, by the Matiyasevich theorem. These >Diaphontine problems should answer your question. Can you prove that there is such a problem which is not solvable in N(a) for any constructable ordinal a? It seems plausible, but plausibility and proof are two different things. Frank Adams ihpn4!philabs!pwa-b!mmintl!franka Multimate International 52 Oakland Ave North E. Hartford, CT 06108