[FOM] Is Con_Q provable in Q?

[Andrew Boucher]

On May 28, 2005, at 7:41 PM, joeshipman at aol.com wrote:
>  
> Here's a more general version of Avron's question:
>  
> Is there ANY consistent theory T in the language of arithmetic 
> (addition and multiplication) for which it makes sense to say that T 
> proves Con(T)? 
>  


Yes.  Consider the sub-theory T of second-order PA with the following 
axioms:

(1)  (n)(m)(k)(Nn & Sn,m & Sn,k => m = k)
(2) (n)(m)(k)(Nn & Nk & Sn,m & Sk,m => n = k)
(3)  (n)(Nn => ! Sn,0)
(4)  Induction schema:  From phi(0) and (n)(m)(Nn & Sn,m & phi(n) => 
phi(m)),
infer (n)(Nn => phi(n))

where:
Nn = n is a natural number
Sn,m = m is a successor of n
! = not

Then T can define addition and multiplication predicates and go on to 
prove Con(T), where this latter is the standard proposition using Godel 
numbering.    While it does not seem that this Con(T) is intensionally 
correct (it appears too weak), one can tweak the system slightly in 
several ways so that it can prove a statement where Godel numbering is 
not used and which does appear to correctly assert its own consistency. 
  One tweak, for instance, would be to limit comprehension to non-empty 
predicates, that is
	(there exists x)(phi(x)) => (there exists R)(x)(Rx <=> phi(x)).

If I may add a few words on the Hilbert-Bernays-Lob conditions of 
provability.

(i)  if Z |- A, then Z |- Prov("A")
(ii) Z |- Prov("A => C") => (Prov("A") => Prov("C")) and
(iii) Z |- Prov("A") => Prov("Prov("A")")

where "A" is the Godel number of the statement A.  These conditions are 
apparently too strong, as they assume certain ontological principles 
(e.g. that there must exist numbers "A", "Prov("A")", 
"Prov("Prov("A")")", etc. ad infinitum, given the provability of A) 
which do not seem to be inherent in the notion of A's provability, and 
indeed one can define what is apparently an intensionally correct 
provability predicate for a theory Z which does not satisfy these three 
provability conditions; an example of such theory would be the 
sub-theory T of second-order PA mentioned at the beginning of these 
comments.