Name the thesis: "Formal sentences capture informal ones"
in [Theory]
|
From: Torkel Franzen on 30 Jan 2005 03:39 Helene.Boucher(a)wanadoo.fr writes: > 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. If we take the view that the existence of n does not imply the existence of 2^n, there is very much in mathematics that falls away, and the question of whether Con(PA) is an adequate formalization of "PA is consistent" becomes a very minor side issue.
From: Helene.Boucher on 30 Jan 2005 03:51 Torkel Franzen wrote: > Helene.Boucher(a)wanadoo.fr writes: > > > 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. > > If we take the view that the existence of n does not imply the > existence of 2^n, there is very much in mathematics that falls away, > and the question of whether Con(PA) is an adequate formalization of > "PA is consistent" becomes a very minor side issue. It's not a side issue to this thread, because that was what this thread was about. I'm not quite sure whether anything essential falls away, in any case.
From: Helene.Boucher on 30 Jan 2005 03:57 I'm sorry, I don't think I understand your reply. "ll programs, formulas, wff, numbers, sentences... all map to some base number OF THE SAME LENGTH AS THAT SENTENCE." I think what you're saying is that, e.g. in base 2, the Godel number coding a sentence has length the length of the sentence. Indeed. Still, because a code is being used, the number is in fact exponential wrt to the length.
From: |-|erc on 30 Jan 2005 04:04 <Helene.Boucher(a)wanadoo.fr> wrote in > I'm sorry, I don't think I understand your reply. > > "ll programs, formulas, wff, numbers, sentences... > all map to some base number OF THE SAME LENGTH AS THAT SENTENCE." > > I think what you're saying is that, e.g. in base 2, the Godel number > coding a sentence has length the length of the sentence. Indeed. > Still, because a code is being used, the number is in fact exponential > wrt to the length. > And 2OL is exponential aswell. It doesn't matter what system of representation you use, a number-string of length L can represent max base^L different formula. How are you getting a more consise representation of proofs? You seem to be using a finite alphabet, and concatinating terms to form an unlimited alphabet. <T10001 T10003 T3332 T100000001> The higher order of representation comes at a cost of more expensive symbols to encode. Herc
From: LordBeotian on 30 Jan 2005 04:30
<Helene.Boucher(a)wanadoo.fr> ha scritto > > If we take the view that the existence of n does not imply the > > existence of 2^n, there is very much in mathematics that falls away, > > and the question of whether Con(PA) is an adequate formalization of > > "PA is consistent" becomes a very minor side issue. > > It's not a side issue to this thread, because that was what this thread > was about. > I'm not quite sure whether anything essential falls away, in any case. A first problem could be that Ex(x=n)->Ex(x=SS0*SS0*...*SS0) [SS0 multiplied n times] is a theorem of PA for any numeral representing n. So PA would be unsound... |