Timeline for Is Monsky's theorem provable in $\mathsf{RCA}_0$?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 12, 2022 at 2:32 | answer | added | Qiaochu Yuan | timeline score: 10 | |
| Oct 12, 2022 at 2:18 | comment | added | François G. Dorais | @GerryMyerson But we can make guesses at the outset so long as one of the guesses must be right. In $\mathsf{RCA}_0$, we're allowed finitely many guesses because of the law of excluded middle. | |
| Oct 12, 2022 at 2:13 | comment | added | Gerry Myerson | We don't know whether $e$ and $\pi$ are algebraically independent. We don't even know whether $e+\pi$ is irrational. | |
| Oct 12, 2022 at 2:11 | comment | added | François G. Dorais | PS: The reason I think the algebraic case is easier is that $\mathbb{Q}(t_1,\ldots,t_k)$ is then a finite dimensional vector space over $\mathbb{Q}$ and the possibilities positive cone in that space could be determined by finitely many guesses. | |
| Oct 12, 2022 at 1:53 | comment | added | François G. Dorais | It's pretty late here for me to try to work this out and, to be honest, any one of these four steps could fail upon further investigation. | |
| Oct 12, 2022 at 1:51 | comment | added | François G. Dorais | The fourth and final idea is that some conservation result for $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$ will allow to conclude the result over $\mathsf{RCA}_0$. | |
| Oct 12, 2022 at 1:49 | comment | added | François G. Dorais | The third idea is that in $\mathsf{WKL}_0$ we can actually make infinitely guesses in a progressive manner. More technically, if $t_1,t_2,\ldots,t_k$ are fixed real numbers the decision procedure we need is a $\Pi^0_1$ singleton. [continued] | |
| Oct 12, 2022 at 1:46 | comment | added | François G. Dorais | The second idea is that we may be able to guess the correct decision procedure with finitely many choices. I think this is true (but not at all obvious) if the $t$s are algebraic but I don't think this is true if we allow transcendentals. [continued] | |
| Oct 12, 2022 at 1:42 | comment | added | François G. Dorais | The first idea is that Monsky's argument works fine for a finitely generated real extension $\mathbb{Q}(t_1,t_2,\ldots,t_k)$ provided we have a decision procedure for which polynomial inequalities are true. (There is no requirement for the $t$s to be algebraic, as Qiaochu suggested, but that does help for the decision process.) [continued] | |
| Oct 12, 2022 at 1:39 | comment | added | François G. Dorais | Yeah, I think I must have reversed quantifiers due to bad memory. Anyway, I think I have an argument that might work but it's not fully fleshed out... | |
| Oct 12, 2022 at 1:01 | comment | added | Timothy Chow | @FrançoisG.Dorais That doesn't sound right to me. See for example the paper by Richter-Gebert and Ziegler, Realization spaces of 4-polytopes are universal. To realize all 4-polytopes, you need all algebraic numbers, but I don't think you ever need transcendental numbers. Qiaochu's argument sounds convincing to me, but can that claim be proved in $\mathsf{RCA}_0$? | |
| Oct 11, 2022 at 23:51 | comment | added | François G. Dorais | @QiaochuYuan I'm almost surely remembering incorrectly but isn't there a counterexample by Micha Perles that such reasoning is not always correct? I'm thinking of some kind of finite combinatorial configuration that can be realized in $\mathbb{R}^n$ but cannot be realized in $K^n$ for any finite extension $K$ of $\mathbb{Q}$. | |
| Oct 11, 2022 at 23:29 | comment | added | Qiaochu Yuan | Isn't the question of whether such a dissection exists consisting of a fixed number $n$ of triangles equivalent to a first-order statement in the language of real closed fields? If so that would imply that if a dissection exists then a dissection exists with all coordinates algebraic (assuming the square's coordinates are algebraic), right? | |
| Oct 11, 2022 at 23:14 | history | asked | Timothy Chow | CC BY-SA 4.0 |