Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: Torkel Franzen on 30 Jan 2005 00:09 tchow(a)lsa.umich.edu writes: > O.K., let me try another version. > > (*) Intension-preserving formalization of informal mathematical > statements is always possible. > Maybe this should be thought of not as a thesis but as a "thesis schema"? > Instances of the schema would be things like: > > (+) Con("PA") is an intension-preserving formalization of "PA is > consistent." (+) is not on the face of it an instance of (*), since it states not only that an itension-preserving formalization of "PA is consistent" is possible, but that a particular arithmetical formula is such a formalization. What is required of an intension-preserving formalization? In formalizing Con(PA) or the fundamental theorem of arithmetic in PA, we need to represent finite sequences of numbers as numbers. This can be done in many ways, but are they intension-preserving?
From: |-|erc on 30 Jan 2005 00:11 "William Elliot" <marsh(a)privacy.net> wrote in ... > On Sat, 29 Jan 2005 tchow(a)lsa.umich.edu wrote: > > > (*) Formal sentences (in PA or ZFC for example) adequately express > > their informal counterparts. > > > A formal sentence could have an unintuitive or even incomprehensible > informal counterpart you're full of propositions today. Herc
From: r.e.s. on 30 Jan 2005 01:04 "William Elliot" <marsh(a)privacy.net> wrote ... > r.e.s. wrote: >> <tchow(a)lsa.umich.edu> wrote ... >>> >>> (*) Formal sentences (in PA or ZFC for example) adequately express >>> their informal counterparts. >> >> That reminds me of what Davis & Hersh say about >> Hilbert's "formalist premise" ... >> > It's the converse of Hilbert's thesis, that every informal mathematical > statement can be formalized. That's not quite what the premise quoted below says, IMO. >> "[...]the formalist premise, >> that a solidly founded theory about formal sentences >> could validate the mathematical activity of real life [...]" This says, roughly, that the formal validates the informal, which suggests that the informal can be formally expressed adequately enough to be validated. --r.e.s.
From: Helene.Boucher on 30 Jan 2005 02:24 tchow(a)lsa.umich.edu wrote:> > Maybe this should be thought of not as a thesis but as a "thesis schema"? > Instances of the schema would be things like: > > (+) Con("PA") is an intension-preserving formalization of "PA is > consistent." > > Yeah, I know I'm abusing the term "schema" here, but I think you know > what I mean. Con("PA") is formal; "PA is consistent" is informal, so > like the Church-Turing thesis I'm equating---or at least making a tight > correspondence between---something formal and something informal. > > Something like (+) is tacitly assumed by most people. Whenever we > draw philosophical conclusions from Goedel's 2nd theorem such as "The > consistency of PA cannot be proved using methods formalizable in PA" > we are tacitly assuming (+) and a whole host of statements like it. > This degree of acceptance seems to me to be very parallel to the > widespread acceptance of the Church-Turing thesis. I don't think Con("PA") is intension-preserving. In fact it seems to make a weaker assertion than "PA is consistent". (So, the assertion that one can't prove Con("PA") in PA is a stronger assertion than what one claims or thinks it to be.) Look at it this way. Proof(x,y) - the first-order wff in PA that x is a Godel number of a proof P of the theorem T represented by the Godel number of y - asserts more than that P is a proof of T. One can imagine the situation where there is a proof P of T, but not that there is the extremely large number x which is used to represent the proof P. You can see this clearly in second-order systems of arithmetic without the successor axiom. There one can write the normal Proof(x,y), where x and y are Godel numbers. But one can write a second-order formula assertion, Proof2(R,S) in the following way. Symbols of a formal language are represented by some (finite) set of numbers, Y. A finite sequence is a second-order letter S such that the domain of S is {x | x <= n} for some natural number n. A finite string is a finite sequence with image Y. A wff is a finite string which meets certain conditions. Y* is the union of Y and some number not in Y. This new number represents a line break; it will separate wffs in a proof. A proof is therefore a finite sequence with image Y* which meets certain conditions. I would assert that Proof2 more closely hews to our intuitive notion of proof than Proof. It also, in general, speaks of numbers much lower than the numbers of Proof. That is, Proof2 speaks of numbers which are the length of a proof, while Proof uses numbers which are exponential with respect to the length. So, in fact, in the second-order systems of which I speak, one can prove that Proof(x,y) implies Proof2(R,S), where R represents the same wff as x, and S represents the same wff as y, but one cannot prove the contrary. Thus, Proof is a stronger notion than our intuitive one. Ergo Con(), which speaks of the inexistence of a proof, is a weaker notion than our intuitive one.
From: |-|erc on 30 Jan 2005 03:03
<Helene.Boucher(a)wanadoo.fr> wrote in message > tchow(a)lsa.umich.edu wrote:> > > Maybe this should be thought of not as a thesis but as a "thesis > schema"? > > Instances of the schema would be things like: > > > > (+) Con("PA") is an intension-preserving formalization of "PA is > > consistent." > > > > Yeah, I know I'm abusing the term "schema" here, but I think you know > > what I mean. Con("PA") is formal; "PA is consistent" is informal, so > > like the Church-Turing thesis I'm equating---or at least making a > tight > > correspondence between---something formal and something informal. > > > > Something like (+) is tacitly assumed by most people. Whenever we > > draw philosophical conclusions from Goedel's 2nd theorem such as "The > > consistency of PA cannot be proved using methods formalizable in PA" > > we are tacitly assuming (+) and a whole host of statements like it. > > This degree of acceptance seems to me to be very parallel to the > > widespread acceptance of the Church-Turing thesis. > > I don't think Con("PA") is intension-preserving. In fact it seems to > make a weaker assertion than "PA is consistent". (So, the assertion > that one can't prove Con("PA") in PA is a stronger assertion than what > one claims or thinks it to be.) > > Look at it this way. Proof(x,y) - the first-order wff in PA that x is > a Godel number of a proof P of the theorem T represented by the Godel > number of y - asserts more than that P is a proof of T. One can > imagine the situation where there is a proof P of T, but not that there > is the extremely large number x which is used to represent the proof P. > > > You can see this clearly in second-order systems of arithmetic without > the successor axiom. There one can write the normal Proof(x,y), where > x and y are Godel numbers. But one can write a second-order formula > assertion, Proof2(R,S) in the following way. > > Symbols of a formal language are represented by some (finite) set of > numbers, Y. A finite sequence is a second-order letter S such that the > domain of S is {x | x <= n} for some natural number n. A finite string > is a finite sequence with image Y. A wff is a finite string which > meets certain conditions. Y* is the union of Y and some number not in > Y. This new number represents a line break; it will separate wffs in a > proof. A proof is therefore a finite sequence with image Y* which > meets certain conditions. > > I would assert that Proof2 more closely hews to our intuitive notion of > proof than Proof. It also, in general, speaks of numbers much lower > than the numbers of Proof. That is, Proof2 speaks of numbers which are > the length of a proof, while Proof uses numbers which are exponential > with respect to the length. So, in fact, in the second-order systems > of which I speak, one can prove that Proof(x,y) implies Proof2(R,S), > where R represents the same wff as x, and S represents the same wff as > y, but one cannot prove the contrary. Thus, Proof is a stronger notion > than our intuitive one. Ergo Con(), which speaks of the inexistence of > a proof, is a weaker notion than our intuitive one. There's 2 kinds of exponential w.r.t. a number, I think you just selectively interpreted one for each case that suits. the size (value) of the number is exponential w.r.t. the length of Proof1 the size (value) of the number is expenential w.r.t. the length of Proof2 Proof 2 is linear to the length of the number. Proof1 is also linear w.r.t. the length of the number. godel numbers were more hindrance than help. all programs, formulas, wff, numbers, sentences... all map to some base number OF THE SAME LENGTH AS THAT SENTENCE. (f(0) & An,f(n)->f(n+1)) -> An,f(n) This is just 121345621749584874833262727 Same size, exponential just means the number of possibilies goes up, same for 1st order and 2nd order systems unless you can define some great compressive mapping. A real program, MS:Paint has a godel number, its the 1 megabyte long value of the file! Herc |