Torkel Franzen on truth
in [Logic]
|
From: LordBeotian on 1 Dec 2007 09:31 "MoeBlee" <jazzmobe(a)hotmail.com> ha scritto >> Consider also that even 2nd order Peano arithmetic is not formalizable. > > I don't know what you mean by '2nd order Peano arithmetic', but there > is a formal theory that is second order Peano arithmetic. Ok, actually second order *logic* is not formalizable. Consider any formalization L2 that is supposed to represent every possible 2nd order deduction. Consider the formula asserting "(the conjunction of the 2nd order Peano Axioms) -> G" where G is the Godel formula for L2. This formula is true in any 2nd order model, so it represents a correct 2nd order deduction. Yet it is not covered by our formalization.
From: hype on 1 Dec 2007 18:41 well, i think the point which Franzen emphasize by the truth which we know is, "if PA is consistent, G is true", what we don't know is, directly " G is true" whether we do not have any idea about the consistency of PA, and because the sentence "if PA is consistent, G is true" is also provable by PA, while G is not if it is consistent. Peter_Smith yazdı: > On 9 Nov, 05:01, Newberry <newberr...(a)gmail.com> wrote: > > On Nov 8, 6:21 am, Peter_Smith <ps...(a)cam.ac.uk> wrote: > > > > > > > > > On 8 Nov, 09:13, Gc <Gcut...(a)hotmail.com> wrote: > > > > > > On 8 marras, 11:10, Gc <Gcut...(a)hotmail.com> wrote: > > > > > > > On 8 marras, 10:26, Peter_Smith <ps...(a)cam.ac.uk> wrote: > > > > > > > > On 8 Nov, 06:01, Newberry <newberr...(a)gmail.com> wrote: > > > > > > > > > In "G�del's theorem" Torkel Franzen disputes that the theorem > > > > > > > indicates that the human mind surpasses any computer. > > > > > > > > > >> ... the mistaken idea that "G�del's theorem states that in any consistent system which is strong enough to produce simple arithmetic there are formulas which cannot be proved in the system, but which we can see to be true." The theorem states no such thing. As has been emphasized, in general we simply have no idea whether or not the G�del sentence of a system is true, even in those cases when it is in fact true. What we know is that the G�del sentence is true if and only if the system is consistent, and that much is provable in the system itself. << p. 55 > > > > > > > >> ... there is no doubt whatever about the consistency of any of the formal systems we use in mathematics. << p. 105 > > > > > > > >> If the axioms of ZFC are manifestly true, they are obviously consistent. << p. 105 > > > > > > > > > I am not sure that I understand what Franzen is saying. > > > > > > > > The first quote you give, I take it is entirely clear (and correct!). > > > > > > > This I don`t understand: > > > > > "As has been emphasized, in general we simply have no idea whether or > > > > > not the G�del sentence of a system is true, even in those cases when > > > > > it is in fact true." > > > > > > > I have thought: If we assume the consistency of PA we can proof in PA > > > > > + con(PA) that the g�del sentence of PA being true but not-provable > > > > > (thus it follows from this that also the con(PA) is not provable from > > > > > the axioms of PA). And certainly we have an least an informally "idea" > > > > > that PA is consistent. > > > > > > Oh wait. OK. Now I understand? The point is in GENERAL we don`t have > > > > an idea if the g�del sentence is true, like in New Foundations? > > > > > Yes, I think that's what TF was after: we'll in general not know > > > whether T's standard G�del's sentence is true because we'll not know > > > whether T is consistent. (Of course, we are usually interested in > > > theories T which we have pretty good reason to think are consistent, > > > and we are usually not interested in the other cases! TF is just > > > reminding us of the general situation.) > > > > Do you mean that PA is PROBABLY consistent? > > Read "pretty good reason" to mean "at least pretty good reason, maybe > conclusive reason". As it happens I think there are conclusive reasons > to believe PA consistent.
From: Chris Menzel on 1 Dec 2007 20:40 On Sat, 1 Dec 2007 15:31:24 +0100, LordBeotian <pokipsy76(a)yahoo.it> said: > > "MoeBlee" <jazzmobe(a)hotmail.com> ha scritto > >>> Consider also that even 2nd order Peano arithmetic is not >>> formalizable. >> >> I don't know what you mean by '2nd order Peano arithmetic', but there >> is a formal theory that is second order Peano arithmetic. > > Ok, actually second order *logic* is not formalizable. It is formalizable in the same sense that 2nd order PA is (or first order PA, for that matter). There's just no semantically complete, consistent, recursive axiomatization of it (just as there is no negation complete, consistent, recursive axiomatization of PA). > Consider any formalization L2 that is supposed to represent every > possible 2nd order deduction. You mean a formalization in which every 2nd order validity (in the language of the formalization) is provable? > Consider the formula asserting "(the conjunction of the 2nd order > Peano Axioms) -> G" where G is the Godel formula for L2. This formula > is true in any 2nd order model, so it represents a correct 2nd order > deduction. I guess you mean a second-order validity. > Yet it is not covered by our formalization. So, assuming "covered by" means "provable in", it appears that, for you, a formalization has to be complete.
From: LordBeotian on 2 Dec 2007 07:54 "Chris Menzel" <cmenzel(a)remove-this.tamu.edu> ha scritto >> Ok, actually second order *logic* is not formalizable. > > It is formalizable in the same sense that 2nd order PA is (or first > order PA, for that matter). There's just no semantically complete, > consistent, recursive axiomatization of it (just as there is no negation > complete, consistent, recursive axiomatization of PA). Ok. >> Consider any formalization L2 that is supposed to represent every >> possible 2nd order deduction. > > You mean a formalization in which every 2nd order validity (in the > language of the formalization) is provable? Yes, I was meaning a complete formalization of second order reasoning. Incomplete formalizations would not allow to say that 2nd order reasonings are formalizable in general (see below). >> Consider the formula asserting "(the conjunction of the 2nd order >> Peano Axioms) -> G" where G is the Godel formula for L2. This formula >> is true in any 2nd order model, so it represents a correct 2nd order >> deduction. > > I guess you mean a second-order validity. Yes. >> Yet it is not covered by our formalization. > > So, assuming "covered by" means "provable in", it appears that, for you, > a formalization has to be complete. Yes... The discussion was getting a bit phylsophical. The point was: does every reasoning have to be formalizable in order to be a "reasoning"? Do there exist rules of reasoning that we follow even when we are not conscient of them? In this context a relevant "formalization" of reasonings should be complete, I think, otherwise evrything is trivially formalizable by an "ad hoc" incomplete set of rules.
From: MoeBlee on 3 Dec 2007 12:18
On Dec 1, 6:31 am, "LordBeotian" <pokips...(a)yahoo.it> wrote: > "MoeBlee" <jazzm...(a)hotmail.com> ha scritto > > >> Consider also that even 2nd order Peano arithmetic is not formalizable. > > > I don't know what you mean by '2nd order Peano arithmetic', but there > > is a formal theory that is second order Peano arithmetic. > > Ok, actually second order *logic* is not formalizable. > Consider any formalization L2 that is supposed to represent every possible > 2nd order deduction. Consider the formula asserting "(the conjunction of the > 2nd order Peano Axioms) -> G" where G is the Godel formula for L2. This > formula is true in any 2nd order model, so it represents a correct 2nd order > deduction. Yet it is not covered by our formalization. I wouldn't put it that way. Rather, I would say: There is a formal system that is called 'second order logic', but (unlike first order logic) with second order logic it is not the case that every validity is provable; and there is a formal system that is called 'second order PA', of which it is not the case that every formula entailed by the axioms is provable from the axioms. What makes a system formal is that it is recursively axiomatized, not whether the system proves every formula that is entailed by the axioms. MoeBlee |