Is it true that if "for all x P(x)" is unprovable in pA then the complexity of the proof of P(n) becomes greater as n grows bigger?
$\begingroup$
$\endgroup$
5
-
$\begingroup$ I assume that by pA you mean Peano arithmetic. Also, you probably assume that every instance P(n) is provable in PA. Can you elaborate what you mean by the complexity of a proof? $\endgroup$– Stefan GeschkeCommented Sep 29, 2014 at 13:05
-
$\begingroup$ Yes to both questions. $\endgroup$– Anders GöranssonCommented Sep 29, 2014 at 13:07
-
3$\begingroup$ Could you tell what measure of proof complexity you are using? Also, couldn't it easily be that $P(n)$ is trivial when $n$ is even, but not when $n$ is odd, in which case you have very easy proofs for very large even $n$, in which case it wouldn't be true that all larger $n$ have only more complex proofs. $\endgroup$– Joel David HamkinsCommented Sep 29, 2014 at 13:08
-
$\begingroup$ I think Anders means that the "complexity" (to be clarified) of proofs of P(n) is unbounded if $\forall xP(x)$ is unprovable in PA and every instance P(n) is provable in PA. $\endgroup$– Stefan GeschkeCommented Sep 29, 2014 at 13:13
-
$\begingroup$ Presumably you're using a model of "complexity" where the complexity of any natural number is bounded, otherwise you don't need the "if" clause: assuming $P(n)$ contains $n$, simply to state $P(n)$ requires an unbounded number of bits as $n$ gets large. $\endgroup$– Robert IsraelCommented Sep 29, 2014 at 19:27
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
2
You didn’t specify what you mean by “complexity”. If one interprets it as the number of lines in the proof, this is a famous conjecture of Kreisel (usually stated contrapositively: if there is a constant $c$ such that $\phi(\overline n)$ has a PA proof with at most $c$ lines for all $n$, then PA proves $\forall x\,\phi(x)$).
Kreisel’s conjecture is still open for the most natural formulation of PA, however it is extremely sensitive to the choice of the language, and various variants of it have been proved and disproved. See Hrubeš for a recent paper in the positive direction, where you can also find pointers to other known results related to the conjecture.
answered Sep 29, 2014 at 13:18
-
$\begingroup$ Thank you, I heard something along these lines (which I tried to formulate), a while ago from a logician and now I believe that what you write above must be what he had in mind. I will look at the paper. $\endgroup$ Commented Sep 29, 2014 at 13:33
-
$\begingroup$ Here is also a survey article: link.springer.com/article/10.1007%2Fs10958-009-9408-0 $\endgroup$ Commented Sep 29, 2014 at 13:45
$\begingroup$
$\endgroup$
3
Consider the assertion $P(x)$ that asserts "$x$ is not the Gödel code of a proof of a contradiction in PA". If PA is consistent, then we can prove $P(n)$ for any particular natural number $n$, since no such $n$ codes a proof. I don't know what is your measure of proof complexity, but the proof of $P(n)$ in every case is mundane: it is because the sequence coded by $n$ violates one of the syntactic requirements of being a proof. Namely, one of the sequents is not an axiom, or does not follow by modus ponens from the earlier sequents, or the conclusion is not a contradiction, and so on. In particular, the formulas appearing in the proofs of $P(n)$ have bounded complexity (although these proofs do get longer, since one must check more cases to cover the earlier sequents). But meanwhile, the assertion $\forall x\, P(x)$ is independent.
answered Sep 29, 2014 at 13:18
-
$\begingroup$ It looks to me like the first example shows that the length of proofs of $P(n)$ can grow quite slowly (something like polynomial in $\log n$, I think) even while $\forall x : P(x)$ is independent. That's something I didn't know, so I appreciate your answer for this reason. $\endgroup$ Commented Sep 29, 2014 at 14:33
-
1$\begingroup$ Yes, I think that is right, since $n$ codes a sequence about length $\log n$. It seems to me, further, that one can push this much slower even, by modifying $P(n)$ to require a bunch of irrelevant padding, so that the extra checking is not required beyond something much further less than $n$. $\endgroup$ Commented Sep 29, 2014 at 14:40
-
2$\begingroup$ See users.math.cas.cz/~pudlak/fin-con.pdf . $\endgroup$ Commented Sep 29, 2014 at 15:51