It is known that the Q axioms are not a conservative extension of the Q1--Q5 axioms. However, I could not find any example of a theorem of the language $\{+,0,\textrm{S}\}$ (i.e., the language of Q1--Q5) that was not provable in the theory of Q1--Q5 but was provable in Q.
In other words, I'm asking for an example of an arithmetic theorem in which addition occurs but not multiplication, which is only provable using some arithmetic theorem in which multiplication occurs (axiom Q6 or Q7).
- Q1 -- $\forall x(\textrm{S}(x)\neq 0)$
- Q2 -- $\forall x\forall y(\textrm{S}(x)=\textrm{S}(y)\rightarrow x=y)$
- Q3 -- $\forall x(x\neq 0 \rightarrow \exists y(x=\textrm{S}(y)))$
- Q4 -- $\forall x(x+0=x)$
- Q5 -- $\forall x\forall y(x+\textrm{S}(y)=\textrm{S}(x+y))$
- Q6 -- $\forall x(x.0=0)$
- Q7 -- $\forall x\forall y(x.\textrm{S}(y)=x.y+x)$
I can't solve the original problem yet.
The best I can do is come up with a statement that's a theorem of the reduced theory of Robinson arithmetic plus a fictitious Q8 (shown below) but not of Q1-Q5.
Q8)
$[\forall x y](x * S(y) = x + x*y)$
Q8 would allow proving associativity of addition with additions of a fixed number repeated standardly-many times.
With multiplication, you can prove that:
$$ [\forall x]((x + x) + x = x + (x + x)) $$
since $(x + x) + x = 3x = x + (x + x) $.
Next, I'm going to construct a nonstandard model of $Q$.
Consider the absolutely free algebra on the language $(0, +, s, p, c)$. Intuitively, $c$ is a nonstandard natural number that's larger than all standard naturals, $s$ is the successor, and $p$ is the predecessor. Note that we introduce negative numbers, which we will then remove.
We will take that algebra, remove the negative elements, and impose only the equivalences that we have to, and be left with a structure that satisfies the Robinson axioms but doesn't have $(c+c)+c = c+(c+c)$.
Here's how to do it. Let's call the full structure $\mathcal{A}$. Let each element be of the form $k + q$ where $k$ is a standard integer and $q$ is an element of the free magma generated by $(c, +)$ or, exceptionally, $0$ if the number has no nonstandard part.
I will now define addition in this structure:
$$ (k + q) + (k' + q') = (k + k') + (q + q') $$
Note that $(k + k')$ is another standard integer, and that the $+$ in $(q + q')$ is neither commutative nor associative.
Define a number of the form $(k + q)$ to be negative if and only if $q$ is $0$, and $k$ is strictly less than $0$.
Define $s(k + q) = (1 + k) + q$.
Define $p(k + q) = (-1 + k) + q$.
$c$ already has the form $0 + c$.
I will now define $\mathcal{A}^+$, the non-negative components of $\mathcal{A}$.
Let the domain of $\mathcal{A}^+$ consist precisely of the elements of $\mathcal{A}$ that are not negative.
Let the symbols of $\mathcal{A}^+$ be the symbols of $\mathcal{A}$ but without $p$, (since $p$ would be a partial function).
Let every other symbol have the same definition that it does in $\mathcal{A}^+$, except restricted to the domain of $\mathcal{A}^+$.
In effect, standard numerals commute and associate in the familiar way, but nonstandard numerals do not. The standard numerals can always be collected as the left summand in our normal form.
I claim that this is a model of $Q$, which I will now verify.