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

From: george (greeneg_at_cs.unc.edu)
Date: 02/01/05 

Date: 1 Feb 2005 08:32:50 -0800

Torkel Franzen wrote:
> tchow@lsa.umich.edu writes:
>
> > O.K., let me try another version.
> >
> > (*) Intension-preserving formalization
> > of informal mathematical
> > statements is always possible.

That is just Obviously False;
Godel's theorem is the classic [counter]example.
Though that doesn't say that "first-order truth
in arithmetic over the natnums" can't be formalized
AT ALL, but rather only that it can't be recursively
formalized in FOL. Obviously, if you relax those restrictions,
something closer is possible; there is also my prior claim
that ANYthing you might want to say about first-order
arithmetic is formal whether you like it or not; that
the alleged informality of some presentations is just
irrelevant superficial surface structure; that to understand
those informal statements IS, internally, to correctly translate
them into formal ones; that the informal statement is just a
STYLE of communicating the inherently formal content.
Therefore, to prevent this from lapsing into triviality,
you have to PRESERVE some relevant constraints.
In the case of first-order PA vs. first-order true arithmetic,
I suppose you could formalize meta-
theorems-[about-first-order-theories]-that-can't-be-
formalized-in-first-order-logic, in HIGHER-order logic,
but that trivializes the whole enterprise. Suppose
you have some natural-language way of saying something.
What sort of formal transformation do you have to apply
to that natural langauge to get "formal langauge" out
of it?? A VERY trivial one, surely. You can put formal
sheep's CLOTHING upon ANY informal wolf, EASILY. ACTUALLY
"formalizing" it surely goes a little deeper, and there is
almost certainly MORE than one way to do that, and they
are NOT likely to be isomorphic. The best you can HOPE for,
truly, is multiple mutual approximations, i.e., for any given
informal conjunction, there are VARIOUS formal counterparts
with VARIOUS degrees of desirability, AND CONVERSELY.

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

But again, if by Con("PA") you mean what Godel meant
by it, then this is just blatantly false: PA + ~Con("PA")
is consistent. If Con("PA") were ACTUALLY intension-
preserving then there couldn't be any models of PA in
which it were false, since the falsity of the
"informal"/intended version is precisely the
NON-existence of ANY models of PA.

I agree with the following:
> (+) is not on the face of it an instance
> of (*), since it states not only that an
> intension-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?

Especially when you are MIXING levels!
The question of the consistency of a first-order
theory is INHERENTLY second-order! The POSSIBLITY
of an intension-preserving FIRST-order formalization
is INDEED problematic!

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

In the case of any first-order anything, preserving
intension SPECIFICALLY around the concept of "finite"
is what is hard. Is there any way to augment the concept
of a first-order language, or even just add a new inference
rule to FOL, such that it "gets" Finitude, without going
all the way to 2nd-order logic?

Relevant Pages