Timeline for Soundness Theorem in reverse mathematics
Current License: CC BY-SA 2.5
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 16, 2011 at 23:16 | history | edited | user5810 | CC BY-SA 2.5 |
expressed myself better
|
| Jan 16, 2011 at 21:59 | history | edited | user5810 | CC BY-SA 2.5 |
inserted one more )
|
| Jan 16, 2011 at 21:48 | vote | accept | CommunityBot | ||
| Jan 16, 2011 at 10:49 | answer | added | François G. Dorais | timeline score: 5 | |
| Jan 16, 2011 at 10:23 | comment | added | user5810 | I think your point is that $ACA_0^+$ is strong enough to form the truth set for the model, because I think $ACA_0$ can "comprehend the truth predicate" for the model. Furthermore, it's not obvious (to me) that $ACA_0^+$ doesn't prove $\Delta_1^1$ induction. Is there an online reference? | |
| Jan 16, 2011 at 9:32 | comment | added | François G. Dorais | I don't think STPL proves $\Delta^1_1$-induction, since it looks like STPL is provable in $ACA_0^+$. (Because $ACA_0^+$ is strong enough to comprehend the truth predicate for a model.) | |
| Jan 16, 2011 at 7:25 | comment | added | user5810 | About the rest of Daniel's comment, a truth predicate has to be for all (codes of) first-order formulas, not just atomic formulas. | |
| Jan 16, 2011 at 7:24 | comment | added | Ed Dean | Somewhat along the lines of Daniel's comment: some forms of STPL, at least, are provable already in RCA0 (as in II.8 of Simpson's SOSOA). | |
| Jan 16, 2011 at 7:22 | history | edited | user5810 | CC BY-SA 2.5 |
changed "arithmetical formulas" to "first-order structures"
|
| Jan 16, 2011 at 7:20 | comment | added | user5810 | Excellent point re arithmetic. (fixing that now) | |
| Jan 16, 2011 at 7:19 | comment | added | Daniel Mehkeri | Would you need the truth predicate for arithmetic? I haven't thought carefully about what STPL would really look like in the language of second-order arithmetic, but aren't the extralogic symbols given as sets? I.e it only needs a truth predicate for logical symbols plus some extra symbols, not successor, addition, multiplication. This sounds like it ought to be simpler than Delta-1-1. | |
| Jan 16, 2011 at 6:33 | history | asked | user5810 | CC BY-SA 2.5 |