[FOM] Provability of Consistency

[Andrei Popescu]

Dear Riki,

Thank you for the clear explanation for why my impression that this argument could be formalized in PA was wrong. (I had not ignored the truth predicates, but had wrongly believed that their behavior could be "inlined" in an inductive proof. Now I see the fundamental limitation.)

Best wishes,

Andrei

________________________________
From: Richard Kimberly Heck <richard_heck at brown.edu>
Sent: 01 April 2019 17:52
To: Foundations of Mathematics; Andrei Popescu
Subject: Re: [FOM] Provability of Consistency

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<https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Frkheck.frege.org%2Fpdf%2Fpublished%2FLogicOfFregesTheorem.pdf&data=02%7C01%7CA.Popescu%40mdx.ac.uk%7C912b56fde2494cd836d908d6b6c256ba%7C38e37b88a3a148cf9f056537427fed24%7C0%7C1%7C636897343131907058&sdata=pQ%2FiET8eQC2Y5y89Tyzg0MphLM84mwwK6L612s3ns%2Bk%3D&reserved=0>

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