# [FOM] Is Con_Q provable in Q?

Wed Jun 1 16:53:46 EDT 2005

```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