Timeline for Disjunction in weakened Robinson arithmetic
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 2, 2020 at 17:44 | comment | added | user44143 | If you have nothing like this axiom then many semi rings will be models (eg the non-negative reals or rationals), so you can’t hope to prove much. | |
| Aug 2, 2020 at 15:29 | comment | added | Emil Jeřábek | On second thought, I’m not sure the Kleene slash argument will work. But in any case, the proof using cut-free sequent calculus is quite simple. | |
| Aug 2, 2020 at 14:10 | comment | added | Mohsen Shahriari | @EmilJeřábek I got it. Thanks. | |
| Aug 2, 2020 at 14:06 | comment | added | Emil Jeřábek | The axioms $\neg\neg A\to A$ are $\lor$-free, hence the result applies to them. And the general statement can be proved in the same way as the more commonly stated fact that theories axiomatized by Harrop formulas have the DP: by induction on the size of a cut-free proof in the intuitionistic sequent calculs allowing at most one formula in the succedent. (Some variant of Kleene’s slash likely works, too, if you make $\exists$ “non-constructive”. That is, redefine $|\exists x\,\phi$ as $\exists x\,|\phi$.) | |
| Aug 2, 2020 at 13:53 | comment | added | Mohsen Shahriari | @EmilJeřábek Well, the logic of $T+\Gamma$ is not exactly intuitionistic logic, as it has axioms of the form $\neg\neg A\to A$ for disjunction-free $A$. These axioms are not readily realizable, and similar considerations seem to suggest that other usual techniques of proving disjunction property (Kleene-Aczels'slash, adding nodes as roots of Kripke models, an such) won't work either. Will you please illustrate how to prove disjunction property in this case? | |
| Aug 2, 2020 at 10:00 | comment | added | Emil Jeřábek | (More generally, the disjunction property holds for “$\lor$-Harrop” theories: axiomatized by formulas in which disjunction can only occur inside antecedents of implications.) | |
| Aug 2, 2020 at 8:44 | comment | added | Emil Jeřábek | It is a general fact about intuitionistic logic that disjunction-free theories have the disjunction property. Thus, assuming $T+\Gamma\vdash\forall x\,(x<2\to x=0\lor x=1)$, let $c$ be a fresh constant; the disjunction-free theory $T+\Gamma+c<2$ proves $c=0\lor c=1$, hence by the DP, it proves $c=0$ or $c=1$. Thus, $T+\Gamma$ proves $\forall x\,(x<2\to x=0)$ or $\forall x\,(x<2\to x=1)$. Hopefully, $T$ still proves $0<2$, $1<2$, and $0\ne1$, which means $T+\Gamma$ is inconsistent. | |
| Aug 2, 2020 at 6:10 | history | edited | Mohsen Shahriari | CC BY-SA 4.0 |
added explanation
|
| Aug 2, 2020 at 5:54 | history | edited | Mohsen Shahriari | CC BY-SA 4.0 |
added explanation
|
| Aug 2, 2020 at 5:42 | comment | added | Mohsen Shahriari | @MattF. Yes, it includes that implication. $\quad$ I don't know if I can prove it from these axioms using classical logic. The mention of classical logic in the "at hand" part of the post was due to the fact that I've been investigating theories other than $T$, too. For example, by adding to $T$ the axiom $x\ne0\to\exists y\,Sy=x$ and other disjunction-free axioms. In the presence of classical logic, those trivially lead to proving the statement. I thought it would be better to keep things simpler by not mentioning those theories. But an answer addressing those theories is desired as well. | |
| Aug 2, 2020 at 4:52 | comment | added | user44143 | How do you prove this statement from this axiomatization using classical logic? | |
| Aug 2, 2020 at 4:50 | comment | added | user44143 | Does "double negation elimination for disjunction-free formulas" include the implication "\neg \neg (\exists y \ Sy=x) \to (\exists y\ Sy = x)$? | |
| Aug 2, 2020 at 4:46 | history | edited | Mohsen Shahriari | CC BY-SA 4.0 |
added explanation
|
| Aug 2, 2020 at 4:23 | history | asked | Mohsen Shahriari | CC BY-SA 4.0 |