[FOM] Consistency

[Andrew Boucher]

On  6 Nov 2006, at 10:52 AM, zahidi at logique.jussieu.fr wrote:

> Dear FOM-members
>
> I was asked the following question:
> "PA does not prove its own consistency. Are there other formal systems
> which do prove their own consistency?"

The answer is "yes".

1/  Jeroslow ("Consistency Statements in Formal Mathematics",  
Fundamenta Mathematicae, vol. 72, 1971, pp. 17-40) used a particular  
fixed point extension of Q v (x)(y)(x = y).
2/  Dan Willard ("Self-verifying axioms systems, the Incompleteness  
Theorem and Related Reflection Principles, JSL, Vol 66, 2001, pp.  
536-596) has presented several cases, based on seven "grounding"  
functions.  He also has a more recent article in the JSL, as I  
recall, also on this topic.
3/  Yvon Gauthier ("The internal Consistency of Arithmetic with  
Infinite Descent", Modern Logic, Vol 8, no 1/2, Jan 1998-Apr 2000,  
pp. 47-86) presented a system with a special quantifier, called  
"effinite".

There is also a system that I have looked at, which is second-order  
Peano Arithmetic without the Successor Axiom, for instance with this  
axiomatization:

(a)  (n)(m)(m')(Nn & Sn,m & Sn,m' => m = m')
(b)  (n)(m)(n')(Nn & Nn' & Sn,m & Sn',m => n = n')
(c)  (n)(Nn => not Sn,0)
(d)  Induction schema.

See http://www.andrewboucher.com/papers/arith-succ.pdf.


>
> I had to admit that I did not know the answer to this question, but  
> that
> it seemed unlikely to me. It seems that just to formalize the sentence
> "i'm consistent" one would need a lot of coding techniques, which  
> in their
> turn would require the fact that the formal system under scrutiny has
> elementary arithmetic inside it.
>

I think you are in good company with this intuitive argument.  Here's  
why it does not hold.   Predicates like Proof(x,y) can be defined by  
referencing only numbers less than or equal to x and y.  One  
therefore does not need the Successor Axiom which says that every  
number has a successor, which ensures that for every number there  
exist greater numbers; one only needs the fact that, given any  
number, there exist smaller numbers.  So one does not need all of the  
Peano Axioms in order to set up coding.  In brief, while elementary  
arithmetic may be needed for coding, Peano Arithmetic is more than  
the elementary required.