Logic

Is it impossible that there be two recursive sets T and T* of axioms (in the same language) such that their closures under the same recursive set of recursive rules is identical and yet there is no recursive proof of this fact? It seems impossible but a simple proof of this fact would help elucidate matters!

Comments

To decide whether T and T* have the same deductive closure involves deciding whether the axioms of T* are deducible in T. That, in general, will require have a decision procedure for determining whether a given sentence is a deductive consequence of T. But theoremhood in T could be recursively undecidable.

Perhaps what's confusing here is one of these each-all things that permeates this whole area. If T and T* have the same theorems, then EACH axiom of T will be provable in T*, and EACH axiom of T* will be provable in T, and of course it follows that there is, as a matter of fact, an algorithmic way of generating precisely those proofs. There is no general reason, however, to suppose that we will be able to prove that EVERY axiom of T is provable in T* nor that EVERY axiom of T* is provable in T. This is the same sort of contrast as between: PA proves EACH statement of the form: n is not a proof of 0=1; but PA does NOT prove: For all n, n is not a proof of 0=1.

Here are a couple ways of spelling out Peter's earlier remark.

The first starts from the fact that S is a theorem of T iff T∪{¬S} is inconsistent. If T is a recursive set of axioms, then of course so is T∪{¬S}. To check if S is a theorem of T, then, you just need to see if T∪{¬S} has the same theorems as some known inconsistent theory. So if you could, in general, decide whether recursive theories prove the same theorems, you could decide whether an arbitrary sentence was a theorem of such a theory, which you can't, since there are undecidable theories. Note that this also shows that, if you could decide whether two theories have the same theorems, you could decide whether an arbitrary theory is consistent. But, in response, one might try restricting the claim to consistent theories.

So begin instead with the fact that S is a theorem of T iff the theory T∪{S} has the same theorems as T. If T is recursive, so is T∪{S}. So if you could decide whether these prove the same theorems, you could again decide theoremhood. Note that, as a special case, this shows that the decision problem we're discussing would allow us to decide logical truth: To decide whether S is a logical truth, just consider the theories {} and {S}.

I find the original question a little unclear, because I'm not sure what a "recursive proof" is. Peter and Richard have interpreted the question as asking whether or not there is an algorithm to tell, in general, whether or not any given recursive sets of axioms T and T* have the same theorems. This is one possible interpretation, and Richard has given a very nice proof that the answer is no.

But the original question does not seem to be asking about a general solution for all recursive sets of axioms T and T*. Rather, it seems to be asking whether there can be a single pair of recursive sets of axioms T and T* such that T and T* have the same theorems, but this fact is, in some sense, not provable. Let me give an example that might respond to this interpretation.

For each natural number n, let P(n) be the statement "n is not the Godel number of a proof of a contradiction in Zermelo Frankel (ZF) set theory." This is expressible in the language of number theory. Let T be the set of Peano axioms, and the T* be T together with the infinitely many additional axioms P(0), P(1), P(2), ... If ZF is consistent, then for every natural number n, P(n) is true, and in fact it is provable in T. It follows that T and T* have the same theorems. On the other hand, if ZF is inconsistent, then for some n, P(n) is false, and in fact its negation is provable in T. It follows that T* is inconsistent. But T is consistent, since all of the Peano axioms are true of the natural numbers. Therefore T and T* do not have the same theorems. So the following statement is true:

(*) ZF is consistent if and only if T and T* have the same theorems.

Furthermore, the statement (*) is provable in ZF: the argument above establishing (*) can be formalized in ZF.

Now, suppose that ZF is consistent. Then by (*), T and T* have the same theorems. But if this fact were provable in ZF then, since (*) is also provable in ZF, it would follow that the consistency of ZF is provable in ZF, contradicting Godel's second incompleteness theorem. Thus the fact that T and T* have the same theorems is not provable in ZF.

I see the difference, and perhaps you are right about how the question should be interpreted. Of course, what makes it difficult to answer, in that form, is that the term "recursive", in "recursive proof", seems not to be doing any work. Perhaps what is meant is "finite proof" (as opposed to one containing infinitely many steps). But then, as you say, it is not clear what might be meant by asking whether some fact is or is not provable in some absolute sense, rather than in this theory or in that one.

In that regard, it's perhaps worth pointing out explicitly that the argument you gave can be replicated for any extension U of PA. Let PA(U) be PA plus all statements of the form: n is not the Godel number of a U-proof of a contradiction. Then it will be provable in PA (and therefore in U) that PA and PA(U) have the same theorems iff U is consistent, and now the rest of the argument goes through.

We can certainly start with theories even weaker than PA. I do not know how weak we can go.

Yes, I agree, under the alternative interpretation I proposed the word "recursive" in "recursive proof" is doing no work. So my interpretation is not entirely satisfactory either. I don't know which interpretation was meant, but both seem to be interesting questions.

As for the generalization to any extension U of PA: Presumably we're talking about recursive extensions of PA. (Well, we do have that occurrence of the word "recursive" floating around that isn't doing any work; perhaps we can use it here.) But there's one other issue. In my argument, I made use of the fact that the consistency of PA is provable in ZF. But the consistency of PA is not provable in PA, so I don't think it's going to be true in general that you can prove in PA that PA and PA(U) have the same theorems iff U is consistent. But I think you can prove it in the theory PA + Con(PA) (that is, the theory PA with an additional axiom asserting that PA is consistent). So as long as U is strong enough to prove the consistency of PA, the generalization should work.

For example, let U be the extension of PA in which we add the statement "0=1" as an additional axiom. Of course, U is inconsistent. And the inconsistency of U is provable in PA; in fact, there is a particular number n such that one can prove, in PA, that n is the Godel number of a U-proof of a contradiction, so one can prove, in PA, that PA(U) is inconsistent. If one could also prove, in PA, that PA and PA(U) have the same theorems iff U is consistent, then one would be able to prove in PA that PA is consistent, contrary to the incompleteness theorem. So in this case we must not be able to prove the statement "PA and PA(U) have the same theorems iff U is consistent" in PA.

Read another response by Peter Smith, Richard Heck, Daniel J. Velleman

Read another response about Logic