[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):
http://www.cohums.ohio-state.edu/philo/people/Faculty/tennant.9/dgp_mind.pdf
Neil Tennant
More information about the FOM
mailing list