Re: Name the thesis: "Formal sentences capture informal ones"

From: Aatu Koskensilta (aatu.koskensilta_at_xortec.fi)
Date: 01/30/05 

Date: Sun, 30 Jan 2005 12:34:30 +0200

tchow@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@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus