Helene.Boucher at wanadoo.fr
Mon Nov 6 16:13:22 EST 2006
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
There is also a system that I have looked at, which is second-order
Peano Arithmetic without the Successor Axiom, for instance with this
(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.
> I had to admit that I did not know the answer to this question, but
> 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.
More information about the FOM