Aatu Koskensilta wrote: > On 2008-01-26, in sci.logic, Nam D. Nguyen wrote: >> What about the knowledge of arithmetic? or the assumption of omega-consistency? >> Aren't these of "non-finitistic" reasoning? Perhaps there is a sense of imperfection >> in your use of "perfectly [innocuous]" here?
> What do you mean by "the knowledge of arithmetic"?
Wonder why you asked me this very trivial question! To understand "the knowledge of X" one of course should understand what X is. Then (in the other thread) what did you mean by "arithmetic", as in "Henry Flynt's tirades against _arithmetic_, for example, are quite perplexing in a delightfully bizarre way..."
> As to omega-consistency, it is a finitistically meaningful property of > formal theories. Of course, that this or that formal theory is > omega-consistent is not necessarily finitistically provable -- in > particular that Peano arithmetic, ZFC and so on are omega-consistent > is not finitistically provable -- > but happily no such assumptions are > used in the proof of the incompleteness theorem.
Are you sure that in Gödel's, as you put it, "original article" he never stipulated the assumption of omega-consistency, or the like?
Pierre Asselin wrote: > Nam D. Nguyen <namducngu...@shaw.ca> wrote:
>> What about the knowledge of arithmetic? or the assumption of omega-consistency? >> Aren't these of "non-finitistic" reasoning? Perhaps there is a sense of imperfection >> in your use of "perfectly [innocuous]" here?
> If omega-consistency bothers you, Rosser weakened the hypothesis to just > consistency. Any objections to consistency?
Why did you think I was bothered with the omega-consistency (or any consistency) in my response to AK? My argument here is there are technical reasons to think his "perfectly innocuous" is not perfect (i.e. not quite correct)! That's all.
> Wonder why you asked me this very trivial question!
I was wondering what you had in mind in bringing in "knowledge of arithmetic" in connexion to your doubts as to the finitary nature of Godel's proofs. It's obscure what you have in mind here. That a proof is finitary simply means that no essential reference is made to any infinitary objects, such as infinite sets, infinite trees, and the like, and that only basic principles concerning finitary objects are used. In particular, Godel's theorems are provable in primitive recursive arithmetic, and even weaker fragments of finitistic arithmetic.
> Then (in the other thread) what did you mean by "arithmetic", as in > "Henry Flynt's tirades against _arithmetic_, for example, are quite > perplexing in a delightfully bizarre way..."
Elementary arithmetic, as we find formalised in e.g. Peano arithmetic or some subtheory thereof.
> Are you sure that in Gödel's, as you put it, "original article" > he never stipulated the assumption of omega-consistency, or the like?
His result is that whenever a system is primitive recursively axiomatised and capable of representing all primitive recursive functions, it will have undecidable statements provided it is omega-consistent. Naturally in a proof of such a conditional statement we introduce the assumption that the system in question is omega-consistent, and on that basis argue that it must contain undecidable statements, finally discharging the assumption in order to arrive at the hypothetical conclusion: if the system is omega-consistent, it contains undecidable statements.
On Jan 28, 3:13 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi> wrote:
> On 2008-01-27, in sci.logic, Nam D. Nguyen wrote:
> > Wonder why you asked me this very trivial question!
> I was wondering what you had in mind in bringing in "knowledge of > arithmetic" in connexion to your doubts as to the finitary nature of > Godel's proofs. It's obscure what you have in mind here. That a proof > is finitary simply means that no essential reference is made to any > infinitary objects, such as infinite sets, infinite trees, and the > like, and that only basic principles concerning finitary objects are > used. In particular, Godel's theorems are provable in primitive > recursive arithmetic, and even weaker fragments of finitistic > arithmetic.
In your own words (stated below) this is what Godel proved:
"...whenever a system is primitive recursively axiomatised and capable of representing all primitive recursive functions, it will have undecidable statements provided it is omega-consistent"
It takes a lot of *coding* to put all of this into primitive recursive arithmetic, which only deals with numbers as objects. Your claim that Godel's proof is finitary is dependent on the fact that the said proof can be encoded into PRA. But I on the other hand, insist that the notion of "all primitive recursive functions" is *essentially* infinitary and *cannot* be encoded via any finitary process into PRA. That is because from my point of view (i.e. the logic NAFL) a function is an essentially infinite object. There is no way to strip functions of this infinite nature and deal only with "uninterpreted" function symbols in NAFL.
This is a fundamental point of departure between NAFL and classical/ intuitionistic logics. No doubt you will assert that you are not interested in NAFL (or that NAFL is of no interest). For the record, I have explained the NAFL position at the end of this post.
> > Then (in the other thread) what did you mean by "arithmetic", as in > > "Henry Flynt's tirades against _arithmetic_, for example, are quite > > perplexing in a delightfully bizarre way..."
> Elementary arithmetic, as we find formalised in e.g. Peano arithmetic > or some subtheory thereof.
> > Are you sure that in Gödel's, as you put it, "original article" > > he never stipulated the assumption of omega-consistency, or the like?
> His result is that whenever a system is primitive recursively > axiomatised and capable of representing all primitive recursive > functions, it will have undecidable statements provided it is > omega-consistent. Naturally in a proof of such a conditional statement > we introduce the assumption that the system in question is > omega-consistent, and on that basis argue that it must contain > undecidable statements, finally discharging the assumption in order to > arrive at the hypothetical conclusion: if the system is > omega-consistent, it contains undecidable statements.
Let us forget omega-consistency and focus on just plain consistency. You would no doubt claim that consistency of a theory like PRA is a finitary notion. In classical/intuitionistic logics, that claim is seemingly justified, for one can make the consistency statement of PRA encode the following sentence:
'There is no proof of the proposition "0=1" in PRA' (1)
But strictly speaking, to show that (1) would entail consistency of PRA, one would have to also use ex falso quodlibet (from a contradiction P&~P, an arbitrary propostion Q can be deduced). For that is the only way in which we can rule out the possibility that PRA proves some other contradiction (say, "1=2"), despite the truth of (1)
So strictly speaking the consistency of PRA *also* requires that the following sentence be proved:
'A proof of any sentence of the form P&~P in PRA implies that every sentence in the language of PRA is deducible in PRA' (2)
I assert that you need to encode (1) and (2) into PRA in order to support your claim that the consistency of PRA is a finitary notion. Which means you basically need the notion of an "arbitrary contradiction" P&~P and also the notion of "every sentence in the language of PRA" to be encoded into *one* sentence in the language of PRA to support your your claim. I assert that any such encoding is an essentially self-referential and from my point of view, infinitary. And that such an encoding is paradoxical is clearly brought out by the fact that classically/intuitionistically there are non-standard models of PRA in which the encoding fails, and in which the consistency sentence of PRA is not really the consistency sentence of PRA, after all.
For the record, let me explain the NAFL postition. In NAFL, ex falso quodlibet fails ( because the assertion that ~P&(PvQ)-->Q is not a theorem of a NAFL theory T in which P is undecidable in T; the law of non-contraction fails in NAFL). Nevertheless, while the NAFL theory T can have a non-classical model in which P&~P is the case, consistency of T still demands that P&~P be unprovable in T (unlike paraconsistent theories, which do permit P&~P to be provable). So the consistency of T would essentially have to express that "All possible contradictions in the language ot T are not deducible in T". If one calls this sentence Con(T), it cannot possibly be a sentence in the language of T because then Con(T) would have to refer to itself and also its negation (i.e.. we would need to have Con(T) to also encode that "Con(T)&~Con(T) is not provable in T", which is the height of absurdity and not possible in NAFL).
The notion of consitency of a NAFL theory T is still meaningful when looked at metamathematically, but it is not finitary in the sense that this notion is not formalizable within NAFL theories.
Regards, RS
***************************************************************** A function f(x) is *unavoidably* an infinite object in NAFL, wherein a variable x takes on a value when and only when the human mind specifies that value. If the human mind fails to specify any value for x, then x takes on all possible values, which would be a contradiction in classical/intuitionistic logics. But in NAFL (where the law of non- contradiction fails) the meaning of such an infinite superposition of values for x means precisely that the human mind has not assigned any particular value for x. Similarly the function represented by f(x), when x and f(x) have no specific values assigned by the human mind, can be thought of as an infinite class of ordered pairs of the form {(1, f(1)), (2, f(2)), .....}. There is no way to encode an infinite class as a natural number or any other finite object in NAFL. *******************************************************************
On Jan 28, 9:05 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> from my point of view (i.e. the logic NAFL)
It is convenient for you, and inconvenient for anyone else, to say what follows from the point of view of NAFL since you won't specify NAFL with sufficient exactness so that anyone but you can say what follows from its point of view.
But this is not PM. There is a ramification and a predicativity condition missing on a.
Bye
the translation you gave us says
substitution from the axiom schema IV, 1, i.e. from the reducibility axiom
40. reduAxiom(x) ⇔ ∃u,v,y,n ≤ x. vtype(n,v) ∧ vtype(n + 1,u) ∧ ¬free(u,y) ∧ isFm(y)∧ x = exists(u,forall(v,equiv(seq(u) ◦ paren(seq(v)),y))) x is a formula obtained by substitution from the axiom schema IV, 1, i.e. from the reducibility axiom
mine says
This axiom represents the axiom of reducibility (
1. (∃u)(v ∀ (u(v) ≡ a))
on substituting for v or u any variables of types n or n + 1 respectively, and for a a formula which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).
> This axiom represents the axiom of reducibility (
> 1. (â u)(v â (u(v) â ¡ a))
> on substituting for v or u any variables of types n or n + 1 respectively, > and for a a formula which does not contain u free. This axiom represents > the axiom of reducibility (the axiom of comprehension of set theory).
On Jan 28, 10:46 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> On Jan 28, 9:05 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > from my point of view (i.e. the logic NAFL)
> It is convenient for you, and inconvenient for anyone else, to say > what follows from the point of view of NAFL since you won't specify > NAFL with sufficient exactness so that anyone but you can say what > follows from its point of view.
Let me apologize to you for my repeated failures to get started on a new NAFL thread that I had promised. I have explained NAFL in some of my eprints, but it would be easier for you if I were to post the essentials in a sci.logic thread.
I suspect, though, that the kind of exactness you are looking for may not be achievable within NAFL, in the sense that certain notions used in NAFL (like undecidability of propositions in NAFL theories or the consistency of a NAFL theory or the notion of a NAFL theory as an object) cannot be formalized within NAFL theories. They are essentially metamathematical notions. Let me see what you have to say about that when I start the thread.
"The system P of footnote 48a is Godel’s streamlined version of Russell’s theory of types built on the natural numbers as individuals, the system used in [1931]. The last sentence of the footnote allstomindtheotherreferencetosettheoryinthatpaper; KurtGodel[1931,p. 178] wrote of his comprehension axiom IV, foreshadowing his approach to set theory, “This axiom plays the role of [Russell’s] axiom of reducibility (the comprehension axiom of set theory).”
from thwe collected works of godel volume 3 godel states 1939
http://209.85.173.104/search?q=cache:3gSInfW9KDUJ:www.ams.org/notices... "In the 1939 lecture he as-serted that “this fundamental theorem constitutesthe corrected core of the so-called Russellian axiom of reducibility.” Thus, Gödel established anotherconnection between L and Russell’s ramified the-ory of types. But while Russell had to postulate his Axiom of Reducibility for his finite orders, Gödel was able to derive an analogous form for his trans-finite hierarchy, one that asserts that the types are delimited in the hierarchy of orders."
> It takes a lot of *coding* to put all of this into primitive recursive > arithmetic, which only deals with numbers as objects. Your claim that > Godel's proof is finitary is dependent on the fact that the said proof > can be encoded into PRA. But I on the other hand, insist that the > notion of "all primitive recursive functions" is *essentially* > infinitary and *cannot* be encoded via any finitary process into > PRA.
We can just talk about, say, extensions of Q, as outlined by Rupert in an another post. As to all the tedious coding, you'll find the details in any number of texts, such as Girard's _Proof Theory and Logical Complexity_. As to NAFL, of which I'm entirely ignorant, it might or might not be that Godel's proof goes through. That's entirely irrelevant to the observation that Godel's proof is perfectly finitary in the ordinary sense of the word.
> But strictly speaking, to show that (1) would entail consistency of > PRA, one would have to also use ex falso quodlibet (from a > contradiction P&~P, an arbitrary propostion Q can be deduced).
If we define inconsistency as proving every sentence ex falso quadlibet is indeed required. However, as outlined in a post of mine /A recursion theoretic look at incompleteness/ we can formulate the first incompleteness theorem in a 'logic-agnostic' form, making no assumptions about the underlying logic of the theory. The second incompleteness theorem has no such formulation, and does depend on the properties of the rules of inference.
> 'A proof of any sentence of the form P&~P in PRA implies that every > sentence in the language of PRA is deducible in PRA' (2)
That is trivially provable in PRA. However, I wonder why you're talking about PRA here? What was at issue was PRA proving the incompleteness theorems, not what PRA proves of itself. (It does, of course, prove that the incompleteness theorems apply to PRA).
> On Jan 28, 10:46 pm, MoeBlee <jazzm...@hotmail.com> wrote:> On Jan 28, 9:05 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > > from my point of view (i.e. the logic NAFL)
> > It is convenient for you, and inconvenient for anyone else, to say > > what follows from the point of view of NAFL since you won't specify > > NAFL with sufficient exactness so that anyone but you can say what > > follows from its point of view.
> Let me apologize to you for my repeated failures to get started on a > new NAFL thread that I had promised. I have explained NAFL in some of > my eprints, but it would be easier for you if I were to post the > essentials in a sci.logic thread.
> I suspect, though, that the kind of exactness you are looking for may > not be achievable within NAFL, in the sense that certain notions used > in NAFL (like undecidability of propositions in NAFL theories or the > consistency of a NAFL theory or the notion of a NAFL theory as an > object) cannot be formalized within NAFL theories. They are > essentially metamathematical notions. Let me see what you have to say > about that when I start the thread.
Ordinary metamathematical notions can be formalized. That you can't formalize yours is a separate matter. Meanwhile almost all of your remarks in your various posts are based on your continued claim as to the superiority of NAFL and as to what follows from it. But not only do we not have before us a formalization, we don't even have a coherent informal description, so reading your posts I can only shrug to say, "Well, so you say, but you've excluded me from determining for myself since you won't give me the same keys to drive the vehicle that you reserve for yourself." It's actually pretty insulting of you to keep pounding people that they should regard mathematics in the context of your own devising but leave it so that, on account of the utter vagueness of your system, no one but you can say what holds or doesn't in your system and thus, in the context that you maintain that your system should be considered superior, in mathematics in general.
> On 2008-01-28, in sci.logic, R. Srinivasan wrote:
> > It takes a lot of *coding* to put all of this into primitive recursive > > arithmetic, which only deals with numbers as objects. Your claim that > > Godel's proof is finitary is dependent on the fact that the said proof > > can be encoded into PRA. But I on the other hand, insist that the > > notion of "all primitive recursive functions" is *essentially* > > infinitary and *cannot* be encoded via any finitary process into > > PRA.
> We can just talk about, say, extensions of Q, as outlined by Rupert in > an another post. As to all the tedious coding, you'll find the details > in any number of texts, such as Girard's _Proof Theory and Logical > Complexity_. As to NAFL, of which I'm entirely ignorant, it might or > might not be that Godel's proof goes through. That's entirely > irrelevant to the observation that Godel's proof is perfectly finitary > in the ordinary sense of the word.
> > But strictly speaking, to show that (1) would entail consistency of > > PRA, one would have to also use ex falso quodlibet (from a > > contradiction P&~P, an arbitrary propostion Q can be deduced).
> If we define inconsistency as proving every sentence ex falso > quadlibet is indeed required. However, as outlined in a post of mine > /A recursion theoretic look at incompleteness/ we can formulate the > first incompleteness theorem in a 'logic-agnostic' form, making no > assumptions about the underlying logic of the theory. The second > incompleteness theorem has no such formulation, and does depend on the > properties of the rules of inference.
I wish to define consistency of a theory T by the requirement that *every* sentence of the form P&~P (i.e. every contradiction) in the language of T should be unprovable in T. Therefore my definition of inconsistency of T is the provability in T of at least one contradiction. By ex falso quodlibet, the consistency of T can be reduced to the unprovability of a single sentence (say, "0=1") and this is seemingly a finitary concept. What I was trying to get at was that this latter assertion requires ex falso quodlibet if it were to really represent consistency, and that the inference from ex falso quodlibet (that T proves every contradiction in its language if T proves one contradiction) cannot really be expressed finitarily. Please see my comments below.
> > 'A proof of any sentence of the form P&~P in PRA implies that every > > sentence in the language of PRA is deducible in PRA' (2)
> That is trivially provable in PRA. However, I wonder why you're > talking about PRA here? What was at issue was PRA proving the > incompleteness theorems, not what PRA proves of itself. (It does, of > course, prove that the incompleteness theorems apply to PRA).
The reason I am talking about PRA is that it is considered as the formal system that correctly captures finitism. Presumably you are asserting that the reasoning used by Godel is finitary because that reasoning can be formalized within PRA.
Now I do not agree with your assertion that the sentence (2) above is trivially provable *in* PRA. We can indeed infer that PRA will prove every sentence in its language if it proves a contradiction. But that inference is not made *within* PRA, it is a metamathematical fact *about* PRA. For the sentences of PRA are about numbers and no sentence of PRA can ever tell you something about all of its sentences, at least not without the kind of coding employed by Godel.
I was considering the incompleteness theorems as applied to PRA and then formalized within PRA. The point I was trying to make was that with Godel's coding, the consistency sentence of PRA can indeed by encoded as a sentence of PRA (call this con(PRA)). What I was trying to get at was that if Con(PRA) were to really represent the consistency sentence of PRA, it must somehow encode the notion of "all sentences of PRA" and I was disputing the alleged finitary nature of that notion.
If Con(PRA) were to express that "There is no proof of "0=S(0)" in PRA", then it would really express the consistency of PRA only along with an iinference from ex falso quodlibet that all sentences of PRA can be deduced from a contradiction. I am claiming that such an inference has to be metamathematical if one only looks at PRA without any encoding. By the process of encoding, Godel apparently succeeded in representing the consistency of PRA within PRA and I am disputing the alleged finitary nature of such an encoding.
I do see your asserition above that by the standard definition of finitism, Godel's reasoning is indeed finitary..I have also noted from previous positngs of yours that you consider the consequences of Godel's theorems, in particular, the existence of non-standard models of PRA, to also be finitary in nature. I am not really convinced (especially of the latter assertion) but I don't think I can conviince of my viewpoint either.
I have explained the NAFL position in my previous post, and by the NAFL yardstick, the reasoning employed by Godel is not finitary.
On Jan 30, 3:12 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> by the > NAFL yardstick, the reasoning employed by Godel is not finitary.
By the NAFL yardstick, anything can be anything you personally claim it to be, since your lack of specifiying exactly what the NAFL yardstick is leaves you as the only person who can say how to apply it.
> On Jan 28, 10:17 pm, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > On Jan 28, 10:46 pm, MoeBlee <jazzm...@hotmail.com> wrote:> On Jan 28, 9:05 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > > > from my point of view (i.e. the logic NAFL)
> > > It is convenient for you, and inconvenient for anyone else, to say > > > what follows from the point of view of NAFL since you won't specify > > > NAFL with sufficient exactness so that anyone but you can say what > > > follows from its point of view.
> > Let me apologize to you for my repeated failures to get started on a > > new NAFL thread that I had promised. I have explained NAFL in some of > > my eprints, but it would be easier for you if I were to post the > > essentials in a sci.logic thread.
> > I suspect, though, that the kind of exactness you are looking for may > > not be achievable within NAFL, in the sense that certain notions used > > in NAFL (like undecidability of propositions in NAFL theories or the > > consistency of a NAFL theory or the notion of a NAFL theory as an > > object) cannot be formalized within NAFL theories. They are > > essentially metamathematical notions. Let me see what you have to say > > about that when I start the thread.
> Ordinary metamathematical notions can be formalized. That you can't > formalize yours is a separate matter. Meanwhile almost all of your > remarks in your various posts are based on your continued claim as to > the superiority of NAFL and as to what follows from it. But not only > do we not have before us a formalization, we don't even have a > coherent informal description, so reading your posts I can only shrug > to say, "Well, so you say, but you've excluded me from determining for > myself since you won't give me the same keys to drive the vehicle that > you reserve for yourself." It's actually pretty insulting of you to > keep pounding people that they should regard mathematics in the > context of your own devising but leave it so that, on account of the > utter vagueness of your system, no one but you can say what holds or > doesn't in your system and thus, in the context that you maintain that > your system should be considered superior, in mathematics in general.
I see that you are eager to sink your teeth into NAFL. I welcome your interest in scrutinzing NAFL. Please hang around, I will try to start the thread on NAFL in February.
I never claimed that NAFL is "superior" or any such thing. I would just like the rest of the world to acknowledge that NAFL exists. I have explained NAFL in various eprints and also a peer-reviewed conference paper in International Journal of Quantum Information. The essentials of NAFL are not at all difficult to understand, although they may be difficult to accept for someone like you who is classically trained.
As for your assertion that ordinary metamathematical concepts can be formalized, I take the stand that you have to draw the line somewhere and accept that certain concepts cannot be formalized, unless you either accept an infinite regress or circularity. The cruical point is that those concepts that I assert cannot be formalized within NAFL should be clear enough for everybody to accept.
NAFL is actually a bunch of metamatthematical rules that NAFL theories have to satsify. I claim that the metamathematical notions used are indeed clear and acceptable and provide a basis for working within NAFL theoreis. But many of these notions are *about* NAFL theories and cannot be formalized within NAFL theories. The metatheory of NAFL theories will necessarily have unformalized concepts and there is no metatheory of this metatheory.
As I type this post at 6 AM, I have been working all night on a software project. I have to complete this project in about a week's time. Once I am done with that I will have some free time to post the thread on NAFL. I will surely be mentally fatigued, but then I have to accept that the days when I could work full time on whatever I wanted to are now over. IBM is insisting on its pound of flesh and I cannot complain about having to work for a living.
On Jan 30, 4:33 pm, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> I see that you are eager to sink your teeth into NAFL. I welcome your > interest in scrutinzing NAFL. Please hang around, I will try to start > the thread on NAFL in February.
Actually, I'm eager not to be kept on a continual jerk-leash by your continual pronouncements about what NAFL determines as a context for mathematics when you won't give a coherent specification of NAFL so that I can decide for myself just what it determines.
> I never claimed that NAFL is "superior" or any such thing.
You've got to be kidding. If 'superior' is not the exact word, then replace with any approriate cognate.
> I would > just like the rest of the world to acknowledge that NAFL exists.
And I'd like the rest of the world to give me youth, beauty, wisdom, and free office supplies for a lifetime. What I've noticed though is that "the rest of the world" is usually fairly occupied with its own needs.
Anyway, for what it's worth, I give you my personal acknowledgment that NAFL exists. As to anything else substantive regarding NAFL, I can't say much, despite my having read plenty of your official and unofficial ramblings on the subject.
> I > have explained NAFL in various eprints and also a peer-reviewed > conference paper in International Journal of Quantum Information. The > essentials of NAFL are not at all difficult to understand, although > they may be difficult to accept for someone like you who is > classically trained.
I can't make sense of it. And my understanding is not limited to classical mathematics.
> As for your assertion that ordinary metamathematical concepts can be > formalized, I take the stand that you have to draw the line somewhere > and accept that certain concepts cannot be formalized, unless you > either accept an infinite regress or circularity.
I call it an ''unlimited escalation'. I've mentioned in some other posts how I view that. In any case, it doesn't vitiate that ordinary theorems of metamathematics can be formally derived.
> The cruical point is > that those concepts that I assert cannot be formalized within NAFL > should be clear enough for everybody to accept.
Tell me what those concepts are. Meanwhile, I've got a bunch of stuff formalized; I see no reason to dump it in favor of NAFL that even you admit is incapable of formalizing such matters.
> NAFL is actually a bunch of metamatthematical rules that NAFL theories > have to satsify.
You still haven't given a coherent definition of 'NAFL theory'.
As to rules, go ahead and state them.
> I claim that the metamathematical notions used are > indeed clear and acceptable and provide a basis for working within > NAFL theoreis.
You claim. Meanwhile, I'll be the judge for myself what is clear and acceptable for my own understanding of mathematics. You're welcome to give your arguments to convince and enlighten me, but your claiming clarity and accetability is not enough.
> But many of these notions are *about* NAFL theories and > cannot be formalized within NAFL theories. The metatheory of NAFL > theories will necessarily have unformalized concepts and there is no > metatheory of this metatheory.
(1) You still haven't given a coherent definition or explanation of what an NAFL theory is. (2) I don't mind informal concepts if they have some role that can't be accomplished by formalized ones, yet I don't know of any advantage of your informal concepts over the formalized ones that I do find useful.
> As I type this post at 6 AM, I have been working all night on a > software project. I have to complete this project in about a week's > time. Once I am done with that I will have some free time to post the > thread on NAFL. I will surely be mentally fatigued, but then I have to > accept that the days when I could work full time on whatever I wanted > to are now over. IBM is insisting on its pound of flesh and I cannot > complain about having to work for a living.
Hard and demanding jobs; working for a living. Hmm, yes, I've heard of it.
Aatu Koskensilta wrote: > That's entirely irrelevant to the observation that Godel's proof is
> perfectly finitary in the ordinary sense of the word.
Yes, in the ordinarily sense of the word "finitary" then every thing Godel or anyone else ever uttered or wrote down (proofs included) would be perfectly finitary, which is of course *very trivial*! But is that what you're really saying here?
> On Jan 29, 9:43 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi> > wrote:
> > On 2008-01-28, in sci.logic, R. Srinivasan wrote:
> > > It takes a lot of *coding* to put all of this into primitive recursive > > > arithmetic, which only deals with numbers as objects. Your claim that > > > Godel's proof is finitary is dependent on the fact that the said proof > > > can be encoded into PRA. But I on the other hand, insist that the > > > notion of "all primitive recursive functions" is *essentially* > > > infinitary and *cannot* be encoded via any finitary process into > > > PRA.
> > We can just talk about, say, extensions of Q, as outlined by Rupert in > > an another post. As to all the tedious coding, you'll find the details > > in any number of texts, such as Girard's _Proof Theory and Logical > > Complexity_. As to NAFL, of which I'm entirely ignorant, it might or > > might not be that Godel's proof goes through. That's entirely > > irrelevant to the observation that Godel's proof is perfectly finitary > > in the ordinary sense of the word.
> > > But strictly speaking, to show that (1) would entail consistency of > > > PRA, one would have to also use ex falso quodlibet (from a > > > contradiction P&~P, an arbitrary propostion Q can be deduced).
> > If we define inconsistency as proving every sentence ex falso > > quadlibet is indeed required. However, as outlined in a post of mine > > /A recursion theoretic look at incompleteness/ we can formulate the > > first incompleteness theorem in a 'logic-agnostic' form, making no > > assumptions about the underlying logic of the theory. The second > > incompleteness theorem has no such formulation, and does depend on the > > properties of the rules of inference.
> I wish to define consistency of a theory T by the requirement that > *every* sentence of the form P&~P (i.e. every contradiction) in the > language of T should be unprovable in T. Therefore my definition of > inconsistency of T is the provability in T of at least one > contradiction. By ex falso quodlibet, the consistency of T can be > reduced to the unprovability of a single sentence (say, "0=1") and > this is seemingly a finitary concept. What I was trying to get at was > that this latter assertion requires ex falso quodlibet if it were to > really represent consistency, and that the inference from ex falso > quodlibet (that T proves every contradiction in its language if T > proves one contradiction) cannot really be expressed finitarily. > Please see my comments below.
> > > 'A proof of any sentence of the form P&~P in PRA implies that every > > > sentence in the language of PRA is deducible in PRA' (2)
> > That is trivially provable in PRA. However, I wonder why you're > > talking about PRA here? What was at issue was PRA proving the > > incompleteness theorems, not what PRA proves of itself. (It does, of > > course, prove that the incompleteness theorems apply to PRA).
> The reason I am talking about PRA is that it is considered as the > formal system that correctly captures finitism. Presumably you are > asserting that the reasoning used by Godel is finitary because that > reasoning can be formalized within PRA.
> Now I do not agree with your assertion that the sentence (2) above is > trivially provable *in* PRA. We can indeed infer that PRA will prove > every sentence in its language if it proves a contradiction. But that > inference is not made *within* PRA, it is a metamathematical fact > *about* PRA. For the sentences of PRA are about numbers and no > sentence of PRA can ever tell you something about all of its > sentences, at least not without the kind of coding employed by Godel.
Expanding on this theme, the sentence (2) under consideration is:
'A proof of any sentence of the form P&~P in PRA implies that every sentence in the language of PRA is deducible in PRA' (2)
This sentence is not expressible in the language of PRA and is really a theorem scheme of PRA. One enumerates the contradictions of the form P&~P and their consequences such that in the given list, every conceivable sentence of PRA follows from each of the contradictions enumerated.
But Godel apparently managed to encode (2) into a single sentence in the language of PRA. Call this sentence as (3):
Sentence encoding (2) into the language of PRA (3)
As per what Aatu said above, (3) is trivially provable in PRA. But if one scans all the proofs of PRA proper (with no encoding), one should not be able to find either a proof or refutation of (2), for the simple reason that (2) is not a single sentence in the language of PRA. Therefore by this logic, (3) *ought* to be undecidable in PRA. But undecidability of (3) in PRA would imply (after decoding) that (2) is undecidable in PRA and therefore by the completeness theorem, there must exist a model for PRA in which
(PRA |- P&~P) & ~(PRA |- Q) (4)
where P and Q are specific sentences in the language of PRA. Such a model cannot exist if |- really represents provability.
So we have the uncomfortable situation in which the provability predicate either wrongly lists the sentence (2) (after encoding via (3)) as a theorem of PRA or else the provability predicate is provably not about provability. Apparently the first of these holds, as per what Aatu said.
This is a general problem with any attempt to encode the notion of "all sentences" in the language of a theory into the language of that theory, which is needed to formalize the notion of prrovability. There is no such thing as an "arbitrary sentence" in the language of first- order theories, but there is such a thing as an arbitrary natural number. Using natural numbers to encode sentences is problematic for this reason, in that the language is really expanded beyond what is acceptable at first order.
> On Jan 30, 4:12 pm, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > On Jan 29, 9:43 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi> > > wrote:
> > > On 2008-01-28, in sci.logic, R. Srinivasan wrote:
> > > > It takes a lot of *coding* to put all of this into primitive recursive > > > > arithmetic, which only deals with numbers as objects. Your claim that > > > > Godel's proof is finitary is dependent on the fact that the said proof > > > > can be encoded into PRA. But I on the other hand, insist that the > > > > notion of "all primitive recursive functions" is *essentially* > > > > infinitary and *cannot* be encoded via any finitary process into > > > > PRA.
> > > We can just talk about, say, extensions of Q, as outlined by Rupert in > > > an another post. As to all the tedious coding, you'll find the details > > > in any number of texts, such as Girard's _Proof Theory and Logical > > > Complexity_. As to NAFL, of which I'm entirely ignorant, it might or > > > might not be that Godel's proof goes through. That's entirely > > > irrelevant to the observation that Godel's proof is perfectly finitary > > > in the ordinary sense of the word.
> > > > But strictly speaking, to show that (1) would entail consistency of > > > > PRA, one would have to also use ex falso quodlibet (from a > > > > contradiction P&~P, an arbitrary propostion Q can be deduced).
> > > If we define inconsistency as proving every sentence ex falso > > > quadlibet is indeed required. However, as outlined in a post of mine > > > /A recursion theoretic look at incompleteness/ we can formulate the > > > first incompleteness theorem in a 'logic-agnostic' form, making no > > > assumptions about the underlying logic of the theory. The second > > > incompleteness theorem has no such formulation, and does depend on the > > > properties of the rules of inference.
> > I wish to define consistency of a theory T by the requirement that > > *every* sentence of the form P&~P (i.e. every contradiction) in the > > language of T should be unprovable in T. Therefore my definition of > > inconsistency of T is the provability in T of at least one > > contradiction. By ex falso quodlibet, the consistency of T can be > > reduced to the unprovability of a single sentence (say, "0=1") and > > this is seemingly a finitary concept. What I was trying to get at was > > that this latter assertion requires ex falso quodlibet if it were to > > really represent consistency, and that the inference from ex falso > > quodlibet (that T proves every contradiction in its language if T > > proves one contradiction) cannot really be expressed finitarily. > > Please see my comments below.
> > > > 'A proof of any sentence of the form P&~P in PRA implies that every > > > > sentence in the language of PRA is deducible in PRA' (2)
> > > That is trivially provable in PRA. However, I wonder why you're > > > talking about PRA here? What was at issue was PRA proving the > > > incompleteness theorems, not what PRA proves of itself. (It does, of > > > course, prove that the incompleteness theorems apply to PRA).
> > The reason I am talking about PRA is that it is considered as the > > formal system that correctly captures finitism. Presumably you are > > asserting that the reasoning used by Godel is finitary because that > > reasoning can be formalized within PRA.
> > Now I do not agree with your assertion that the sentence (2) above is > > trivially provable *in* PRA. We can indeed infer that PRA will prove > > every sentence in its language if it proves a contradiction. But that > > inference is not made *within* PRA, it is a metamathematical fact > > *about* PRA. For the sentences of PRA are about numbers and no > > sentence of PRA can ever tell you something about all of its > > sentences, at least not without the kind of coding employed by Godel.
> Expanding on this theme, the sentence (2) under consideration is:
> 'A proof of any sentence of the form P&~P in PRA implies that > every sentence in the language of PRA is deducible in PRA' (2)
> This sentence is not expressible in the language of PRA and is really > a theorem scheme of PRA. One enumerates the contradictions of the form > P&~P and their consequences such that in the given list, every > conceivable sentence of PRA follows from each of the contradictions > enumerated.
> But Godel apparently managed to encode (2) into a single sentence in > the language of PRA. Call this sentence as (3):
> Sentence encoding (2) into the language of PRA (3)
> As per what Aatu said above, (3) is trivially provable in PRA. But if > one scans all the proofs of PRA proper (with no encoding), one should > not be able to find either a proof or refutation of (2), for the > simple reason that (2) is not a single sentence in the language of > PRA.
To be more precise, one ought not to find a proof of (2) in PRA proper (with no encoding) because (2) is not a single sentence in the language of PRA. The refutation of (2) will be the proof of a single sentence (the sentence (4) below), but one ought not to find that either because such a proof would contradict ex falso quodlibet.
>Therefore by this logic, (3) *ought* to be undecidable in PRA. > But undecidability of (3) in PRA would imply (after decoding) that (2) > is undecidable in PRA and therefore by the completeness theorem, there > must exist a model for PRA in which
> (PRA |- P&~P) & ~(PRA |- Q) (4)
> where P and Q are specific sentences in the language of PRA. Such a > model cannot exist if |- really represents provability.
> So we have the uncomfortable situation in which the provability > predicate either wrongly lists the sentence (2) (after encoding via > (3)) as a theorem of PRA or else the provability predicate is provably > not about provability. Apparently the first of these holds, as per > what Aatu said.
> This is a general problem with any attempt to encode the notion of > "all sentences" in the language of a theory into the language of that > theory, which is needed to formalize the notion of prrovability. There > is no such thing as an "arbitrary sentence" in the language of first- > order theories, but there is such a thing as an arbitrary natural > number. Using natural numbers to encode sentences is problematic for > this reason, in that the language is really expanded beyond what is > acceptable at first order.
On Jan 30, 10:39 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> On Jan 30, 3:12 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > by the > > NAFL yardstick, the reasoning employed by Godel is not finitary.
> By the NAFL yardstick, anything can be anything you personally claim > it to be, since your lack of specifiying exactly what the NAFL > yardstick is leaves you as the only person who can say how to apply > it.
I notice that you have not responded to the main argument in my post to which you were replying. And nobody has responded to either that post or my subsequent posts elaborating that argument. Why can't we have a striaghtforward discussion even in a open newsgroup like sci.logic (where there are no "moderators" to manipulate the discussion)? May I conclude from the deafening silence that my argument is essentially correct? If not, can you enlighten me on what I am to conclude?
Anyway, some time back you remember that I said that a NAFL theory T has a separate "proof syntax" (p-syntax) and "theory syntax" (t- syntax). The t-syntax consists of all the legitimate propositions of T, including its axioms, theorems and undecidable propositions. The t- syntax can be thought of as the main formalism that represents T. I also mentioned that classical tautologies like ~(P&~P), Pv~P, (P&~P --
>Q), modus ponens, etc. are not legitimate propositons in the t-
syntax, even though they may be used in the proofs (present in the p- syntax) of the theorems of T (in its t-syntax). In fact T will have models in which these classical tautologies are negated. In other words, the theorems in the t-syntax do not imply the classical tautologies, even though these may used in the proofs of the theorems (i.e., the reverse implication may hold).
The sentences in the t-syntax of T cannot contain any sentential variables and it is illegal to quantify over these sentences. So Godlel-encoding of these sentences or their proofs is ruled out in NAFL. And therefore the notion of provability cannot be imported into the main formalism of a NAFL theory T, represented by its t-syntax. Provability must remain at a metatheoretical level, as represented by the p-syntax, which is classical and accepts classical inference rules with sentential variables, etc.
It would be illegal for a NAFL theory T to have "all" sentences of the form
P&~P --> Q
as theorems in its t-syntax without including the above tautology. For such a notion of "all" would contradict NAFL principles. It is just as well that this tautology cannot be a theorem scheme in the t-syntax of NAFL theories.
If you follow the argument I made in my previous 3 posts or so it will give you some insight as to why this restriction on provability is necessary in NAFL, which in my view, represents the genuine yardstick for finitary reasoning (or finitism, which means the same thing in NAFL). Godel's theorems fail in NAFL and therefore cross the boundaries of finitary reasoning.
I will start the NAFL thread explaining all this with as much clarity as I can muster. In the meanwhile let me know what you think.
> On Jan 30, 10:39 pm, MoeBlee <jazzm...@hotmail.com> wrote:> On Jan 30, 3:12 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> > > by the > > > NAFL yardstick, the reasoning employed by Godel is not finitary.
> > By the NAFL yardstick, anything can be anything you personally claim > > it to be, since your lack of specifiying exactly what the NAFL > > yardstick is leaves you as the only person who can say how to apply > > it.
> I notice that you have not responded to the main argument in my post > to which you were replying. And nobody has responded to either that > post or my subsequent posts elaborating that argument. Why can't we > have a striaghtforward discussion even in a open newsgroup like > sci.logic (where there are no "moderators" to manipulate the > discussion)? May I conclude from the deafening silence that my > argument is essentially correct? If not, can you enlighten me on what > I am to conclude?
I don't have time or interest to comment on every argument, even arguments by people with whom I am engaged in other comments at the time. My silence on any particular matter is not to be taken as any form of tacit agreement.
> Anyway, some time back you remember that I said that a NAFL theory T
What follows does me little good unless you define the predicate 'T is an NAFL theory'.
> has a separate "proof syntax" (p-syntax) and "theory syntax" (t- > syntax). The t-syntax consists of all the legitimate propositions of > T, including its axioms, theorems and undecidable propositions.
What is the definition of 'an NAFL theory'? What is the definition of 'a legitimate propostion'?
What (if any) are the restrictions on what may be an axiom of a theory?
> The t- > syntax can be thought of as the main formalism that represents T. I > also mentioned that classical tautologies like ~(P&~P), Pv~P, (P&~P -->Q), modus ponens, etc. are not legitimate propositons in the t-
> syntax, even though they may be used in the proofs (present in the p- > syntax) of the theorems of T (in its t-syntax).
That might be of some interest if you define 'legitimate proposition'.
> In fact T will have > models in which these classical tautologies are negated.
By 'negated in the model' do you mean 'false in the model'?
And are you using 'model' in its usual sense in mathematical logic?
> In other > words, the theorems in the t-syntax do not imply the classical > tautologies, even though these may used in the proofs of the theorems > (i.e., the reverse implication may hold).
Each of your paragraphs now is compounded in unintelligability to me for the growing list of undefined terminology.
> The sentences in the t-syntax of T cannot contain any sentential > variables and it is illegal to quantify over these sentences.
Where do provide all the rules? Where are the rules for what is a sentence of the t-syntax? Where are the rules for quantifiers?
> So > Godlel-encoding of these sentences or their proofs is ruled out in > NAFL. And therefore the notion of provability cannot be imported into > the main formalism of a NAFL theory T, represented by its t-syntax. > Provability must remain at a metatheoretical level, as represented by > the p-syntax, which is classical and accepts classical inference rules > with sentential variables, etc.
If you provided the rules by which you are making those inferences about NAFL, then other people could check your statements and discover inferences of their own too. As it stands, I can only take your word for it that you've made these inferences about these things that you still have not even defined for me.
> It would be illegal for a NAFL theory T to have "all" sentences of the > form
> P&~P --> Q
> as theorems in its t-syntax without including the above tautology. For > such a notion of "all" would contradict NAFL principles. It is just as > well that this tautology cannot be a theorem scheme in the t-syntax of > NAFL theories.
At this point, you might as well be reading to me random selections from the rules of various obscure card games mixed together with sub- regulations in arcane tax and tariff codes.
> If you follow the argument I made in my previous 3 posts or so it will > give you some insight as to why this restriction on provability is > necessary in NAFL, which in my view, represents the genuine yardstick > for finitary reasoning (or finitism, which means the same thing in > NAFL). Godel's theorems fail in NAFL and therefore cross the > boundaries of finitary reasoning.
Your view that NAFL is the genuine standard for finitary reasoning. Perhaps one day you'll say that NAFL IS so that other people can form also their own views on the matter.
> I will start the NAFL thread explaining all this with as much clarity > as I can muster. In the meanwhile let me know what you think.
I just did, and have been, which is infintely more than you've done to make good on your continual promise to make that thread of yours.
On Feb 9, 12:27 am, MoeBlee <jazzm...@hotmail.com> wrote:
> On Feb 8, 8:54 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
[...] > > In other > > words, the theorems in the t-syntax do not imply the classical > > tautologies, even though these may used in the proofs of the theorems > > (i.e., the reverse implication may hold).
> Each of your paragraphs now is compounded in unintelligability to me > for the growing list of undefined terminology.
The point I was trying to make is that even though, say, Pv~P, may be used to prove theorems of a NAFL theory T, it does not follow that T implies Pv~P. In fact it does not, if P is undecidable in T; Pv~P is not even a legitimate proposition in the t-syntax
[...]
> Your view that NAFL is the genuine standard for finitary reasoning. > Perhaps one day you'll say that NAFL IS so that other people can form > also their own views on the matter.
> > I will start the NAFL thread explaining all this with as much clarity > > as I can muster. In the meanwhile let me know what you think.
> I just did, and have been, which is infintely more than you've done to > make good on your continual promise to make that thread of yours.
OK, I will post this thread in the near future, when I find some continuous free time. I do not want to start a thread and then not respond to queries for days. Need to keep up the continuity of the thread, and need to have a free mind to think and post clearlyl
On Feb 9, 4:22 am, "R. Srinivasan" <sradh...@in.ibm.com> wrote:
> The point I was trying to make is that even though, say, Pv~P, may be > used to prove theorems of a NAFL theory T, it does not follow that T > implies Pv~P. In fact it does not, if P is undecidable in T; Pv~P is > not even a legitimate proposition in the t-syntax
You're giving a bit of information still without giving me a systematic context.
|
