Timeline for Can the "real" Peano Arithmetic be inconsistent?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 6, 2017 at 0:36 | comment | added | Ruizhi Yang | @EmilJeřábek Great remark! The example you gave perfectly addresses my concern. | |
| May 5, 2017 at 13:58 | vote | accept | Ruizhi Yang | ||
| May 5, 2017 at 7:48 | comment | added | Emil Jeřábek | @ganganray PA proves the consistency of each its (standard) finite part. So, a proof of contradiction in PA in a model of PA must necessarily use nonstandard axioms of PA. But in general, it is perfectly possible to have nonstandard proofs using only standard axioms. For example, consider a model of $I\Sigma_1+\neg \mathrm{Con}(I\Sigma_1)$ (using its finite axiomatization). Since the theory is finitely axiomatized, all axioms in the proof of contradiction are standard, but the proof must be nonstandard. | |
| May 5, 2017 at 3:28 | comment | added | Ruizhi Yang | Thank you for pointing out that the Feferman-style of PA works! I am not sure if I fully understand your find remark. Is it possible to have a proof using only standard axioms but with nonstandard number of steps, and cannot be shrunk back to a standard proof of the same sentence? Am I right that such a proof can only make use of finitely many standard axioms, since it cannot use exactly $\omega$ many standard axioms, and if it uses nonstandard number of axioms, there must be some nonstandard one? Is that why such a proof does not exist? | |
| May 5, 2017 at 2:20 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |