## lo.logic – Disjunction in weakened Robinson arithmetic

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$$?