I think everyone is familiar with Goedel's incompleteness theorems. In particular they imply that PA (Peano arithmetic) can not prove its own consistency. Now my question is what is the largest subsystem of PA that "can" prove its own consistency? You definitely can't have the induction axiom but is that enough?
$\begingroup$
$\endgroup$
Add a comment
|
4 Answers
1
-
$\begingroup$ Many thanks for this link, it introduced me to the nice work of Dan Willard. $\endgroup$ Commented Jun 18, 2011 at 15:12
$\begingroup$
$\endgroup$
6
As proved by Pudlák, Gödel's theorem holds in the strong form that no consistent r.e. extension of Robinson's arithmetic $Q$ can prove its own consistency. (Moreover, as shown by Paris and Wilkie, the consistency of $Q$ is not provable even in $I\Delta_0+\exp$.)
answered Jun 18, 2011 at 11:48
-
$\begingroup$ Emil, can you provide a reference for this? I had the feeling that this was proven much earlier. $\endgroup$– KavehCommented Feb 19, 2012 at 18:27
-
1$\begingroup$ The paper I had in mind is Cuts, consistency statements and interpretations, JSL 50 (1985), #2, 423–441 (where Pavel proves something even stronger). I don’t think it was stated before in such a generality. Bezboruah and Shepherdson (Gödel’s second incompleteness theorem for $Q$, JSL 41 (1976), #2, 503–512) show that $Q$, or in fact $PA^-$ (the theory of nonnegative parts of discretely ordered rings) does not prove the consistency of anything. Paris and Wilkie (On the scheme of induction for bounded arithmetic formulas, APAL 35 (1987), 261–302) prove the second Gödel’s incompleteness $\endgroup$ Commented Feb 20, 2012 at 12:11
-
1$\begingroup$ ... theorem for extensions of $I\Delta_0+\Omega_1$, and that $I\Delta_0+\exp\nvdash\mathrm{Con}_Q$. $\endgroup$ Commented Feb 20, 2012 at 12:12
-
$\begingroup$ Thanks and apologies that my comment wasn't clear. I meant "Gödel's theorem holds in the strong form that no consistent r.e. extension of Robinson's arithmetic Q can prove its own consistency". Somehow I feel that it was proven earlier although not in the stronger form that Pavel proved it. (I don't remember where but I might have seen it in Kleene's Metamathematics.) $\endgroup$– KavehCommented Feb 20, 2012 at 23:37
-
1$\begingroup$ @AnduinWilde Yes, but that is more of a curiosity than a useful result. It exploits the weakness of Q to construct a weird model (in which it is quite dubious that Con_Q can be considered to have the intended meaning in the first place), and in particular, their result does not apply to proper extensions of Q, hence it is not in any way a strengthening of the usual Gödel’s second incompleteness theorem. No one really cares if Q itself proves its own consistency. Q is useful as a weak base theory that is included in many theories of interest, and their consistency is what we care about. $\endgroup$ Commented Sep 3, 2023 at 7:25
$\begingroup$
$\endgroup$
First, it's not clear whether you are talking about first-order PA or second-order PA. It seems, because you are mentioning induction as an axiom rather than a schema, that you are talking about second-order PA, but I will answer for a special form of first-order Peano Arithmetic, denoted PA1. The answer for PA2 is similar.
Secondly, it is incorrect to ask what is "the" largest. The answer to your question is: there exists sub-systems of PA which prove their own consistency but there is no largest such sub-system.
Let PA have the language with a constant 0, a one-place predicate N, and a 2-place predicate Sx,y. Usually the axioms of PA1 include axioms for addition and multiplication. I will present a system which has axioms for sequences rather than addition and multiplication; addition and multiplication can then be defined using the notion of sequences. The axioms of PA1 are:
(1) N0
(2) (n)(m)(Nn & Sn,m => Nm)
(3) (n)(Nn => (there exists m) Sn,m)
(4) (n)(m)(m')(Nn & Sn,m & Sn,m' => m = m')
(5) (n)(m)(n')(Nn & Nn' & Sn,m & Sn',m => n = n')
(6) (n)(Nn => not Sn,0)
(7) Induction schema, phi[0\n] & (n)(m)(Nn & Sn,m & phi => phi[m\n]) => (n)(Nn => phi)
(8) For every natural number x, there exists a sequence <(0,x)>
(9) For every sequence f, if Nn & Sn,m & <(m,x)> belongs to f, then <(n,y)> belongs to f for some y
(10) For every sequence f, if Nn & Nm & Ny & Sn,m & <(n,x)> belongs to f, there there exists a sequence g exactly like f except that it may differ at the mth place where <(m,y)> belongs to g
Apologies for the imprecision of (8), (9), and (10), but it's the quickest way for me to write them down here.
Call fpa the system made up of axioms (4) through (10). Then fpa proves its own consistency. It also proves the consistency of fpa + (1) (call this X). So a fortiori X proves its own consistency. fpa also proves the consistency of fpa + (N0 => (2) & (3)), so this latter (call it Y) also proves its own consistency. But any system stronger than both X and Y contains PA1, which can't prove its own consistency. Hence there is no strongest sub-system of PA1 which proves its own consistency.
Please see http://www.andrewboucher.com/papers/fpa.pdf for details.
$\begingroup$
$\endgroup$
1
This answers to this question may be of use - Can any formal system prove its own consistency?
In short, it states that $PA$ is too strong to prove its own consistency, Presburger arithmetic (see Neel Krishnaswami's answer in the link) is too weak (although it is consistent). Other sub-systems like $I\Sigma_1$ can't prove their own consistency. $PA^-$ (PA without induction) I'm not sure about, but I wouldn't expect it to prove its own consistency.
But Paseman's comment is probably most accurate!
An inconsistent sub-system could, but I don't think that's what you're after... ;)
Presburger Arithmetic http://www.cs.albany.edu/~dew/m/jsl1.pdf http://en.wikipedia.org/wiki/Presburger_arithmetic
-
2$\begingroup$ Concerning "an inconsistent subsystem could": Since PA is consistent, it doesn't have inconsistent subsystems. $\endgroup$ Commented Feb 12, 2012 at 23:05