[FOM] Godel, Wittgenstein etc.

Neil Tennant neilt at mercutio.cohums.ohio-state.edu
Tue May 6 21:16:13 EDT 2003

Panu is right when he says that

> the real point seems to be that (for a given system F):
> Cons(F) => (-Prov([G]) & G). 

and that adding an explicit "True([G])" is unnecessary.

But it is worth looking a little more closely at what is going on here.
We can split the claim

	 Cons(F) => (-Prov([G]) & G)

into two:

(1)  Cons(F) => -Prov([G]) 
(2)  Cons(F) => G

and then re-write "=>" as a turnstile. The question then arises as to what
system-subscript can be appended to this turnstile. (We already know, of
course, that G is interdeducible with -Prov([G]).)

If "Cons(F)" is the arithmetized consistency statement, then the turnstile
can be that of a possibly very weak subsystem of F---depending, of course,
on just how strong F itself is. But the cost of this is a great increase
in the length of any proof witnessing the turnstile claim.

If, on the other hand, "Cons(F)" is understood as a claim in (what
one might call) "meta-F", then the proofs of (1) and (2) are considerably
shortened. But we have to bear in mind that it is meta-F that is
subscripting the turnstile, and certainly not any subsystem of F.

This brings one to a connection with my earlier exchange with Torkel.
Suppose that instead of "meta-F", one adopts a system in exactly the same
language as F, by adding a suitably weak reflection principle for F. Call
the resulting system F*. In F* one can prove G outright, without using an
explicit consistency assumption for F. The system F* is, however,
equivalent to the consistency extension of F. The reflection principle in
question is

	(n)Prov([psi([n])]) -> (m)psi(m)

where Prov is the provability predicate for the system F. The F*-proof of
G is very natural.

So the "real point" that Panu was trying to get at might be put in the
following summary way:

There is no need for any talk of truth when proving the Godel-sentence
G for F. It suffices either 
(i) to assume, in meta-F, that F is consistent; or 
(ii) to extend F with a reflection principle (but with no new
extra-logical vocabulary) so as to be able to prove G.

Panu's points about conservative truth-theoretic extension were, by the
way, also made in my paper 'Deflationism and the G"odel-Phenomena',
which was what prompted the exchange with Torkel. For (ii) above, see page
577 of that paper (Mind, vol. 111, July 2002):


Neil Tennant

More information about the FOM mailing list