Timeline for The relation between $\Pi_1$-Foundation and $\Sigma_1$-Foundation over Kripke-Platek set theory
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 29, 2023 at 20:10 | history | edited | Farmer S | CC BY-SA 4.0 |
Made major changes handling mistake in earlier version
|
| Mar 29, 2023 at 20:02 | comment | added | Fedor Pakhomov | @HanulJeon It could not prove existence of even $L_1$. | |
| Mar 29, 2023 at 16:15 | comment | added | Hanul Jeon | @FedorPakhomov Thank you for your answer. It looks like to me that RRST cannot prove the L-hierarchy is definable. Am I correct? | |
| Mar 29, 2023 at 8:50 | comment | added | Fedor Pakhomov | @HanulJeon Sorry wasn't very precise there. $\mathsf{RRST}$ should be $B_0^\mathsf{set}+\mathsf{TC}+\mathsf{Regularity}$, where $B_0^\mathsf{set}$ is from Simpson's book and is axiomatized by Extensionality, Infinity, and the axioms of Rudimentary Closure. The hierarchy $L_\alpha(x)=\mathsf{TC}(x)\cup\{x\}\cup\bigcup\limits_{\beta<\alpha}\{y\mid y \text{ is first-order definable in }L_{\beta}(x)\}$. | |
| Mar 29, 2023 at 0:04 | comment | added | Hanul Jeon | @FedorPakhomov What does $\mathsf{RRST}$ stand for? Is it a variation of the Rudimentary set theory with Rudimentary Recursion? | |
| Mar 28, 2023 at 18:51 | comment | added | Fedor Pakhomov | @HanulJeon Deriving $\mathsf{TC}$ from $\mathsf{KP}_{\omega_0}+\Sigma_1\textsf{-Ind}$ is not a problem. For any $x$, by $\Sigma_1$-induction on naturals you could prove that for each $n$ there is a set $y_n$ consising of pairs $\langle m,z\rangle$, $m\le n$ such that $(y_n)_0=\{z\mid \langle 0,z\rangle\in y\}$ is equal to $x$, and for $m<n$, $(y_n)_{m+1}=\{z\mid \exists w\in (y_n)_m(z\in w)\}$. Then you simply apply collection to $\omega$ to obtain the set of all $y_n$ and then obtain the transitive closure as $\bigcup\limits_{n<\omega,m<\omega}(y_n)_m$. | |
| Mar 28, 2023 at 14:12 | comment | added | Fedor Pakhomov | However, I think that a version of this argument shows that $\mathsf{KP}_{\omega_0}+\Sigma_1\textsf{-Ind}_\omega$ implies $\Pi_1\textsf{-Ind}$ in $L$ and thus $\mathsf{KP}_{\omega_0}+\Pi_1\textsf{-Ind}$ is an extension of $\mathsf{KP}_{\omega_0}+\Sigma_1\textsf{-Ind}_\omega$ of the same consistency strength. And it should be easy to show that their $\Pi_2$-consequences are exactly the $\Pi_2$-consequences of $\mathsf{RRST}+\{\forall x\exists L_{\alpha}(x)\mid \alpha<\omega^\omega\}$, which makes their consistency strength much weaker than that of $\mathsf{KP}_{\omega_0}+\Sigma_1\textsf{-Ind}$. | |
| Mar 28, 2023 at 14:00 | comment | added | Fedor Pakhomov | Interesting argument. Though I pretty much sure that it does not work in $\mathsf{KP}_{\omega_0}$. The problem is that $\mathsf{KP}_{\omega_0}$ doesn't prove $\Sigma_1$-recursion. And consistency strengths don't match: the $\mathsf{KP}_{\omega_0}$ is $\Pi_2$-conservative over Rudimetary Recursive Set Theory with infinity whose minimal constructive model is $L_{\omega 2}$. And over $\mathsf{KP}_{\omega_0}$, $\Pi_1$ membership induction implies $\Pi_1$-induction on natural, which in turn implies $\Sigma_1$-induction on naturals and the latter implies the existence of the ordinal $\omega 2$. | |
| Mar 27, 2023 at 3:53 | comment | added | Hanul Jeon | Even if we assume the existence of the transitive closure as a separate axiom, we need to check whether $L$ is definable from $\Delta_0$-induction (to $\Delta_0$-formulas.) The other issue is that whether $\mathsf{KP\omega}_0$ proves if we have $L$, then $L$ satisfies $\mathsf{KP\omega}_0$. I guess the proof in Matthews-Rathjen should work, but I am not sure. Despite that, your proof is interesting as it still shows $\mathsf{KP\omega}_0$ + $\Sigma_1$-Induction + Transitive Closure proves $L$ satisfies $\Pi_1$-Induction, which seems new. | |
| Mar 27, 2023 at 3:53 | comment | added | Hanul Jeon | Thank you for your answer, but I have a question about your answer; How can we ensure $\mathsf{KP\omega}_0$ proves $L$ is definable? The $L$-hierarchy is defined recursively and requires at least $\Sigma$-Recursion. I used to thought $\Sigma$-Recursion is provable from $\mathsf{KP\omega}_0$ with $\Sigma_1$-Induction, but a typical proof for $\Sigma$-Recursion uses TC-Recursion on $\Sigma$-formulas, and the existence of TC uses $\Pi_1$-Induction. (cf. Theorem I.6.1 of Barwise.) | |
| Mar 27, 2023 at 2:28 | history | answered | Farmer S | CC BY-SA 4.0 |