From: Helene.Boucher on 30 Jan 2005 05:07 First, as a concrete example use instead the much simpler (x)(Nx => Ex Sxy) . Then this a theorem of PA, since it is an axiom of PA. It would not, however, be provable in the systems of which I speak. Anyway, I'm not quite sure what essential falls away if PA proves propositions which are not true.
From: Torkel Franzen on 30 Jan 2005 05:12 Helene.Boucher(a)wanadoo.fr writes: > It's not a side issue to this thread, because that was what this thread > was about. Your particular grounds for regarding Con(PA) as not being a faithful formalization of "PA is consistent" involve so many other basic questions that it becomes a side issue, as when somebody questions the consistency of ZFC on the basis that we don't even know that PA is consistent.
From: Aatu Koskensilta on 30 Jan 2005 05:34 tchow(a)lsa.umich.edu wrote: > 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." > > 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. But (+) isn't an instance of (*). In order to get equivalences like (+) we already need a notion of which formal sentences correspond to informal mathematical statements. For example, how do we know that Con("PA") - expressed in what ever way - instead of the myriard other possible arithmetical sentences is the formal counterpart of "PA is consistent"? The point I'm trying to make here is that in order to instantiate (*) to get something like (+) for a particular mathematical statement P we would need to know what formal sentence is the intension-preserving formalization of P. This in turn requires that the notion of "intension-preserving formalization" is explicated in an informative, hopefully mathematical, way. We could consider a more restricted thesis: (*) If phi is an arithmetical formula defining a set of sentences in some formal language, then Con_phi (expressed in some canonical way picked in advance) intension-preservingly formalizes the statement that the theory axiomatized by the set of sentences defined by phi is consistent. But even this thesis is problematic. What sort of consistency are we talking here? Herbrand consistency? Hilbert consistency? Or are these irrelevant and are we assuming some background theory in respect to which various formalizations are found to be equivalent? And how do we know that Con_phi "intension-preservingly" expressed the consistency of the theory defined by phi? What if it just expresses this in a non-intension-preserving way? -- Aatu Koskensilta (aatu.koskensilta(a)xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: LordBeotian on 30 Jan 2005 06:13 <Helene.Boucher(a)wanadoo.fr> ha scritto > First, as a concrete example use instead the much simpler > > (x)(Nx => Ex Sxy) . > > Then this a theorem of PA, since it is an axiom of PA. It would not, > however, be provable in the systems of which I speak. What is the relevance of its being unprovable in that particular system? What is special about that system? > Anyway, I'm not quite sure what essential falls away if PA proves > propositions which are not true. Uhm... if it is not true that Ex(x=n)->Ex(x=SS0*SS0*...*SS0) we should add its negation to PA, but this lead to inconsistency, so we have to change the axioms of PA and so an enormous part of mathematics (which is all connected with arithmetic) should be changed.
From: Helene.Boucher on 30 Jan 2005 06:40
Not at all. To show that two concepts are not equivalent, it is sufficient to present an environment in which they are clearly not the same. The environment that I have proposed does that - thus Con(PA) and "PA is consistent" cannot be intensionally equivalent; they do not "say the same thing." Why this raises "basic questions" is for you to elucidate. If you have an alternative environment, which does the same work, but more suitable to your taste, then by all means present it. Of if you have an alternative argument, then present that. |