From: Helene.Boucher on
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
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
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

<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
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.