Timeline for Transfinitely extending $\sf PA$ — can we get stronger than $\sf ZFC$?
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 16, 2014 at 15:36 | vote | accept | Vladimir Reshetnikov | ||
| Jun 13, 2014 at 0:20 | answer | added | Noah Schweber | timeline score: 8 | |
| Jun 13, 2014 at 0:05 | comment | added | Vladimir Reshetnikov | @AlexGavrilov There is a certain difference between the soundness axiom schema and the single axiom of consistency. Imagine a pure formalist (I'm not) who rejects any meaning of mathematical symbols and accepts a statement as a theorem only when a full formal proof is presented. Suppose he formally proved in $\sf PA$ that a certain statement $S$ has a formal proof in $\sf PA$. Because he does not assign any meaning (let alone truth) to what he just proved, he cannot use it as a substitute for a proof of $S$. But if he works in $\sf PA_1$, the soundness schema immediately yields a proof of $S$. | |
| Jun 12, 2014 at 23:46 | history | edited | Vladimir Reshetnikov | CC BY-SA 3.0 |
Update: Dealing with the ambiguity in my definition
|
| Jun 12, 2014 at 23:04 | comment | added | Vladimir Reshetnikov | @AlexGavrilov $\sf PA_\omega$ contains all axioms of all $\sf PA_n$ for $n\in\omega$. So, it asserts that all theorems of $\sf PA$ are true, and if we add this as a new axiom to get $\sf PA_1$, then all its theorems are true, and if we add this as a new axiom to get $\sf PA_2$, then all its theorems are true, and if we repeat this step any finite number of times to get $\sf PA_n$, then all its theorems are also true (this is not a quantified statement, but an axiom schema). It's still a decidable problem to check if a wff is an axiom of $\sf PA_\omega$, so it is recursively axiomatizable. | |
| Jun 12, 2014 at 4:33 | comment | added | Alex Gavrilov | By the way, what is $PA_{\omega}$? I am curious. | |
| Jun 11, 2014 at 16:43 | history | edited | Vladimir Reshetnikov | CC BY-SA 3.0 |
fixing an axiom
|
| Jun 11, 2014 at 15:40 | comment | added | François G. Dorais | @Alex: I think the OP is expressing a reflection principle or perhaps a soundness property rather than just iterated consistency. | |
| Jun 11, 2014 at 15:33 | comment | added | François G. Dorais | Note that your theories $\mathsf{PA}_\alpha$ are not entirely well-defined, as explained in this earlier question. This probably answers Question 1. | |
| Jun 11, 2014 at 14:59 | comment | added | Alex Gavrilov | If you take for $\Phi$ a false statement, then the axiom simply states that $T$ is consistent. So, actually there is no need for a schema of axioms, one is enough. | |
| Jun 11, 2014 at 13:18 | comment | added | Joel David Hamkins | @PhilipWelch I would suggest that your comment should be an answer. | |
| Jun 11, 2014 at 11:25 | comment | added | Emil Jeřábek | You got the axioms wrong: the theory you described has a one-point model, and as such it is much weaker than PA. You need to replace the last but one axiom with $a+1\ne0$. | |
| Jun 11, 2014 at 6:09 | comment | added | Piotr Shatalin | There could be nothing wrong with saying that everything $PA$ proves is true. This is what most mathematicians believe anyway. But, of course, $PA$ itself cannot prove it, because it implies its consistency (something that a consistent theory cannot prove about itself). | |
| Jun 11, 2014 at 5:58 | comment | added | Philip Welch | @Vladimir There is a whole literature on this kind of thing, initiated by Turing and carried on by Feferman. A huge amount of care is needed to get this formalised correctly. A good place to start looking is T. Franzen "Inexhaustibility", ASL Lecture Notes in Logic, vol.16. | |
| Jun 11, 2014 at 4:51 | history | asked | Vladimir Reshetnikov | CC BY-SA 3.0 |