Timeline for Show that Z2 is not conservative over PA
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 26, 2014 at 1:12 | comment | added | Benedict Eastaugh | @A.C. try Takeuti's book Proof Theory (second edition). He refers to $\mathsf{ACA}$ as $\mathbf{S}^2$. The system Carl has talked about ($\mathsf{ACA}_0 + \Sigma^1_1\text{-}\mathsf{IND}$) is referred to as $\mathbf{S}^1$. | |
| Jan 26, 2014 at 0:33 | comment | added | Carl Mummert | @A.C.: your summary seems reasonable. The references for ACA tend to be older, and in proof-theory literature rather than the reverse mathematics literature. Feferman's article in the Handbook of Mathematical Logic should have something, I think. | |
| Jan 26, 2014 at 0:29 | comment | added | Carl Mummert | @François: yes, it is enough in addition to $\mathsf{ACA}_0$. All you need is "for all $n$ there is a truth set for $\Sigma^0_n$ formulas without set parameters", i.e. a fragment of $\mathsf{ACA}_0'$. The claim is that this proves that $\mathbb{N}$ satisfies PA, and then Con(PA) follows from the completeness theorem and $0\not=1$. The proof is by cases; only induction is interesting; given a coded formula $\phi(n)$ for an instance of induction in PA, we may form the truth set for $\phi$ by assumption, and then use normal set induction to verify that $\mathbb{N}$ satisfies that instance. | |
| Jan 25, 2014 at 23:42 | comment | added | François G. Dorais | Very nice. Do you know how much induction you really need to prove Con(PA)? Is $\Sigma^1_1$-induction enough? | |
| Jan 25, 2014 at 23:04 | comment | added | A.C. | Ah, OK. Repeating this back to make sure I have it right: The only reason we need impredicative sets in the proof of Con(PA) is so that we can use them with the induction axiom, which in $\mathsf{Z}_2$ is written in terms of sets. You're saying that we can bypass the set definition as long as we're able to perform induction on that second-order formula directly. Could you link to any references on ACA? I can't find it in the Simpson book (Subsystems of Second Order Arithmetic). | |
| Jan 25, 2014 at 22:00 | comment | added | Carl Mummert | In fact Con(PA) is provable in systems quite weaker than $\mathsf{ATR}_0$; once you have the satisfaction predicate for first-order sentences, the rest can be done in $\mathsf{ACA}_0$. | |
| Jan 25, 2014 at 21:57 | history | answered | Carl Mummert | CC BY-SA 3.0 |