Timeline for A Question related to the Formula Hierarchy
Current License: CC BY-SA 3.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 30, 2014 at 14:38 | vote | accept | Frode Alfson Bjørdal | ||
| Oct 30, 2014 at 13:21 | comment | added | François G. Dorais | @EmilJeřábek: Indeed, for strict $\Sigma^1_1$-formulas of the form $\exists X\phi(X,n)$ where $\phi(X,n)$ is $\Pi^0_1$, choice follows from $\mathsf{WKL}_0$. Additionally, if $\phi(X,n)$ is $\Sigma^0_2$ then choice follows from $\mathsf{ACA}_0$. The general case is when $\phi(X,n)$ is $\Pi^0_2$ (the complexity of saying that a set is the graph of a total function). | |
| Oct 30, 2014 at 11:26 | comment | added | Emil Jeřábek | I should say that I was ignoring the requirement on the complexity of $\alpha$; the speculation that the formula may not be $\Pi^1_2$ without $\Sigma^1_1$-AC was supposed to apply to arbitrary arithmetic $\alpha$ (though $\Sigma^0_2$ should suffice). As shown in François’s answer, this makes a lot of difference. | |
| Oct 30, 2014 at 1:43 | answer | added | François G. Dorais | timeline score: 4 | |
| Oct 29, 2014 at 23:19 | comment | added | Frode Alfson Bjørdal | Let us continue this discussion in chat. | |
| Oct 29, 2014 at 20:44 | comment | added | Emil Jeřábek | Let me put it more clearly: these formulas are certainly $\Pi^1_3$ with almost no assumptions on the base theory, as one can simulate number quantifiers by set quantifiers. They are probably not in general $\Pi^1_2$ (or even $\Pi^1_1$) unless the base theory is sufficiently strong, but this requires proof. | |
| Oct 29, 2014 at 18:50 | comment | added | Frode Alfson Bjørdal | For the record and to make issues comprehensible, I deleted a question which Emil related to and which asked whether his "only" could be replaced by something like "even". | |
| Oct 29, 2014 at 17:48 | comment | added | Frode Alfson Bjørdal | It is in the context of a modal ontological argument I have developed, with roots in the work of Gödel and others - including myself. (Details on request.) The complexity issue will only figure as an incidental remark, and the matters are of course further complexified by the presupposition of a second order $modal$ machinery. I guess my association mentioned below to Skolem is to the point? | |
| Oct 29, 2014 at 17:37 | comment | added | Emil Jeřábek | “Where” = “in which theory do you need the formula to be proven equivalent to something of a particular complexity”. Regarding the second comment, I’d rather leave that to someone familiar with subsystems of second-order arithmetic, however, I assume so by analogy with the corresponding question in the arithmetic hierarchy: no true $\Pi_2$-axiomatized theory can prove that all $\forall\exists\forall\Delta_0$ formulas with the existential quantifier bounded are equivalent to $\Pi_2$ formulas (whereas $B\Sigma_1$ proves they are $\Pi_1$). | |
| Oct 29, 2014 at 17:25 | vote | accept | Frode Alfson Bjørdal | ||
| Oct 30, 2014 at 14:38 | |||||
| Oct 29, 2014 at 17:12 | comment | added | Frode Alfson Bjørdal | @Emil I do not understand the import of the question for location. | |
| Oct 29, 2014 at 17:04 | comment | added | Emil Jeřábek | Where? It’s $\Pi^1_1$ if you have $\Sigma^1_1$-AC, but only $\Pi^1_3$ otherwise. | |
| Oct 29, 2014 at 16:58 | answer | added | Noah Schweber | timeline score: 7 | |
| Oct 29, 2014 at 16:28 | history | asked | Frode Alfson Bjørdal | CC BY-SA 3.0 |