Loeb’s theorem shows that if PA proves “not P(C)->C”, then PA proves C (using P(X) for “X is provable in PA”).
It follows from that, using the Deduction Theorem, that PA proves “(not P(C)->C)->C”; it does not follow
that “(not P(C)->C)->C” is a logical tautology.
From that, you obtain, similarly, that PA proves “(not P(C)) → C”. And you say “I cannot prove that 2 = 1″. Sure,
you cannot, but can PA? That’s the real question.
There’s nothing particularly surprising about PA proving “(not P(C))->C”. After all, were PA to prove “not P(C)”
for any C, it would prove its own consistency, and therefore be inconsistent, and therefore prove C.
Loeb’s theorem shows that if PA proves “not P(C)->C”, then PA proves C (using P(X) for “X is provable in PA”).
It follows from that, using the Deduction Theorem, that PA proves “(not P(C)->C)->C”; it does not follow that “(not P(C)->C)->C” is a logical tautology.
From that, you obtain, similarly, that PA proves “(not P(C)) → C”. And you say “I cannot prove that 2 = 1″. Sure, you cannot, but can PA? That’s the real question.
There’s nothing particularly surprising about PA proving “(not P(C))->C”. After all, were PA to prove “not P(C)” for any C, it would prove its own consistency, and therefore be inconsistent, and therefore prove C.