details re Z-R |- PA consistent
in [Math]
|
From: Nam Nguyen on 5 Jul 2010 23:11 Aatu Koskensilta wrote: > William Hale <hale(a)tulane.edu> writes: > >> But, I am not asking whether this is a viable approach. I am asking if >> this is what you are doing. I understand that you will introduce >> "model theory" to wrap up the proof. But, I am taking this >> introduction of "model theory" to be similar to the introduction of >> "complex number theory" to wrap up a proof in basic number theory (eg, >> proving Fermat's last theorem). > > I have already posted an outline of a proof where we need not invoke any > model theory, indeed nothing beyond basic properties of naturals and an > elementary infinitary inductive definition, stuff probably transparent > to anyone who's ever seen any inductive definitions in mathematics. The unfortunate thing for us, however, is that "basic properties" of the natural numbers have dual faces: one can also express the fundamental theorem of arithmetic _without_ induction at all! > Only an overexposure to formalities, or a bent mind -- not that that's > necessarily a bad thing > -- can possibly lead one to doubt the > legitimacy, correctness, evidence, sureness, of such mathematical > constructions and see-for-yourself proofs thereof. Difficulties in sciences in general were often marked by seemingly contrasting realities: the relativity vs the absoluteness of the speed, of light, the clock-work universe vs Heisenberg's Uncertainty, the wave vs particle duality of photons, etc... And in those difficult times of knowledge, _only non-bias reconciliation of concepts_ would prevail! Today we're facing the same kind of difficulty in FOL reasoning: the seemingly irreconcilable induction nature of pCG expression, and the non-induction counterpart of cGC. If, in the name of familiarity of "ordinary" mathematics, we _discard_ one of them (the later) so that our reasoning life be somehow less "burdened" then we have indeed failed what is the spirit of mathematics and mathematical reasoning! Both then are condemned to the sorrow state of eternal stagnation!
From: herbzet on 5 Jul 2010 23:15 herbzet wrote: > Just btw, my cousin set a collegiate record, back in the day, for > continuous radio broadcasting, under the name of "Beau Harris" -- > five days with a lot of coffee and only a little dozing during long > cuts. > > Just to give you something to shoot for ... http://en.wikipedia.org/wiki/KWUR#History
From: William Hale on 5 Jul 2010 23:34 In article <87pqz1jsa0.fsf(a)dialatheia.truth.invalid>, Aatu Koskensilta <aatu.koskensilta(a)uta.fi> wrote: Briefly, I think that you are saying I am wrong when I say that logicians don't work in ZFC. I agree that I was wrong. I understand that you don't like the term "work in ZFC" since mathematicians don't work in ZFC as such. But, I am using the term "work" as a shorthand for what is meant when we say that ZFC serves as a foundation for proving things in standard mathematics. By standard mathematics, I was limiting myself to the areas of real analysis, complex analysis, algebra, topology, and (differential) geometry. That is, areas of mathematics discussed before 1900. I didn't include logic since its main results were done after 1900. Let me give some more on what I mean by "work in ZFC". I think some non-mathematicians think that a mathematician comes up with an informal proof and that it may or may not be formalized. For example, a mathematician might come up with an informal proof that that two natural number always has a least common multiple. I think the non-mathematician might then think in order to formalize this informal proof, one would first decide what axioms system to use, say PA or ZFC. I object to this viewpoint (if anyone actually even has it). The mathematician should already have decided what axiom system he is working in, either PA or ZFC, before he writes out his informal proof. If I were given the exercise to prove that theorem in a class where I was learning PA, then I would consider the theorems that have been proved in PA to come up with a (informal) proof of existence of LCM. But, if I were given the exercise to prove that theorem in a class where I was learning abstract algebra (where ZFC is the foundation, since we talk about sets and Zorn lemma a lot), then I would consider the theorems that have been proved in ZFC to come up with a (informal) proof of the existence of LCM. These two informal proofs would not be the same, and my thought process would be different in the two cases. Thus, in the first case, I came up with an informal proof working in PA, while in the second case, I came up with an informal proof working in ZFC. I don't like the idea of just coming up with an informal proof, with no mention of the axiom system being used. Of course, I realize that many mathematicians could care less about all this when they prove things. > (Those who choose to read the following do so at their own risk. It > contains erratic rambling and pointless maundering. Some topical logical > babbling has been thrown in to fool the spam filter. (It would be very > helpful if those portions of this post had been marked somehow. It's a > pity that they aren't. I think it's mostly the middle bits, but it's > difficult to tell as reading what I've written puts me to sleep.) I > tried for half an hour to make it all -- that is, all of the nonsensical > twaddle I've for some reason liberally peppered this post with, at > random junctions, although usually within parentheses, happily) hang > together, then gave up. I then tried again. Alas, I had in the meantime > forgotten what it was all about so it only made things worse. Next, I > decided it would be a good idea to read a logic text for a while -- I > was trying to wrap my head around some erudite concepts of generalized > recursion theory -- and have a few cigarettes. After that, I returned to > polishing this post, and proceeded to do so. I soon found out I had no > idea what I had been earlier writing about, why I had made the > "corrections" I had made, and so on, so with hindsight it wasn't a great > idea. It was also not a huge success, judging by the result. My > apologies, (Plus, I promise to buy anyone who reads through this post a > few beers, making also a generous allowance to those who don't like to > alcohol that they have the choice of an American beer if they so wish.)) > > William Hale <hale(a)tulane.edu> writes: > > > At this point of time, my thinking is that the theory of PA can be > > made to correspond to something that can be given in ZFC. But my > > current thinking is that the theory of PA are metatheorems, rather > > than theorems of ZFC. I think I can see how the theory of PA and these > > metatheorems can be made to correspond to things in ZFC so that the > > metatheorems of the metatheory become theorems of ZFC. But, just like > > I don't think the non-Euclidean geometer so work in Euclidean > > geometry, I don't thing the mathematical logician should work in ZFC > > to do his thing. The logician is contemplating many axiom system with > > many different logical rules and many different deduction > > principles. The logician does not need to cast all of this into the > > ZFC system (even if it could be done). > > But should the logician accept, say, theorems of the form > > Theory T is inconsistent. > > There are infinitely many twin primes. > > and so on, on basis of their provability in ZF(C)? On what basis should > we accept as correct statements of the form > > The statement P is provable in theory T. > > The statement P is not provable in theory T. > > It is undecidable in PA whether P is provable in theory T. Well, I thought the logician was not working in ZFC. For example, take the deduction theorem in logic, which Enderton mentions in his book. I thought that this was a metatheorem. I took the proof of "A -> A" that used the deduction theorem and following the meta-proof of the deduction theorem, I was able to eliminate the use of the deduction theorem and just use the axioms given by Enderton to give a proof of "A -> A" according to the definition of proof that Enderton stated. Likewise, Enderton stated that you can cheat in a proof by just referring to previous theorems as justification, without having to refer back only to axioms (according to the definition of proof that Enderton stated). This seemed like a meta-theorem also. Whether these two meta-theorems needed to be proved ultimately in ZFC I didn't consider as necessary. Even now, I am not sure how they fit into logic as a logician would discuss them. I think that you are telling me that logicians have succumbed to using ZFC like the other mathematicians have. I understand and agree that the theory of Turing Machines are best done in the framework of ZFC, where one defines a turing Machine as a tuple of certain sets. I am not so sure that the lambda calculus should be done in the framework of ZFC (or even if you are saying that it is done in ZFC, though I suspect that you would say it is). > > ? Even medias res in contemplation of many many axiom systems and what > not, surely we should accept some such statements, reject some such > statements, remain undecided about some such statements. As a matter of > fact, we accept some such statements, reject some such statements and > steadfastly remain agnostic about some such statements, as with any > mathematical claims. We're not here dealing with some strange > metaphysical assertions, after all, but with perfectly meaningful > mathematical claims: there's a finite tree, graph, sequence (depending > on which way you swing when it comes to presenting formal proofs as > mathematical objects) meeting such and such mathematical > conditions. Surely whatever attitude we adopt towards claims and > assertions about finite trees, graphs, sequences, meeting > straightforwardly defined mathematical conditions, must extend also to > consistency statements. Whatever contemplating of different axiom > systems we may envisage is as relevant in case of the Kruskal tree > theorem, Dirilecht's theorem, the fundamental theorem of analysis, as it > is in case of consistency theorems. I guess I was misled by the term "meta", which you explain further down should not be given too much significance. I was reading too much into the term "meta". > > > I don't think that the claim that ZFC is the foundation of standard > > mathematics includes proving PA is consistent. > > Surely it does, since it's a trivial exercise to prove PA consistent in > standard mathematics. Ok. > > > I don't require that logicians work in ZFC. I think that is an > > artificial requirement. > > It's an extremely artificial requirement. No one "works in" ZFC in any > literal sense. I didn't mean it in a literal sense. I was comparing it more to trying to do non-Euclidean geometry in the framework of Euclidean geometry. Even though it could be done, I think that is artificial. As you are pointing out to me, you want to have ZFC provide the framework for you to prove your (logical) theorems about (logical) theories. > People just do mathematics in a way that, as it happens, > virtually always is formalizable in ZFC (or certain other standard > systems, e.g. in case of constructive or intuitionistic mathematics > (although even here we may note intuitionists and classical > mathematicians are happily agreed, in spite of their disagreement with > each other, and disagreement within, on what theories are > unproblematically consistent and on for what theories consistency is an > open problem, thanks, in no small part, to much work in proof theory > relating constructive and classical theories, which work, rather > curiously, is the main concern of a great many constructivists instead > the proving of constructive results as one might naively expect) in > intuitionistic analysis, constructive type theory, formalizations of > recursive mathematics), in so far as provability of results, suitably > formalized, is concerned. > > > (I again ask that the reader for patience, and also that they accept the > challenge of testing their hand, for no skill can develop without > practice and exercises that are on the verge of being impossible, their > keen skill at parsing, and of course, there being no implication my > readers are illiterate slobs, at easily understanding, making sense of, > and comprehensively comprehending arbitrarily deeply nested syntactic > constructions, finite instances of which can be discerned in the > preceding sentence. I ask only that they go about this task with a sense > of play and fun, as if children once again, shedding all needless cloths > of solemn adult seriousness (and pretentiousness) that serve no purpose > other than to conceal, or to reveal, so to speak, what is not really > there, creating a phantasm of cloth, of intimidating protruding alien > and inhuman shapes suggestive of false contours, impossible on a human > being, shedding these cloths that embody and implicitly, with their > gentle all-embracing embrace, imprison -- for adulthood can't escape its > shallow window dressing, the prison it's made for itself out of all the > needless junk of the yonder year, of random fragments of speech that > were never meant to mean much which stuck for some random reason to the > mind of an impressionable child, many decades ago, this impossibility, > of escaping these thing, manifest in the very need to attempt to do so > at all -- in them all that is grown-up, all the unsaid rules, about who > can wear this, who can wear that, about what can't be even mentioned and > must be alluded to in hushed voices filled with intimate secrets (or a > promise of an intimate secret, one day, or perhaps of disappointment, > once you get old enough to know about these thing) their peddler doesn't > even know they harbour, hushes from the abyss of memory so profound it > eludes the photoalbum residing instead in the irrational fear you have > of bees, the feeling of happiness the smell of butter in the morning > (but never at any other time) inexplicably brings to your little > brother, residing deep in the farthest recesses of their mind and > memories, in the most foldy of the folds of their neocortex folds, > inherited and passed through a nondescript chain of innumerable > nondescript ancestor, all of them who were equally bewildered by the > idea of hidden revelations, promised, but never, even when they get old > enough, revealed, the shared notion they should have figured it all out > on their own already making it impossible to ask, these hinted at > secrets that make them adult, make them special, make them capable of > making decisions for others, for taking responsibility, passed through > an equally hushed hint that this is not the done thing, this is the way > of man, this the way of woman, communicated steganographically by way of > an unenthusiastic, lukewarm compliment on a drawing or winning the > cricket match, words exchanged when they don't think you can hear, a > gesture that goes unnoticed by everyone else but means the worlds, > whispers that clumsily yet so effectively point at the unsaid and > unutterable truth, the truth of a life that's your not of your own > making, that you can't make your life in your image, as we all wish -- > and think true -- when we're children, that we must live a life > governed, shaped, molded, put in perspective -- a silly, tragically > ill-headed putting this, since there's no perspective for life, or, > rather, there are an indefinite number of perspectives, and no absolute > notion of a valid perspective, since like is both great, little, and > neither of these things, and is made of the unthinkable eons of > cosmological evolution, in as great degree as it is made of the > intoxicating feeling of kissing the one you love for the first time > (going for sleep for an extended period also gives one an intoxicated > feeling, and a tendency to ramble, but is not anywhere as pleasant, > which is why I don't really recommend it for anyone), and tasting a > faint smell of tobacco and tooth-paste in the kiss, happy in the > knowledge there's nothing essentially different to what the other person > is tasting, happy in the knowledge that in this most banal, common, > usual, everyday act there's no difference between its occurrences if we > look at it from afar, but a whole veritable world of difference, a world > to learn, a world to enter into, not as a conqueror, but as an invited > guest, happy in all this when it's you who's kissing -- with the > horrible, clinical, sterile idea of doing good, in the exact way your > parents understood it, which, for all their rebellion, got from their > parents, save for adding some inchoate bits of "No!" into it whenever > they were too badly burned, correcting some details got wrong (or not, > depending on how accurate your parents' recollection is), some peculiar > folk ways, family traditions associated in the mind of your mother with > an unkindly aunt, a trait of manliness someone tried forcefully to > instill in your father, some inessential detail of credo omitted so as > to not repeat the parental sins of generations before, leading to > heartfelt abstract promises which never effect anything but an > unnecessary pointless feeling of vague guilt, that so often get in the > way of pure linguistic joy, in our contrived, constricted, daily > routine, routine of going through the motions with no real feeling, with > no sense of being actually alive, with the eerie and derealizing > sensation, something you can't quite put you're finger on but which you > also can't shrug off, that sensation of not being there, in the here, > the sensation of actually being there, in the present, in all your > bodily, social, personal glory, all this glory that is you, that > consists in, that is somehow conjured out of failures, silliness, > greatness, having farted at an inappropriate time, saying all you really > think about someone without realizing they're withing hearing range, > realizing there's nothing more to your life than this and being happy > about it, of just, this one time, getting shitfaced instead of retiring > to bed at 11pm when you said you would, and as everyone thinks you do > every night, night after night, on and on, of all that, to just them > giving this task of making some sense of the preceding sentence at a > glance, which surely is their Chomskyan right and wont, a try. (You can > recurse if you wish)) > > > I don't have to bring in metatheory. Why do I have to bring in > > metatheory to prove a Z-R theorem (ie "PA is consistent") in Z-R. I am > > not doing logic at this point, I am just proving a theorem in Z-R. > > It's just a pointless piece of jargon, liable to cause confusion in the > mind of those who are not familiar with it. When in logic we talk of > "metatheory" we have nothing in more mind than the mathematical concepts > and principles that go into our reasoning about whatever mathematically > defined theory we're studying. When this reasoning is formalized in a > formal theory, "metatheory" refers simply to the formal theory in which > we're carrying out the reasoning about the theory we're reasoning > about. And, to add to the confusion, it might well be this theory, in > which we formally reason, is the very theory we're reasoning about. The > term "metatheory" is a purely relative, descriptive term, applying to > one theory in relation to another. This term, alas, is encumbered with > all sorts of unnecessary (and easily avoidable -- by eschewing this > terminology altogether, to name one easy device) philosophical baggage > that befuddles logically innocent. (Since I've got an excuse at this > hour, let me mention that set theorists going about "equiconsistency" > results is an equally inexcusable phenomenon. Some more lack of sleep > will no doubt have me going at Greenian lengths about the evil of this > terminological ill... ILLLLLL!!!! DUMBASS!!! Oh, sorry.) > > For an analogy, suppose comparative literature types went about how > Kundera's _Testaments Betrayed_ was a metabook about books whose > authors, before their death -- which is usually when authors put forth > demands about what should be done about this and that after their death > -- demanded they be burned (the books, not the authors). This would > strike anyone as a peculiar usage, unless it was explained that a > "metabook" simply means a book that is, in part, about books. After it > was explained that comparative literature people are out of their minds > and have introduced a special technical term to refer to books that > mention other books all would be explained, and it might happen that > their perverse nature had led the comparative literature researchers to > introduce yet another technical term, "objectbook", to refer to a book > that is discussed in some other book. Obviously, whether a book is a > "metabook" or an "objectbook" depends on which two books we're thinking > of. Kundera's _Testaments Betrayed_ is a metabook, with certain of > Kafka's writings as its objectbook, among other texts, but it is also an > objectbook, namely of Liisa Saariluomas metabook _Milan Kundera -- > Viimeinen Modernisti_ (a scholarly look at Kundera's oeuvre by a notable > Finnish scholar) which, if we carry out this terminological analogy to > absurd lengths, is also a metametabook to a metabook, which is also one > of its objectbooks, viz Kundera's metabook in which he discusses Kafka's > objectbook (in so far as we take, say, Kafka's _Amerika_ to be a book.) > This analogy, I hope, illustrates, in its flagrant pointlessness, in its > small way, the pointlessness of the meta-this-meta-that talk in > mathematical logic some people cling to with fetishist -- I'm not sure, > but my sense of English tells me "fetishist" is a perfectly fine > adjective, which although I readily admit I could be mistaken about I > hope I'm not, since my sense of English also tells me that both > "finitist" and "finitistic" and "predicativist" and "predicatisitic" are > in free variation, and if I'm mistaken about that there's something > seriously wrong with my sense of English and I'll have to rewrite most > of what I've written on these subjects, which, since there's loads of it > available on Google, won't be a trivial task-- fervour. Sometimes we > need these distinctions in order to be clear, although even in such > situations it's probably better simply to explain we're talking about > what's provable about Q in T, what can be expressed in Q about T; most > of the time they're nothing but a ritualistic remnant, a stale leftover, > a vestigial philosophical organ from a bygone age. > > > I was being informal. At this point of the discussion, I don't even want > > to bring in any discussion of "model" or "true" of "false". > > Well, your statement was perfectly fine. MoeBlee was overly cautious, > though perhaps for all the right reasons. There's nothing wrong in > saying > > It's false that P. > > to mean not-P. He was just alerting you, in his inimitable way, to the > possibility that when we're discussing the truth and falsity of this and > that in a model, a use of the word "true" or "false" in a different > sense, even a very usual and commonly used sense, might confuse the poor > reader. I don't share his opinion that this is a good reason to avoid > these locutions. Rather, I think that in a logic text it's a good idea > to stress that "P is true" and P are exactly equivalent, in so far as > any mathematical considerations extend. This, it is also to be stressed, > in contrast to such expressions as "P is true in the model M" etc. Alas, > while I'm quite sure in this belief of mine, I can't back it up with any > substantial expertise in logical pedagogy, just a few personal anecdotes > from my years in news, and my encounters with people perplexed by logic > in other contexts. Take it, I advise you in light of this, with a > mouthful of grains of sands, then, which is an exercise, this filling > your oral cavity with pebbles of rather small size, that will in any > case improve your oratory skills -- not that there's any pressing call > for such an improvement, what with your skills being so fine and swell > already. > > > Just like we define x to be an even number when there is some y such > > that x = 2 * y, don't we have to define P to be a negative statement > > where there is some Q such that P = not Q? Otherwise, wffs are just > > opaque sets. > > Right. We have exciting definitions like > > o P is a negation if there is a (set theoretic code for a) formula Q > such that P can be obtained by applying whatever set theoretic > construction we've arbitrarily chosen to play the role of the > sentential negation operator, to P, yielding Q. > > spelled out in full gory in the language of set theory, for Charlie-Boo > to marvel at. He will soon adapt BCL to spout an endless stream of such > definitions! Thus axiomatizing, he will be, flouting his defiance in the > face of the logical establishment, for all hoi polloi, in the form of > meaningless strings of symbols, some of which are, as he will explain, > to be taken to stand for this and that, and sometimes also those things > there, all of the dreary business of tediously detailed formal pedantry > of no possible mathematical interest, saving us all the trouble when the > next Charlie arrives on sci.logic, fresh, armed with an inscrutable > forge to crank out formulas, as well as his unwavering conviction he's > right and his formalism is the bee's knees unswayed by any argument or > explanation, steadfastly, with dogged determination, telling it's all a > big lie, a swindle credulous idiots have been taken by! It is a day to > look forward to, in all likelihood with the odd, depressed, even > desperate, and forced sort of optimism people who claim to think > positive, for reasons ineffable and unfathomable, so often unwittingly > affect. > > > But, I am not asking whether this is a viable approach. I am asking if > > this is what you are doing. I understand that you will introduce > > "model theory" to wrap up the proof. But, I am taking this > > introduction of "model theory" to be similar to the introduction of > > "complex number theory" to wrap up a proof in basic number theory (eg, > > proving Fermat's last theorem). > > I have already posted an outline of a proof where we need not invoke any > model theory, indeed nothing beyond basic properties of naturals and an > elementary infinitary inductive definition, stuff probably transparent > to anyone who's ever seen any inductive definitions in mathematics. I am not seeking alternative proofs: I want to understand the proof that Moeblee had in mind. I think my confusion rested in the belief that "model theory" was not a part of ZFC. I think that you and Moeblee are telling me that "model theory" is a part of ZFC, and thus when "model theory" proves that "PA is consistent", then of course the proof is within ZFC (or even Z-R), as the title of this thread claims. I thought that you were just claiming that "model theory" could be cast into the framework of Z-R to answer affirmatively the question that Charlie Boo posed about whether or not ZFC (or Z-R) could prove "PA is consistent". I think I see now that there is no casting to be done: everything is happening in ZFC (or Z-R) even before Charlie Boo asked his question. > Only > an overexposure to formalities, or a bent mind -- not that that's > necessarily a bad thing, as evidenced by such bent people as Brouwer, > Girard, Kripke, Solovay, Cohen -- or possibly an interest in obscure > philosophical matters so erudite as to be completely unintelligible to > the mathematician in the street -- which also is not necessarily not a > bad thing, as we find in the writings of Kreisel, Torkel, Feferman, who > not, what have you, etc -- can possibly lead one to doubt the > legitimacy, correctness, evidence, sureness, of such mathematical > constructions and see-for-yourself proofs thereof.
From: Nam Nguyen on 5 Jul 2010 23:49 Nam Nguyen wrote: > Aatu Koskensilta wrote: > >> William Hale <hale(a)tulane.edu> writes: >> >>> But, I am not asking whether this is a viable approach. I am asking if >>> this is what you are doing. I understand that you will introduce >>> "model theory" to wrap up the proof. But, I am taking this >>> introduction of "model theory" to be similar to the introduction of >>> "complex number theory" to wrap up a proof in basic number theory (eg, >>> proving Fermat's last theorem). >> >> I have already posted an outline of a proof where we need not invoke any >> model theory, indeed nothing beyond basic properties of naturals and an >> elementary infinitary inductive definition, stuff probably transparent >> to anyone who's ever seen any inductive definitions in mathematics. > > The unfortunate thing for us, however, is that "basic properties" of > the natural numbers have dual faces: one can also express the fundamental > theorem of arithmetic _without_ induction at all! > >> Only an overexposure to formalities, or a bent mind -- not that that's >> necessarily a bad thing >> -- can possibly lead one to doubt the >> legitimacy, correctness, evidence, sureness, of such mathematical >> constructions and see-for-yourself proofs thereof. > > > Difficulties in sciences in general were often marked by seemingly > contrasting realities: the relativity vs the absoluteness of the speed, > of light, the clock-work universe vs Heisenberg's Uncertainty, the > wave vs particle duality of photons, etc... And in those difficult > times of knowledge, _only non-bias reconciliation of concepts_ would > prevail! > > Today we're facing the same kind of difficulty in FOL reasoning: the > seemingly irreconcilable induction nature of pCG expression, and the > non-induction counterpart of cGC. > > If, in the name of familiarity of "ordinary" mathematics, we _discard_ > one of them (the later) so that our reasoning life be somehow less > "burdened" then we have indeed failed what is the spirit of mathematics > and mathematical reasoning! Both then are condemned to the sorrow state > of eternal stagnation! Not to mention that we would, in such case, brainwash our future generations to what we today _believe_ as "ordinary", "self-evident",... and rob them of the ability to discover for themselves what the natural numbers might be. Or NOT be.
From: MoeBlee on 6 Jul 2010 12:20
William, I have some tough deadlines this week and next, so I can only give you brief, hasty, and sometimes only rough and approximate answers. On Jul 5, 4:58 pm, William Hale <h...(a)tulane.edu> wrote: > In article > <0d269069-0f3d-46d1-b228-94763c248...(a)i28g2000yqa.googlegroups.com>, > MoeBlee <jazzm...(a)hotmail.com> wrote: > > On Jul 5, 11:58 am, William Hale <h...(a)tulane.edu> wrote: > > > In article > > > <c0b94c40-c6c0-4edf-916d-7fc31f249...(a)x27g2000yqb.googlegroups.com>, > > > MoeBlee <jazzm...(a)hotmail.com> wrote: > > Yes, indeed. But to be clear, the symbols of OBJECT languages (such as > > PA) discussed "IN" Z-R are sets. But, also to make Z-R itself a formal > > theory (and with the symbols of Z-R being sets) we have a meta-theory > > for Z-R (usually, to start, the meta-theory for Z-R is an informal > > meta-theory). > > I don't understand why you are mentioning this. Then skip it for now. It's an ancillary matter. It's not necessary for the immediate proof in this thread. > This is where I (and I > believe Charlie Boo) Let's leave Charlie-Boo out of this, okay? Trying to figure out why Charlie-Boo believes this or that is worse than a "Where's Waldo?" puzzle. > > > > Z-R theorem: There does not exist a formula P such that both P and ~P > > > > are in PA. (Remember, PA IS the set of theorems, in the language, from > > > > a certain set of axioms). > > > > > > I see that I need a Z-R function that takes wffs x and y and maps it to > > > > > a wff that represents "x and y". Like, I need a Z-R function that takes > > > > > a wff x and maps it to a wff that represents "not x". I believe that > > > > > these things can be done in Z-R. > > > > > Forget about that. It's not the way it works. > > > > I don't won't to forget about it. > > > Sorry, but I can't make sense of it, and I don't see what it has to do > > with my proof. > > Just like we define x to be an even number when there is some y such > that x = 2 * y, don't we have to define P to be a negative statement > where there is some Q such that P = not Q? Otherwise, wffs are just > opaque sets. Maybe I understand what you're driving at. Perhaps it is this: We need to say that the way we set up our language, the "~" symbol works in a certain way so that it provides what we actually mean by 'negation'. Well, yes, we do that both in regards syntax and semantics. > I am taking this introduction of > "model theory" to be similar to the introduction of "complex number > theory" to wrap up a proof in basic number theory Okay, let me sort that out: It seems to me that the heart of your question is to distinguish between two things: (1) A Z-R proof of the consistency of PA, in which Z-R proof we refer only to syntactical aspects of PA (its language syntax and proof syntax) (2) A Z-R proof of the consistency of PA, in which Z-R proof we refer not only to syntactical aspects of PA but also to semantical aspects of PA (models). The answer is that in my proof here, I use also semantical aspects of PA. Remember, my only claim about this particular proof is that Z-R proves the consistency of PA. And in Z-R we may formulate semantics for PA. Also, there are theorems that related syntax of PA and semantics for PA (particluarly, if PA has a model (a semantical aspect) then PA is consistent (a syntactical aspect), and so by proving something about semantical aspects of PA (viz. that PA has a model) we also may prove the syntactical matter that PA is consistent. As to whether there is a Z-R proof of the consistency of PA that does not involves semantics, I don't wish to say, since there may arise technicalities in that matter in which I am not sure-footed (however, you may refer to the literature where you will find such things as Gentzen's proof and you can decide for yourself whether it meets your criteria). > > However, for FIRST order, you could define 'theory' without models by > > instead of using entailment use derivability. > > Yes, I am using derivability. But I am not. Enderton is not. > So, am I going doing the wrong road to > understand your proof? Do I need to use and understand "entailment"? Yes, you need to understand entailment. > And, as you point out, I would then need to know and understand "model" > since "entailment" is defined in terms of "model"? Yes, you must understand the basics of models in order to understand my proof. MoeBlee |