FOM: request for info

[Stephen Cook]

In my 1975 STOC paper on PV I outlined a proof that the Godel sentence
for PV implies the consistency of PV.   (Buss proved in his PhD thesis
that S^1_2 is essentially a conservative extension of PV.)

Steve Cook

	   
	   The equivalence of a Godel sentence for S and the statement
	 Con(S)  can be proved in either:  (for "reasonable systems" S)
	 
	 	a) I-Delta_0+\Omega_1    (in a paper of Paris & Wilkie, see 
	 				  also work of Ed Nelson)
	 or
	 	b) S^1_2	 (slightly later in my phd thesis).
	 
	 As far as I know, these are the weakest systems in which the
	 G\"odel incompleteness theorem has been proved in an
	 manner which is *intensional* in the sense of Feferman.
	   If there are any other intensional proofs the second 
	 incompleteness theorem in weak systems, I'd be interested 
	 to hear about them.
	 
	  --- Sam Buss
	 
	 In reply to:
	 ------------
	 > Date: Fri, 12 Feb 1999 11:15:51 -0500 (EST)
	 > From: Neil Tennant <neilt at mercutio.cohums.ohio-state.edu>
	 > To: fom at math.psu.edu
	 > Subject: FOM: request for info> Cc: neilt at mercutio.cohums.ohio-state
	.edu
	 > 
	 > Can anyone tell me what the weakest theory of arithmetic is within w
	hich
	 > one can formalize the argument for the equivalence of the G"odel-sen
	tencefor S with Con(S), where S contains Robinson's arithmetic R and S 
	is a 
	 > subtheory of Th(N)?
	 > 
	 > Neil Tennant
	 >