Consider the usual first-order language $ \mathcal L = \{ 0 , S , + , \cdot \} $ of arithmetic, and let $ y < x $ be an abbreviation for $ \exists z \ y + S z = x $. An almost negatively axiomatized arithmetical theory (ANAAT for short) $ T $ is a theory in the language $ \mathcal L $ axiomatized over first-order intuitionistic logic with equality by the axiom-schema of strong induction $$ \forall x \Big( \forall y \big( y < x \rightarrow A ( y ) \big) \rightarrow A ( x ) \Big) \rightarrow \forall x \ A ( x ) $$ and a collection of disjunction-free sentences, containing the following axioms of Robinson arithmetic $$ \forall x \forall y ( S x = S y \rightarrow x= y ) \text ; $$ $$ \forall x \ S x \ne 0 \text ; $$ $$ \forall x ( x \ne 0 \rightarrow \exists y \ x = S y ) \text ; $$ $$ \forall x \ x + 0 = x \text ; $$ $$ \forall x \forall y \ x + S y = S ( x + y ) \text ; $$ $$ \forall x \ x \cdot 0 = 0 \text ; $$ $$ \forall x \forall y \ x \cdot S y = x \cdot y + x \text . $$
Question: Is there an ANAAT equivalent to Heyting arithmetic?
An important point is the choice of strong induction over the usual mathematical induction axiom-schema $$ A ( 0 ) \land \forall x \big( A ( x ) \rightarrow A ( S x ) \big) \rightarrow \forall x \ A ( x ) \text . $$ A direct consequence of the usual induction is $$ \forall x ( x = 0 \lor \exists y \ x = S y ) $$ which is a disjunctive version of the third axiom in the list above. If we took this version as an axiom, the two schemata of induction would reduce to one another over intuitionistic logic, and the question would be pointless. The question is thus equivalent to checking whether this sentence is derivable from the above axioms (together with some other disjunction-free theorems of Heyting arithmetic). I neither could find a derivation for it, nor a proof that this is not possible.
This is in fact a follow-up of a previous question of mine concerning theories with only disjunction-free axioms. It was answered by Emil Jeřábek in a comment, noting that disjunction-free theories over intuitionistic logic have the dicjunction property, as a consequence of cut-elimination in the corresponding sequent calculus.
The difference here is the presence of the strong induction axiom schema, which can have positive disjunctions on the right-hand side of implication. Also, cut-elimination can't be done anymore.
An observation can be made about disjunction property of an ANAAT $ T $, via the following version of Kleene's slash for sentences of $ \mathcal L $: $$ \begin {array}{} T | A & & \text {iff} & & T \vdash A \text {, for atomic } A \text ; \\ T | A \land B & & \text {iff} & & T | A \text { and } T | B \text ; \\ T | A \rightarrow B & & \text {iff} & & T | A \text { and } T \vdash A \text { imply } T | B \text ; \\ T | A \lor B & & \text {iff} & & \text {either } T | A \text { and } T \vdash A \text {, or } T | B \text { and } T \vdash B \text ; \\ T | \forall x \ A ( x ) & & \text {iff} & & T | A ( n ) \text { for every numeral } n \text ; \\ T | \exists x \ A ( x ) & & \text {iff} & & T | A ( n ) \text { and } T \vdash A ( n ) \text { for some numeral } n \text . \end {array} $$ This definition can be extended to all formulas of $ \mathcal L $ via taking universal closures. It's then rather straightforward to verify that if we have $ T | A $ for any axiom $ A $ of an ANAAT $ T $ other than the ones explicitly appearing in the definition, then we have $ T | A $ for any theorem $ A $ of $ T $. Therefore, an important class of ANAATs, which includes the minimal one, consists of theories with disjunction property. A similar thing can be said about numerical existence property.
