Timeline for Intutionistic Robinson Arithmetic
Current License: CC BY-SA 3.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 15, 2020 at 7:27 | history | edited | CommunityBot |
Commonmark migration
|
|
| Jan 9, 2016 at 15:12 | vote | accept | Erfan Khaniki | ||
| Jan 9, 2016 at 14:51 | answer | added | Emil Jeřábek | timeline score: 7 | |
| Jan 9, 2016 at 12:26 | comment | added | Erfan Khaniki | @EmilJeřábek: I edited my post and explain what I mean by $\Pi_2$ formula $\phi$. Suppose $K\Vdash Q^e$ is a Beth model, then I think by induction on complexity of $\Delta^+_0$ formula $\phi$ it can be proved that :If for every node $k\in K$, $\mathcal{M}_k\models \phi$ ( $\mathcal{M}_k$ means classical structure of node $k$), then $K\Vdash \phi$. Because every node of such Beth model is locally $Q^e$, therefore by completeness the proof will complete, but I don't know this proof is true and works correctly. | |
| Jan 9, 2016 at 12:15 | history | edited | Erfan Khaniki | CC BY-SA 3.0 |
added 624 characters in body
|
| Jan 9, 2016 at 11:11 | comment | added | Emil Jeřábek | Quick and dirty, by appealing to witnessing theorems for fragments of intuitionistic bounded arithmetic (which is likely an overkill, and only gives a conditional result). There should be a simpler direct argument. I don't quite understand the conditions in your claim, but how do you intend to do the step for quantifiers? | |
| Jan 9, 2016 at 10:57 | comment | added | Erfan Khaniki | @EmilJeřábek: I'm not sure about $Q$ in intutionistic logic, but I think we can prove for every $\Delta_0$ formula $\phi$ such that $\phi$ does not have any $\neg$, $Q^e\vdash_i \phi \lor \psi$ where $Q^e\vdash_c \psi \leftrightarrow \neg \phi$ and also $\psi \in \Delta_0$ does not have any $\neg$ in its syntax. How do you prove your claim? | |
| Jan 9, 2016 at 10:49 | history | edited | Erfan Khaniki | CC BY-SA 3.0 |
added 283 characters in body
|
| Jan 9, 2016 at 10:49 | comment | added | Emil Jeřábek | You may try sending an email to Michal or Albert. But you just answered your own question negatively: neither $Q$ nor $Q^e$ should prove decidability of $\Delta_0$ formulas. | |
| Jan 9, 2016 at 10:28 | comment | added | Erfan Khaniki | @EmilJeřábek: Thank you very much. How can I find those work? | |
| Jan 9, 2016 at 10:27 | comment | added | Erfan Khaniki | @FrançoisG.Dorais: Thank you for you answer. As you said "usual" $Q$ hardly proves any $\Pi_2$ formula, but for example for every $\Delta_0$ formula $\phi$,$Q\vdash_c \phi \lor \neg \phi$. | |
| Jan 9, 2016 at 10:08 | comment | added | Emil Jeřábek | Michal Dančák is studying intuitionistic $Q$, some of it jointly with Albert Visser. I don't think anything is published, yet. There are subtleties concerning the choice of axioms. | |
| Jan 9, 2016 at 0:24 | comment | added | François G. Dorais | Since the "usual" $Q$ hardly proves any $\Pi_2$ facts and you're interested in a nontrivial extension of $Q$, it might be better to state all the axioms to avoid confusion. | |
| Jan 8, 2016 at 21:19 | history | edited | Erfan Khaniki | CC BY-SA 3.0 |
added 717 characters in body; edited tags
|
| Jan 8, 2016 at 19:02 | history | edited | Erfan Khaniki |
edited tags
|
|
| Jan 8, 2016 at 17:32 | history | edited | Erfan Khaniki | CC BY-SA 3.0 |
added 42 characters in body
|
| Jan 8, 2016 at 15:19 | history | asked | Erfan Khaniki | CC BY-SA 3.0 |