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

• Previous message: |-|erc: "My claim on Omega's defn"
• In reply to: tchow_at_lsa.umich.edu: "Re: Name the thesis: "Formal sentences capture informal ones""
• Next in thread: Torkel Franzen: "Re: Name the thesis: "Formal sentences capture informal ones""
• Reply: Torkel Franzen: "Re: Name the thesis: "Formal sentences capture informal ones""
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Date: 29 Jan 2005 23:24:54 -0800

tchow@lsa.umich.edu wrote:>
> 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.
>
> Something like (+) is tacitly assumed by most people. Whenever we
> draw philosophical conclusions from Goedel's 2nd theorem such as "The
> consistency of PA cannot be proved using methods formalizable in PA"
> we are tacitly assuming (+) and a whole host of statements like it.
> This degree of acceptance seems to me to be very parallel to the
> widespread acceptance of the Church-Turing thesis.

I don't think Con("PA") is intension-preserving. In fact it seems to
make a weaker assertion than "PA is consistent". (So, the assertion
that one can't prove Con("PA") in PA is a stronger assertion than what
one claims or thinks it to be.)

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.

You can see this clearly in second-order systems of arithmetic without
the successor axiom. There one can write the normal Proof(x,y), where
x and y are Godel numbers. But one can write a second-order formula
assertion, Proof2(R,S) in the following way.

Symbols of a formal language are represented by some (finite) set of
numbers, Y. A finite sequence is a second-order letter S such that the
domain of S is {x | x <= n} for some natural number n. A finite string
is a finite sequence with image Y. A wff is a finite string which
meets certain conditions. Y* is the union of Y and some number not in
Y. This new number represents a line break; it will separate wffs in a
proof. A proof is therefore a finite sequence with image Y* which
meets certain conditions.

I would assert that Proof2 more closely hews to our intuitive notion of
proof than Proof. It also, in general, speaks of numbers much lower
than the numbers of Proof. That is, Proof2 speaks of numbers which are
the length of a proof, while Proof uses numbers which are exponential
with respect to the length. So, in fact, in the second-order systems
of which I speak, one can prove that Proof(x,y) implies Proof2(R,S),
where R represents the same wff as x, and S represents the same wff as
y, but one cannot prove the contrary. Thus, Proof is a stronger notion
than our intuitive one. Ergo Con(), which speaks of the inexistence of
a proof, is a weaker notion than our intuitive one.

• Previous message: |-|erc: "My claim on Omega's defn"
• In reply to: tchow_at_lsa.umich.edu: "Re: Name the thesis: "Formal sentences capture informal ones""
• Next in thread: Torkel Franzen: "Re: Name the thesis: "Formal sentences capture informal ones""
• Reply: Torkel Franzen: "Re: Name the thesis: "Formal sentences capture informal ones""
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]