[FOM] Provability of Consistency

[Richard Kimberly Heck]

On 3/31/19 8:31 PM, Andrei Popescu wrote:
> Where I disagree with Till is in that I don't see the need of
> second-order arithmetic for proving (2). Isn't (first-order) PA
> sufficient? The informal finitistic proof of (2) given in the paper
> suggests that it can be turned into: PA |- forall x, "PA |- ConS(PA)_x".

The proof does not go through in PA as stated. It requires deploying a
different partial truth-predicate depending upon the maximum complexity
of formulas that occur in a given proof. I.e., trying to formalize it in
PA would mean thinking we had truth-predicates Tr_n, for variable n,
which we do not. What Artemov gives us is just a proof *schema*. But, so
far as I can see, there is nothing new in the observation that we can
re-construe the usual proofs (in PA) that I\Sigma_n is consistent in
that way. I.e.: Every PA-proof is a proof in some I\Sigma_n. But PA
proves that I\Sigma_n is consistent. So no PA-proof is a proof of 0=1.
How does what Artemov says at the end of section 5 not apply just as
well to that argument?


For essentially that same reason, it is consistent with PA that, for
some n, I\Sigma_n is not consistent. (Because PA *can* prove that every
PA-proof is a proof in some I\Sigma_n.) Hence, PA does *not* prove the
sentence mentioned above.


There may well be some notion of 'schematic proof' here that is worth
exploring. But then what Hilbert needs is a proof, in that 'schematic'
system (which would be stronger than PA), that *that system* is
consistent, not just that PA is. I've explored some systems like this
myself [1], but I'm not sure how much help that would be here.


Riki


[1] http://rkheck.frege.org/pdf/published/LogicOfFregesTheorem.pdf


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190401/68d01fc8/attachment-0001.html>