From: Jesse F. Hughes on 2 Mar 2010 13:22 "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes: > Newberry <newberryxy(a)gmail.com> writes: > >> On Mar 2, 6:30 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote: >>> Suppose, for instance, that we have a proof >>> >>> (Ex)Px -> (Ex)(Px & Qx). >>> >>> For instance, let Px stand for (E a,b,c)(a^x + b^x = c^x) and Qx stand >>> for x is prime. Then we know that the above sentence is true: if >>> there is a counterexample to Fermat's last theorem, then there is a >>> counterexample in which the exponent is prime. >>> >>> Equivalently, >>> >>> ~(Ex)(Px & Qx) -> ~(Ex)Px. (1) >>> >>> Suppose further that I prove (according to the usual notion of >>> mathematical proof) that >>> >>> ~(Ex)(Px & Qx). (2) >>> >>> Then, (1) and (2) allow me to conclude >>> >>> ~(Ex)Px. (3) >>> >>> Ah, but here's the rub! According to your comments, if (3) is true, >>> then (2) is neither true nor false and hence not true. If (2) is not >>> true, then surely there is something wrong with my proof of (3), since >>> my proof of (3) depends on (2). I thought I had a proof of (2), but >>> it turns out that I didn't. >>> >>> At this point, you may say that what I really had was a proof of a >>> second-order statement >>> >>> ~T((Ex)(Px & Qx)), (2') >>> >>> and that I can somehow use (2') and (1) to derive (3), but you are >>> only blowing steam at present, since you haven't given us any >>> second-order logic to conclude that (1) & (2') |- (3). >>> >>> Statements like (2) are useful in mathematical reasoning. We use them >>> to derive statements like (3) >> >> Obviously if we do not use clasical logic the derivation system will >> be different. If we have a semantically complete system and >> >> ~(Ex)Px. (3) >> >> is true then we will be able to prove it. Your example is useful when >> we use classical logic. If we do not then it will not be useful. It is >> that simple. > > I just don't see any reason to give up a perfectly straightforward and > sensible argument (like that above) in order to fit your intuitions > that, if (3) is true, then (2) is neither true nor false. Perhaps > t-relevance logic is useful, but it does not seem to be satisfactory > for mathematical reasoning. In mathematics, the argument I outlined > above is a perfectly good argument for (3). I misspoke here, since t-relevant logic doesn't (yet?) do anything regarding predicate calculus. I meant that perhaps the logic that Newberry wants is useful for something -- but that logic still does not exist, of course. > Seems to me that you've got quite a job convincing mathematicians > otherwise. -- Jesse F. Hughes "Of course, my ability to admit my mistakes and correct them is a trait that many of you seem to never have properly appreciated." -- JSH, discussing his 1463rd "proof" of Fermat's Last Theorem.
From: MoeBlee on 2 Mar 2010 13:46 On Mar 1, 11:36 pm, Newberry <newberr...(a)gmail.com> wrote: > > > b) Is this > > > > (x)((2 > x > 4) -> ~(x < x + 1)) > > > > "ordinary mathematical reasoning"? > > > It isn't reasoning at all. It's a formula that doesn't formalize any > > statement we would ordinarily meet in mathematical reasoning. > > So why do you exhort people that it is true? Aatu can answer for himself, but I would say it is true based on the principle that an if-then statement with false antecedent is true (and though this is counter-intuitive to certain people it is also intuitive in the sense when people say things like "If Sarah Palin is well versed in political philosophy and the particulars of public affairs then I'm a monkey's uncle", which is true since Sarah Palin is decidedly a complete dope as to anything in political philosophy or public affairs). This doesn't contradict that the particular statement you display is not one that we would expect oridinarily to meet. MoeBlee
From: Nam Nguyen on 2 Mar 2010 23:43 Aatu Koskensilta wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> You should have told me so years ago. Now I feel "unfortunate" that I >> bought Shoenfield's "Mathematical Logic" to loose my precious time >> learninng formal systems and FOL proofs! (Kind of kidding, of course!) > > There are some formal proofs in Shoenfield's _Mathematical Logic_ but > mostly we find just loads of ordinary mathematical proofs of theorems > about formal provability, formal proofs, formal systems, models, > recursive functions, definable sets of naturals, axiomatic set > theory. Here by "ordinary mathematical proof" is meant a piece of > mathematical reasoning (in mathematical English) from basic mathematical > principles -- the principle of mathematical induction, basic properties > of addition and multiplication, ... -- establishing some conclusion. > >> You seem to have lost me here. Isn't formalizing a proof in a formal >> system essentially the same as deducing a formal system theorem, which >> as you said above isn't the case because "G�del's proof isn't a formal >> proof in a formal system."? > > I can't really see what it is you find difficult to understand. Because you explained a technical judgment with non-technical opinions which actually didn't quite correlate with Godel's paper. (And I'm going to elaborate on this). > G�del's > proof is not a formal proof, as is apparent on even a brief glance at > the paper, First of all, FOL formal proof is a technical concept and whether or not Godel's proof is a formal one should be judged on technical evidences, *not* on a *vague and subjective* opinions such as "as is apparent on even a brief glance at the paper". Secondly, the translated version I have is 26 page-long and 24 of them are full of FOL proofs and formulas that one could easily mistake the paper for a prt Shoenfield's modern textbook on FOL formal systems! And that doesn't at all correlate with your assessment that his proof isn't a formal proof just because of a "brief glance" at it. So of course I found it difficult when a technical judgment was rendered on the ground of vague and subjective opinion. > but we can formalise it to give a formal proof in a suitable > formal system, such as primitive recursive arithmetic. Secondly, if you could formalize what he wrote into a full blown formal proof then in effect his proof was essentially a formal proof to begin with! You just have to forgive the fact that there's always the possibility certain amount of "informality", "idiosyncrasy" would exist in technical presentations. I could easily cite one or two "crazy" informalities in Schoenfield's book but that wouldn't make the proofs in his book no less formal than the proofs in Godel's paper! > In this it is no different from any proof in mathematics. "Any any proof in mathematics" is way too vague to really understand what you said here. > That the proof doesn't involve > e.g. any model theoretic considerations we ascertain simply by > inspecting the proof and the relevant definitions. I hate to say it but "simply by inspecting the proof and the relevant definitions" simply isn't a *technical* explanation of the technical judgment on whether or not Godel's proof is a FOL formal proof. We all know the criteria for determining whether or not his proof is formal: if there's a formal system where what he asserted is a theorem, then his proof is a formal proof. If not then his proof isn't. It's that's straight forward which doesn't require explanation on thing such as "ordinary mathematical proof", as you said. If you say, for example, his theorem can be proven in the formal PRA then there's a formal proof for what he asserted in the paper, hence at the same time saying there's no formal proof for what he asserted is contradictory. Naturally. *** Godel's proof isn't a formal proof for a _different reason_, despite that the formula (~Bew_c[(17 Gen r)] /\ ~Bew_c[Neg(17 Gen r)]) is a theorem in a "proving"/"encoding" formal system, such as PRA.
From: Nam Nguyen on 3 Mar 2010 00:03 Aatu Koskensilta wrote: > That the proof doesn't involve > e.g. any model theoretic considerations we ascertain simply by > inspecting the proof and the relevant definitions. Really? How about: (1) "0=0 is true" is true (2) "0=0 is true" (3) "0=0" (4) 0=0 Isn't it true that there's convention that in certain proper context (1) asserts the same truth as (4)? [And (4) is just a formula!]
From: Newberry on 3 Mar 2010 01:19
On Mar 2, 10:15 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote: > Newberry <newberr...(a)gmail.com> writes: > > On Mar 2, 6:30 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote: > >> Suppose, for instance, that we have a proof > > >> (Ex)Px -> (Ex)(Px & Qx). > > >> For instance, let Px stand for (E a,b,c)(a^x + b^x = c^x) and Qx stand > >> for x is prime. Then we know that the above sentence is true: if > >> there is a counterexample to Fermat's last theorem, then there is a > >> counterexample in which the exponent is prime. > > >> Equivalently, > > >> ~(Ex)(Px & Qx) -> ~(Ex)Px. (1) > > >> Suppose further that I prove (according to the usual notion of > >> mathematical proof) that > > >> ~(Ex)(Px & Qx). (2) > > >> Then, (1) and (2) allow me to conclude > > >> ~(Ex)Px. (3) > > >> Ah, but here's the rub! According to your comments, if (3) is true, > >> then (2) is neither true nor false and hence not true. If (2) is not > >> true, then surely there is something wrong with my proof of (3), since > >> my proof of (3) depends on (2). I thought I had a proof of (2), but > >> it turns out that I didn't. > > >> At this point, you may say that what I really had was a proof of a > >> second-order statement > > >> ~T((Ex)(Px & Qx)), (2') > > >> and that I can somehow use (2') and (1) to derive (3), but you are > >> only blowing steam at present, since you haven't given us any > >> second-order logic to conclude that (1) & (2') |- (3). > > >> Statements like (2) are useful in mathematical reasoning. We use them > >> to derive statements like (3) > > > Obviously if we do not use clasical logic the derivation system will > > be different. If we have a semantically complete system and > > > ~(Ex)Px. (3) > > > is true then we will be able to prove it. Your example is useful when > > we use classical logic. If we do not then it will not be useful. It is > > that simple. > > I just don't see any reason to give up a perfectly straightforward and > sensible argument (like that above) in order to fit your intuitions > that, if (3) is true, then (2) is neither true nor false. Perhaps > t-relevance logic is useful, but it does not seem to be satisfactory > for mathematical reasoning. In mathematics, the argument I outlined > above is a perfectly good argument for (3). > > Seems to me that you've got quite a job convincing mathematicians > otherwise. I encourage you to look at the big picture and not just pick at one particular aspect. And do not worry about mathematicians. You can make your own judgement, can you not? > -- > Jesse F. Hughes > "I'm a geek hatchling." -- Quincy P. Hughes, age 7- Hide quoted text - > > - Show quoted text - |