details re Z-R |- PA consistent
in [Math]
|
From: Nam Nguyen on 5 Jul 2010 16:54 Nam Nguyen wrote: > MoeBlee wrote: >> On Jul 5, 1:46 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: >>> MoeBlee wrote: >>>> On Jul 5, 1:14 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: >>>>> MoeBlee wrote: >>>>>> On Jul 5, 11:52 am, Nam Nguyen <namducngu...(a)shaw.ca> wrote: >>>>>>> Well, then, PA is consistent can be proven in T = {(x=x) /\ ~(x=x)}, >>>>>> Sure, but with the one technical quibble that the language for T >>>>>> provides a formulation of "PA is not consistent". But, yes, on the >>>>>> basic point, we agree. >>>>>>> which I did mention already. That should settle the issue of formal >>>>>>> proof of PA's consistency! Why bother with any thing as complicated >>>>>>> as Z-R or ZFC, or what have we? >>>>>> Exactly! I mean that NOT sarcastically. This is part of what we've >>>>>> been saying ALL ALONG (in other threads, in various books, especially >>>>>> as well explained in Franzen's incompleteness book). >>>>> So OK then. Do you now agree with me that: >>>>> [...] there's no formal proof that PA is >>>>> consistent in a consistent theory (formal system)? >>>>> A clear answer and that would settle the discussion here. >>>> I GAVE YOU a clear answer to that question in some detail in another >>>> thread. My answer does not take the form yes/no, for the reasons that >>>> can be seen in my fuller answer. Also, I just remarked in that thread >>>> that I'm not interested in responding to you in the manner of a >>>> deposition. I'm not going to give you bare "Yes"/"No" answers that >>>> require elaboration as to the actual sense and framework of the >>>> question. >>> That's why our discussion in this thread (at least) goes around >>> and around, despite _your and mine_ wishes to the contrary: you simply >>> refused to answer direct to the point important but very easy to >>> understand question. (Btw, I already mentioned "I don't know" is >>> a valid question too!) >> >> We're done, Nam. > > If you say so (without giving an clear cut answer, even the framework, > you had sought for clarification, was confirmed to you)! > > I've done my best to encourage a spirited discussion on foundational > problems! I might have meant "fruitful/result-oriented" instead of "spirited".
From: William Hale on 5 Jul 2010 17:58 In article <0d269069-0f3d-46d1-b228-94763c248f00(a)i28g2000yqa.googlegroups.com>, MoeBlee <jazzmobe(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: > > > Hi William, > > > > > First a note: Just to be clear, when I listed certain symbols in my > > > post, I mean that those are AMONG the symbols of those languages; It > > > is not to be construed that those lists exhaust the symbols of those > > > languages. > > > > > Some items from your post: > > > > > > One subgoal is to define a set in Z-R that represents the wffs of PA. > > > > > Or, we can be more definite and say not just that we find a set to > > > "represent" PA, but rather we actually define a specific set that IS > > > PA. > > > > Yes, I meant that. > > > > > > > > > > We > > > > must first agree on an alphabet of characters that we will use in these > > > > wffs. > > > > > Yes, except I say 'symbols'. At least in my view, the particular > > > typographic shapes we use merely indicate the actual symbols, as the > > > symbols themselves are abstract set-theoretic objects. (See Enderton's > > > remarks on what symbols are, as I adopt one of the options he allows.) > > > > I am not talking about the physical or typographic shapes of symbols. > > Just like we say the natural number 0 corresponds to the set {}, > > I wish to be pedantic in some of these matters, since we are in an > area of fine-grained analysis. > > So, in Z-R, the natural number 0 IS the empty set. (Not just > corresponds to the empty set.) Yes, I agree. Let me give an analogy for you to see my viewpoint. It is well-known that in Euclidean geometry you can define a collection of Euclidean things to correspond to things in a non-Euclidean geometry. One could drop this correspondence idea and say that this collection of Euclidean things IS the things in a non-Euclidean geometry. One then could say that a mathematician proving theorems of non-Euclidean geometry is working in Euclidean geometry. But, I wouldn't want to say that because I think that puts non-Euclidean geometry as a second citizen, below Euclidean geometry. I would rather say that Euclidean geometry and non-Euclidean geometry are on equal footing, each with their own set of axioms. I am not worried about consistency or relative consistency: I want to do geometry, not logic. I cannot do the same thing with PA and ZFC as regards natural numbers N. I cannot prove the theorems of number theory by working in PA. I can prove some theorems in PA, but not all the ones I want. Thus, I bite the bullet and work in the theory (ZFC theory) where I can prove the theorems that I want to prove. Thus, I want to say that the natural numbers N IS something in ZFC, rather than saying that the natural numbers (as given by PA) corresponds to something in ZFC. 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). In particular, I disagree with the title of the thread "How can ZFC/PA do much of Math - It can't even prove PA is consistent". I don't think that the claim that ZFC is the foundation of standard mathematics includes proving PA is consistent. I don't require that logicians work in ZFC. I think that is an artificial requirement. However, I understand that you are claiming that it can be done, and I am trying to understand the outline of doing what is claimed in ZFC. My biggest obstacle is that I currently view "model theory" as a metatheory (with the little I know about "model theory"). This view is what I am trying to change. In summary, I am thus willing to say "IS" rather than "correspond". > > > I want > > to say the char 'i' corresponds to the set 105 and the char 'f' > > corresponds to the set 102 > > I'd put it even STRONGER. > > But, first, I'm going to move past characters, and talk instead about > symbols. Second, I'm going to go past "corresponds" and talk instead > about "IS". > > We may (emphasis on 'may') elect to take the symbols of the language > to BE natural numbers (and I'm not conflating with Godel numbering, > though that too is consistent with what I'm saying here). I want the symbols to be sets in ZFC. Of course, they need not be natural numbers (that are defined in ZFC). Also, I am trying to side-step the notion of symbol (which seems to denote a glyph), and not worry to much about whether I write "->" or "implies" or "if ... then ....". I think we have agreed that whatever the PA symbols, wffs, proofs, etc are in Z-R, they are at bottom just sets. That was the only point I was trying to make. > > > and the symbol "if" corresponds to the > > function {<0,105>, <1,102>}, etc. > > You might set up all kinds of ways. Personally, I take the symbol > indicated by '->' (for simplicity, I'll just say "the '->' symbol") to > be a natural number. In my own treatment (and the specifics of the > proof in this thread don't depend on such particulars), I take the > symbols to be natural numbers (and I work it out so that what KIND of > symbol is from a DECIDABLE subset of the set of natural numbers), then > I take expressions to be finite sequences of symbols, then wffs to be > a special kind of expression. > > > > Without going into details, I just > > wanted to confirm that symbols, wffs, etc are really just sets in Z-R. > > 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. This is where I (and I believe Charlie Boo) are losing track of what is being discussed. I don't want any mention of metatheory at this point. If I want to prove a theorem in number theory, 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. > > > > The symbols for set theory are the logical symbols (the quantifier, > > > connectives), the variables (denumerably many), and the predicate > > > symbols ('=' and 'e' (for 'e' read as the epsilon symbol)). > > > > That is given. But, that does not say what the symbols of PA in Z-R are. > > In fact, I am saying that the symbols of PA in Z-R must be sets. The > > symbol 'e' is not a set. > > Right. And I'm a bit guilty of having gone off as to what the symbols > of Z-R are, when the more pressing matter for our purposes here is > what the symbols of PA are. Indeed, in this analysis, the symbols of > PA are themselves sets. > > > > > Let say we stipulate an alphabet of 255 characters (probably 50 > > > > would suffice). > > > > > Actually, we have denumerably (countably infinite) many symbols., as I > > > mentioned above. > > > > But, those symbols in Z-R are not the symbols in what we want to call PA > > in Z-R. > > Sorry, right. But, still, there are denumerably many symbols for the > langauge of PA too, since the language of PA, as any first order > language, has denumerably many variables. > > > > > We associate distinct concrete sets with each of these > > > > 255 characters. For example, we call the set 97 'a', 98 'b', etc > > > > > No, throw that out. It doesn't work that way at all. > > > > If I throw that out, then I will have to go back to square one. Are you > > sure you want me to throw that out? > > I see where I got off your track. I took you too literally. You said > we associate sets with characters. It's the other way around: We > "associate" characters (better, symbols) with sets.So it's not as if > each set has a corresponding symbol, but rather that each symbol has a > corresponding set. But, and I grant this is pedantic, we don't just > associate symbols with sets, rather the symbols ARE sets. I agree. > > > > > > > The set of sentences is a proper subset of the set of wffs. The > > > sentences are the wffs that have no free variables. > > > > I was trying to be precise. I am taking sentences to be strings like > > "===Sx Syy z zz" (that is, any list of characters to be used in our PA > > within Z-R). > > In, say, Enderton's terminology, the set of strings on the alphabet is > the set of expressions. Then there is a proper subset of the set of > expressions that is the set of wffs. Then there is a proper subset of > the set of wffs that is the set of sentences. > > Note: For certain technical reasons, my treatment is different from > Enderton's in one respect: He takes expressions to be n-tuples of > symbols, while I take expressions to be actual sequences (actual > functions). > > se that there is some wff p in PA_Wffs such that (p > > > > and not p) is an element of PA_Theorems. > > > > > Since we have a more exact notion of falsehood in play in the proof, > > > just to be very clear, let's leave out the word 'false' in this > > > particular place. > > > > But, this is exactly one of the points that I am not clear about. The > > "false" that I am using here is a Z-R terminology, not something about > > what we are doing for PA within Z-R. > > > > I could say: > > > > Theorem 1. It is false that {} in {}. > > That's only okay informally. To be more correct: > > Theorem 1: { } not in { }. > > Leave the words 'true' and 'false' out of the Z-R theorems unless we > are talking about actual formal model theoretic truth and falsehood, > and where we're taking Z-R as a meta-theory to talk about truth or > falsehood in models for object languages. 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". > > > By that I mean: > > > > Theorem 1. not ( {} in {} ) > > Sure, and informally that's fine. But, since we're also getting into > formal truth and falsehood per models, it's better to keep to the > pure: > > Theorem 1: not { } in { } > or > Theorem 1: ~ 0e0 > or, even more pedantically (though not necessary to be so pedantic): > Theorem 1: ~e00 > > > Again, I am not trying to be precise. But, in Z-R, I don't have any > > concept or definition of what "true" or "false" is. Do I need to > > introduce these concepts at square one? I haven't even mentioned > > anything about proving anything consistent or not. I am just working > > with sets, whether one set is an element of another set. > > No, let's put aside for the time being 'true' and 'false' for Z-R. > (But we will talk, IN Z-R about 'true' and 'false' for PA.) So, in > this context, as to Z-R, lets just talk about its THEOREMS and Z-R > proofs of theorems. (Later, we will say that every theorem of Z-R is > true in every model of Z-R. But we don't need that for the purpose of > this thread.) > > > > 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. > > Meanwhile, if you are using it to make sense for yourself of > something, then I very strongly recommend seeing how Enderton develops > things in his book; I think that will provide you the context to make > sense better. > > > > The overall plan is this (all in Z-R): > > > > > We define 'model of a theory'. > > > > This is exactly one of the points I am trying to figure out. > > See Enderton's mathematical logic book. He explains it beautifully. > > > I was > > hoping to do a portion of the setup of stating and proving PA consistent > > in the framework of Z-R. > > Yes, in Z-R, we do not just a portion, but the whole thing. I understand, but I want to do just the beginning. If I am way off, then there is no need to proceed along the wrong path. In fact, I am not even beginning at the beginning. I want to concentrate on a particular set of Z-R that is the set of all (valid) proofs of PA. I gave an outline of how that set might be defined in Z-R. Then, my claim was that it is enough to show that there is no element of that set whose final wff is of the form "P and not P". You changed this to it is enough to show that there are no elements proof1 and proof2 of that set such that the last wff of proof1 is P and the last wff of proof2 is "not P", for some wff P. That's ok with me also. 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). That is, Fermat's last theorem can be stated in elementary terms, but the proof is based on machinery of complex analysis which is developed in ZFC. In particular, we have to show that the integers are ring isomorphic to a subring of the complex numbers so that the original theorem in "integers" remains true in "complex numbers". I suspect something like that will happen when you introduce model theory. But, I am not at that point yet to discuss model theory. However, if my formulation of what we are trying to prove in Z-R that "PA is consistent" is not related at all to how the proof will unfold in your development, then I need to go back to square one. In other words, do I need to know model theory just to state what I am trying to prove in Z-R that PA is consistent? > > > In your terminology, I was trying to set up the apparatus to define what > > a 'theory' is as an object in Z-R. > > Right. We do that. > > > I was hoping that "model" would not be needed up to that point. > > Actually, the way Enderton does it, we need structures (models) for a > language to define 'theory', since we define a theory in terms of > entailment while entailment is defined in terms of models. > > However, for FIRST order, you could define 'theory' without models by > instead of using entailment use derivability. Yes, I am using derivability. So, am I going doing the wrong road to understand your proof? Do I need to use and understand "entailment"? And, as you point out, I would then need to know and understand "model" since "entailment" is defined in terms of "model"? > > > For example, with the set up that I presented, couldn't I prove in Z-R > > that there is no proof of less that 100 symbols that would prove a > > contradiction "P and ~P" for some wff P? That is, I just enumerate the > > 255^100 proofs, select the proofs composed of wff sentences, filter out > > the invalid proofs, and see if any of the valid proofs of what remains > > has a last sentence of the form �"P and ~P"? > > Yes. But let's not say 'invalid proof'. Instead say 'sequence not a > proof' (or something else other than 'invalid proof' which is > terminology that tends to confuse certain things). > > MoeBlee
From: RussellE on 5 Jul 2010 18:48 On Jul 5, 10:47 am, MoeBlee <jazzm...(a)hotmail.com> wrote: Thanks for providing such a detailed explaination. > The overall plan is this (all in Z-R): > > We define 'model of a theory'. Very roughly, a model of a theory T is > a model FOR the language of T such that every member of T is mapped to > the value 1 (1 for true, 0 for false) by a function that maps all > sentences of the language of T to either 0 or 1 and as stipulated by > the ordinary "Tarski method". Doesn't this mean the model is complete? "All sentences" means any wff? > We also prove (trivially) that if a theory has a model then the theory > is consistent. By definition of the model. The model is complete (and non-empty) by definition. > We also prove (quite trivially) that if all the axioms of a theory are > true in a given model then that model is a model of the theory that is > the entailment-closure of those axioms. (And PA is the entailment- > closure of a certain set of axioms.) "Entailment-closure" is the part that bothers me. > Then we construct a specific model for the language of PA and show > that that model is model of PA. We show that by showing that all the > axioms of PA are true in said model. Consider two sentences: 1) It is false that there is some wff p in PA_Wffs such that (p and not p) is an element of PA_Theorems. 2) It is true that there is some wff p in PA_Wffs such that (p and not p) is an element of PA_Theorems. If statement (1) is true, the model must include (1). If statement (2) is true, the "model" must include both statements (1) and (2). Either way, statement (1) is part of the model. Proving (1) says nothing about the consistency of the the theory. Assume the theory is incomplete. Now, it is possible statement (2) is true, but unprovable. Even if an incomplete theory proves its own consistency, it is still possible the theory is inconsistent. Russell - 2 many 2 count
From: Aatu Koskensilta on 5 Jul 2010 21:47 (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. ? 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 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. > 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. 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. 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. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: herbzet on 5 Jul 2010 22:10
Aatu Koskensilta wrote: > > (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. > > ? 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 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. > > > 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. 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. 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. 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 ... -- hz |