Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Posting-Version: version B 2.10.1 6/24/83; site mmintl.UUCP Path: utzoo!watmath!clyde!cbosgd!ihnp4!houxm!vax135!cornell!uw-beaver!tektronix!hplabs!pesnta!pyramid!decwrl!decvax!genrad!panda!talcott!harvard!cmcl2!philabs!pwa-b!mmintl!franka From: franka@mmintl.UUCP (Frank Adams) Newsgroups: net.religion,net.math Subject: Re: Conditioning for Reason Message-ID: <1054@mmintl.UUCP> Date: Fri, 17-Jan-86 19:17:39 EST Article-I.D.: mmintl.1054 Posted: Fri Jan 17 19:17:39 1986 Date-Received: Thu, 23-Jan-86 08:40:39 EST References: <2314@umcp-cs.UUCP> <2232@pyuxd.UUCP> Reply-To: franka@mmintl.UUCP (Frank Adams) Followup-To: net.math Organization: Multimate International, E. Hartford, CT Lines: 94 Xref: watmath net.religion:8970 net.math:2684 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