Timeline for Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA?
Current License: CC BY-SA 4.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 9, 2020 at 1:47 | comment | added | Jori | That was a typo, by the way, I meant $I\Sigma_{n+1}$. | |
| Aug 9, 2020 at 1:28 | comment | added | Jori | That's okay. Thank-you for all the help. There is no supervisor and MSE usually doesn't answer in this area. I will definitely look at the paper, I think with a bit of patience I should have the level to process it. I'm not a PhD student btw. Again, thanks for your help. I'm sorry to have bothered you so often. | |
| Aug 8, 2020 at 7:38 | comment | added | Emil Jeřábek | $I\Sigma_n$ is $\Pi_{n+2}$, just count the quantifiers. You would know this if you looked at the Leivant paper in the first place. Concerning the FINAL THING, let $\psi$ be a conjunction of axioms of $I\Delta_0+\mathrm{EXP}$ (which is $\Pi_2$, and enough to verify the properties of $\mathrm{Tr}_n$), and given a $Q$-proof of a $\Sigma_{n+1}$ sentence $\sigma$ (the “$x$”), construct a proof of $\psi\to\mathrm{Tr}_{n+1}(\ulcorner\sigma\urcorner)$, and apply the reflection principle. | |
| Aug 8, 2020 at 1:31 | comment | added | Jori | The final thing I don't understand is why your $\Sigma_{n+1}$ reflection scheme proves $\text{RFN}(\Sigma_{n+1})$ over $I\Sigma_n$? What is the complexity by the way of $I\Sigma_n$? as a single sentence? $\Pi_{n+3}$? | |
| Aug 3, 2020 at 15:39 | comment | added | Jori | Yes, I see. If we know $\phi$ to be false then so must $\psi(t)$, and hence if $\Gamma \implies \Delta, \psi(t)$ is true, one of $\Delta$ must be true, or one of $\Gamma$ be false, but under these conditions $\Gamma \implies \Delta,\phi$ is true, so we remain in good shape. | |
| Aug 3, 2020 at 14:07 | comment | added | Emil Jeřábek | If you hardcode $\phi$ as false, you need $\phi$ to be actually false in order to prove soundness of the inference rules for the induction step. In particular, write $\phi=\exists x\,\psi(x)$, and consider an $\exists$-right inference from $\Gamma\Longrightarrow\Delta,\psi(t)$ to $\Gamma\Longrightarrow\Delta,\phi$. | |
| Aug 3, 2020 at 13:41 | comment | added | Jori | Ah, I see. That clarifies it. It's not about obtaining a proof of the empty sequent, rather on the assumption of $\neg\phi$, you obtain that the empty sequent is true, which by definition of the (adjusted) truth predicate is impossible. Right? I'm trying to think why we need $\neg\phi$ to change the truth definition. It seems we can just "hard code" the falsehood of $\phi$ in it no matter what. | |
| Aug 3, 2020 at 13:18 | comment | added | Jori | By the way, I really really appreciate all your help and comment. Thank you. | |
| Aug 3, 2020 at 13:18 | comment | added | Emil Jeřábek | Valid just means true under all assignments. The last sequent of the proof is $\Longrightarrow\phi$. Under the truth definitoin that fixes $\phi$ as false, or equivalently, that removes it from the succedent of any sequent before checking its truth, this is the same as the empty sequent $\Longrightarrow$. | |
| Aug 3, 2020 at 13:07 | comment | added | Jori | I think I must be confusing some of your terminology: OK, we have a cut free proof of $\implies \phi$, and we can prove (using our $\Pi_n$ truth definition) that all sequent above this are true (what do you mean by valid?), and we have $\neg\phi$ (for contradiction). How does that lead to a prove of the empty sequent? | |
| Aug 3, 2020 at 9:07 | comment | added | Emil Jeřábek | ... equivalent to $I\Sigma_n$, see e.g. Hájek&Pudlák), prove that all sequents in the proof are valid under this truth definition. In the end, you obtain that the empty sequent (that is, $\Longrightarrow\phi$ with $\phi$ discarded as false) is valid, which is a contradiction. | |
| Aug 3, 2020 at 7:10 | comment | added | Emil Jeřábek | ... formulas in the antecedent, except that you can only apply the truth definition to the part of the sequent without $\phi$, as $\phi$ itself has too large complexity. This is the reason why you have to check the truth of $\phi$ before the inductive argument. If it’s true, we are done as that’s what we want to prove, and if it’s false, we have to obtain a contradiction. So, assume it is false, and consider a $\Pi_n$ truth definition for sequents in the proof that fixes the value of $\phi$ as false, and evaluates other formulas in the normal way. Then, using $\Pi_n$ induction (which is ... | |
| Aug 3, 2020 at 7:06 | comment | added | Emil Jeřábek | First, a truth definition for $\Sigma_n$ formulas is $\Sigma_n$, and a truth definition for $\Pi_n$ formulas is $\Pi_n$. You can’t mix the two. Cut-free sequent calculus has the subformula property, respecting the polarity of subformulas, hence in a proof of a $\Sigma_{n+1}$ sentence $\phi$ (with a single leading $\exists$ quantifier), every sequent in the proof has $\phi$ and $\Pi_n$ formulas in the succedent, and $\Sigma_n$ (really, $\Pi_{n-1}$) formulas in the antecedent. A truth definition for such sequents can be written as $\Pi_n$ as the semantics of sequents effectively negates ... | |
| Aug 2, 2020 at 17:55 | comment | added | Emil Jeřábek | We are proving inside $I\Sigma_n$ that if a sentence $\phi\in\Sigma_{n+1}$ is provable in $Q$, then $\phi$ is true. $\psi$ is $\neg\phi$, written in a prenex normal form so that $\psi\in\Pi_{n+1}$. A refutation of $\psi$ is a proof of the sequent $\psi\Longrightarrow{}$. Though now that I think about it, it’s not necessary to make the proof into a refutation. We can just take directly a cut-free proof of $\Longrightarrow\phi$, and assuming $\phi$ is false, show by induction that all sequents in the proof with $\phi$ deleted are true. | |
| Aug 2, 2020 at 17:26 | comment | added | Jori | I know about cut elimination, but I don't understand what you mean by "a cut-free sequent refutation of its negation $\psi$". | |
| Aug 2, 2020 at 16:56 | comment | added | Emil Jeřábek | ... as apart from $\psi$, all the sequents have $\Sigma_n$ antecedents and $\Pi_n$ succedents. (3) The truth definition for $\Sigma_n$ formulas is $\Sigma_n$. | |
| Aug 2, 2020 at 16:55 | comment | added | Emil Jeřábek | (1) What I presented above are called uniform (or global) reflection principles, as opposed to local reflection principles, which are the schemata $\mathrm{Pr}_Q(\ulcorner\phi\urcorner)\to\phi$ for sentences $\phi$. (2) It’s not that easy, as it relies on cut elimination. But basically, you convert a proof of a $\Sigma_{n+1}$ sentence into a cut-free sequent refutation of its negation $\psi$, which is $\Pi_{n+1}$; assuming for contradiction that $\psi$ is true, you prove by induction that all the sequents in the proof with $\psi$ removed are true. This is $\Pi_n$-induction, ... | |
| Aug 2, 2020 at 15:12 | comment | added | Jori | I've accepted your answer; but I remind that the question of a natural example is still open. Or are there such that imply $I\Sigma_2$ easily? | |
| Aug 2, 2020 at 15:10 | vote | accept | Jori | ||
| Aug 2, 2020 at 15:08 | comment | added | Jori | Yes! Thanks! And this only uses the consistency of PRA + $\epsilon_0$-induction, but you need that anyway, otherwise the result is of course false. A few short questions: 1) what do you mean with "uniform"? 2) is it hard to show that $I\Sigma_n$ proves the uniform $I\Sigma_{n+1}$-reflection schema for $Q$? 3) What is the complexity of the truth predicate of up to $n$ quantifiers ($\text{Tr}_n$); I think $\Delta_n$? | |
| Aug 2, 2020 at 11:38 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |