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