Timeline for Does Robinson arithmetic interpret a Kripke model of the double negation translation of $\mathsf{I}\Delta_0 + \mathrm{Exp}$?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2021 at 10:40 | comment | added | Emil Jeřábek | I mean, the double negation translation of a single formula is linear in size, but one also has to supply proofs of translations of logical axioms. Though now that I think about it, these are just fixed schemata, so the overall proof length blow up should be linear, indeed. On the other hand, it is enough to do the verification in $I\Delta_0+\mathrm{Exp}$ if this makes it easier to see that it works, because still $I\Delta_0+\mathrm{Exp}\nvdash\mathrm{Con}_Q\to\mathrm{Con}_{I\Delta_0+\mathrm{Exp}}$. | |
| Apr 13, 2021 at 10:35 | comment | added | Emil Jeřábek | I’m not sure about linear, but it is definitely polynomial. It is given by a polynomial-time function which is easy to define in $I\Delta_0+\Omega_1$, and then one just proves by induction on the length of the proof that it works. | |
| Apr 13, 2021 at 9:28 | comment | added | James E Hanson | @EmilJeřábek Is that because the double negation translation only has something like a linear increase in proof length? | |
| Apr 13, 2021 at 9:22 | comment | added | Emil Jeřábek | Without checking the details of your definition, it is certainly true that $I\Delta_0+\Omega_1$ proves that the consistency of $(I\Delta_0+\mathrm{Exp})^{\neg\neg}$ (over intuitionistic logic) implies the consistency of $I\Delta_0+\mathrm{Exp}$, and that consistency is preserved under interpretations (at least between finitely axiomatized theories), while it does not prove $\mathrm{Con}_Q\to\mathrm{Con}_{I\Delta_0+\mathrm{Exp}}$. | |
| Apr 13, 2021 at 9:11 | comment | added | James E Hanson | @MattF. I have added an explicit description, but the short version of it is that there is a natural way of thinking of a Kripke frame as a two-sorted classical structure, and I'm referring to interpreting that structure in the given classical structure in the standard sense of interpretation in model theory. | |
| Apr 13, 2021 at 9:10 | history | edited | James E Hanson | CC BY-SA 4.0 |
Added explicit description of interpreting a Kripke frame
|
| Apr 13, 2021 at 7:30 | comment | added | user44143 | Yes, I was asking about what it means to interpret a Kripke model | |
| Apr 13, 2021 at 7:19 | comment | added | James E Hanson | @MattF. Or are you asking about what it means to interpret a Kripke model, rather than what a Kripke model is? | |
| Apr 13, 2021 at 6:44 | comment | added | James E Hanson | @MattF. The Wikipedia article on it has a nice writeup of the definition. | |
| Apr 13, 2021 at 2:08 | comment | added | user44143 | Do you have a reference for (or precise statement of) what it means to interpret a Kripke model of a theory? | |
| Apr 4, 2021 at 18:00 | history | asked | James E Hanson | CC BY-SA 4.0 |