1
$\begingroup$

Let $ T $ denote the theory obtained by removing the axiom $ \forall x ( x = 0 \lor \exists y \, S y = x ) $ and restricting double negation elimination to disjunction-free formulas of Robinson arithmetic. In other words, $ T $ is axiomatized over intuitionistic logic by arithmetical axioms of Robinson arithmetic other than $ \forall x ( x = 0 \lor \exists y \, S y = x ) $, and double negation elimination for disjunction-free formulas.

I've been playing around with $ T $ for quite a while (actually months, on and off), and it seems that no genuine theorems containing a positive disjunction can be proven in $ T $. By genuine I mean those theorems that are not proven by mere logic, like those of the form $ A \rightarrow A \lor B $, or $ A \lor B \rightarrow C \lor D $ where $ A $ implies $ C $ and $ B $ implies $ D $. For example, I couldn't find any way of proving $ \forall x ( x < 2 \rightarrow x = 0 \lor x = 1 ) $. As neither induction nor classical logic is at hand, non of the usual ways of thinking seems to work, at least as far as I could check. I'm really not sure about unprovability of this sentence, as I couldn't find any useful method to show that it's not provable.

So to avoid any possible complexity that could come from considering more general theorems containing positive disjunctions, I ask my question like this:

Is there a method for showing that $ \forall x ( \exists y \, x + S y = 2 \rightarrow x = 0 \lor x = 1 ) $ is provable/unprovable in $ T $?

EDIT:

After @MattF.'s comment, I'm inclined to add that I've been investigating theories other that $ T $, too. For example by adding to $ T $ the axiom $ \forall x ( x \ne 0 \rightarrow \exists y \, S y = x ) $, or other disjunction-free axioms. It's obvious that in the presence of classical logic, these extra axioms trivially imply the above sentence. I first thought that it would be better not to mention these other theories, to keep the question simpler. But if answering the question is easier for these theories than for $ T $, it is desired as well.

EDIT:

To make my thoughts even clearer, I've become suspicious that in the absence of classical logic and extra axioms containing positive disjunctions, the source of all genuine arithmetical theorems containing positive disjunctions is the axiom $ \forall x ( x = 0 \lor \exists y \, S y = x ) $. So I could ask my question like this:

Is there a set $ \Gamma $ of disjunction-free axioms such that $ T + \Gamma \vdash \forall x ( x < 2 \rightarrow x = 0 \lor x = 1 ) $?

Improve this question
$\endgroup$
10
  • $\begingroup$ Does "double negation elimination for disjunction-free formulas" include the implication "\neg \neg (\exists y \ Sy=x) \to (\exists y\ Sy = x)$? $\endgroup$
    – user44143
    Commented Aug 2, 2020 at 4:50
  • $\begingroup$ How do you prove this statement from this axiomatization using classical logic? $\endgroup$
    – user44143
    Commented Aug 2, 2020 at 4:52
  • 2
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Aug 2, 2020 at 8:44
  • 1
    $\begingroup$ (More generally, the disjunction property holds for “$\lor$-Harrop” theories: axiomatized by formulas in which disjunction can only occur inside antecedents of implications.) $\endgroup$
    – Emil Jeřábek
    Commented Aug 2, 2020 at 10:00
  • 2
    $\begingroup$ 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$.) $\endgroup$
    – Emil Jeřábek
    Commented Aug 2, 2020 at 14:06

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .