I want to show that the Theory of commutative rings with $1$, satisfies the disjunction property. That is
If $A\lor B$ is a theorem then $A$ is a theorem or $B$ is a theorem.
The language I use is $L:=\{=,+,\cdot,-,0,1\}$ and with this language we form the axioms of $T_{\text{cring}}$:
$\forall x (x=x)$
$\forall x\forall y (x=y\rightarrow y=x)$
$\forall x\forall y\forall z (x=y\land y=z\rightarrow x=z)$
$\forall x\forall y(x=y\rightarrow -x=-y)$
$\forall xyzu(x=y\land z=u\rightarrow x+z=y+u)$
$\forall xyzu(x=y\land z=u\rightarrow xz=yu)$
$\forall xyz((x+y)+z=x+(y+z))$
... and so on.
I am using intuoinistic predicate logic $I$.
So, there is a theorem which say that if $\Gamma$ does not contain disjunction as strictly positive part (s.p.p) then, if $\Gamma\vdash A\lor B$ it follows that $\Gamma\vdash A$ or $\Gamma\vdash B$. Hence, if we can prove our theory (I think?) does not contain disjunction as s.p.p then we are finished. I've also read something about Harrop formulas, which could be another way to prove this(?). I don't which one of these two approaches would be the easier one and I don't know where to start on any the two approaches. I have tried to search around the internet about disjunction property, s.p.p and so on, but I find very little material which I find useful.
Can someone please give me any hints on how to approach this kind of problems? If there are several cases to prove this, perhaps show me one case so I can try to do the rest of them? I am not sure I really know what s.p.p is for that sake either. Sorry, but I seriously don't know where to start... :/
In this case the axioms you have quoted don't contain any disjunction at all, so in particular it doesn't contain any disjunction in a strictly positive position either.
By the way, this special case is easily proven by taking our proof system to be the intuitionistic sequent calculus LJ and using induction over the structure of a cut-free proof of $\Gamma\vdash A\lor B$:
The last rule applied cannot be the identity axiom or $\lor L$ because $\Gamma$ is assumed not to contain $\lor$.
If the last rule is $\bot L$ or $\neg L$, then we can trivially replace the conclusion with either $A$ or $B$, as we please.
If the last rule is any other left rule, then $A\lor B$ is the conclusion of exactly one of the premises, and we proceed by induction.
If the last rule is a right rule, it can only be one of the $\lor R$ rules, in which case the premise is either $\Gamma\vdash A$ or $\Gamma\vdash B$, as desired.
By closer inspection of this proof we see that it is not really required that $\Gamma$ is completely free of $\lor$. An analysis of exactly what we need to assume about $\Gamma$ leads to a recursively defined concept that is almost identical to that of Harrop formulas, except that for our purposes it is okay for $\Gamma$ to contain existential quantifiers at the top level, even though they are not Harrop.
(Hmm... actually it would make sense to describe the contexts this recursively defined concept restricts as "strictly positive positions", so it is possible that I have merely restated the theorem you already know ...)