Timeline for Are there "typical" formal systems that have mutual consistency proofs? How long a chain of these can we build?
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 16, 2021 at 19:35 | vote | accept | krzysz00 | ||
| Jan 16, 2021 at 8:56 | comment | added | Emil Jeřábek | BTW, alternatatively, one can formalize the following argument with a little effort: if $T\vdash Q+\mathrm{Con}_S$ and $S\vdash Q+\mathrm{Con}_T$, then $U=T\cap S$ satisfies $U\vdash Q+\mathrm{Con}_U$, hence $U$ is inconsistent, hence so are $T$ and $S$. | |
| Jan 16, 2021 at 8:53 | comment | added | Emil Jeřábek | See Pudlák, Cuts consistency statements and interpretations, JSL 1985, or the last chapter of Hájek&Pudlák. I believe I already wrote this many times on Mathoverflow. | |
| Jan 16, 2021 at 7:50 | comment | added | Noah Schweber | @EmilJeřábek I'm not familiar with those same tricks - do you have a reference? (All my proof theory has been absorbed from mathoverflow and random snatches of overheard conversation. (That's less of a joke than it should be.)) That said, I've edited to acknowledge your comment. | |
| Jan 16, 2021 at 7:49 | history | edited | Noah Schweber | CC BY-SA 4.0 |
deleted 220 characters in body
|
| Jan 16, 2021 at 7:32 | comment | added | Emil Jeřábek | With all questions about provability of consistency statements, the answer is always the same: yes, it works already for $Q$. Use the same tricks as always. (Pass to a cut satisfying $S^1_2$, use provable $\exists\Sigma^b_1$-completeness in $S^1_2$. The provability predicates are $\exists\Sigma^b_1$ as the theories can be assumed finitely axiomatized.) | |
| Jan 16, 2021 at 5:34 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
Typo affecting math formatting
|
| Jan 16, 2021 at 5:30 | comment | added | David Roberts♦ | @LSpice I did consider this. But I think leaving it here to show how it was removed amicably is an important lesson in how MO can be made a better place. | |
| Jan 16, 2021 at 5:13 | comment | added | LSpice | @DavidRoberts and @NoahSchweber, since these comments draw attention to material with whose removal all are happy, maybe they (together with mine) should be deleted? | |
| Jan 16, 2021 at 4:46 | comment | added | David Roberts♦ | ^_^ It's the little things that help people feel welcome! | |
| Jan 16, 2021 at 4:45 | history | edited | Noah Schweber | CC BY-SA 4.0 |
deleted 149 characters in body
|
| Jan 16, 2021 at 4:45 | comment | added | Noah Schweber | @DavidRoberts Fair enough, I certainly didn't mean it to become a big deal. | |
| Jan 16, 2021 at 4:44 | comment | added | David Roberts♦ | OK, thanks. It probably would have been better as a comment first (minus the "barely") before you wrote your answer. By now, with three answers, I don't think people are going to start downvoting now in any case, so why wait until tomorrow? | |
| Jan 16, 2021 at 4:41 | comment | added | Noah Schweber | @DavidRoberts It looks like I overreacted; I was expecting a quick negative reaction to this question, and I wanted to preempt it. If this hasn't become a downvote magnet by tomorrow, I'll remove that line. | |
| Jan 16, 2021 at 4:07 | history | answered | Noah Schweber | CC BY-SA 4.0 |