Consider the language $(+, -, 0, \langle – , – \rangle -)$ of abelian groups, with an additional ternary operation $\langle – , – \rangle -$, which is intended to represent the operation of taking vectors $u, v, w$ of an inner product space and returning $\langle u, v \rangle w$.
Let $T$ be the theory consisting of all first-order sentences written in this language which are satisfied by all real inner product spaces (or maybe even "rational inner product spaces"?). My broad question is: what can be said about $T$? Is it interesting, has it been studied? Two concrete questions are:
Is $T$ finitely axiomatizable?
What are interesting structures that model $T$, apart from inner product spaces?
(This question does not have an application in mind, it is plain curiosity.)
Best Answer
For concreteness, let's work over the reals, so $T$ is the theory of all real inner product spaces, in your language. Relative to $T$, there is a definable equivalence relation on pairs, given by $$(x,y)E(x',y') \iff \forall z\,(\langle x,y\rangle z = \langle x',y'\rangle z).$$ We can think of the equivalence classes for $E$ as scalars. I'll write the equivalence class of $(x,y)$ as $[x,y]$. Now we can define addition and multiplication of scalars as follows:
\begin{align*} [x_1,y_1] + [x_2,y_2] = [x_3,y_3] &\iff \forall z\, (\langle x_1,y_1\rangle z + \langle x_2,y_2\rangle z = \langle x_3,y_3\rangle z)\\ [x_1,y_1] \times [x_2,y_2] = [x_3,y_3] &\iff \forall z\, (\langle x_1,y_1\rangle (\langle x_2,y_2\rangle z) = \langle x_3,y_3\rangle z) \end{align*}
Note that $T$ asserts that the truth values of the formulas on the right do not depend on the chosen representatives of the $E$-classes, since this is true in any real inner product space.
Now for any real inner product space $V$, if $V = \{0\}$, then there is only one $E$-class in $V$. On the other hand, if $V$ is nontrivial, then every real number is in the range of the inner product, and distinct real numbers have distinct actions on any nonzero vector. So $V^2/E$ is in bijection with $\mathbb{R}$, and further, $T$ asserts $V^2/E$, with the operations $+$ and $\times$ defined above, satisfies all the first-order sentences true of $(\mathbb{R},+,\times)$. Thus in any nontrivial model $V\models T$, we have that $V^2/E$ is a real closed field. Finally, in any nontrivial model, we have a definable map $V^2 \to V^2/E$ sending $(x,y)$ to $[x,y]$ (as a formula, this is just the identity relation), and we have a definable map $V^2/E\times V \to V$ by $([x,y],z)\mapsto \langle x,y\rangle z$ (this clearly does not depend on the choice of representative $(x,y)$), and $T$ asserts that these maps make $V$ into an inner product space over $V^2/E$.
This shows that every model of your theory $T$ arises as an inner product space over a real closed field (certainly the trivial model does: the trivial group can be viewed as an inner product space over any field). So I guess the answer to your second question is "there are no interesting models" (unless you find inner product spaces over the hyperreals interesting, for example).
To answer your second question, let's reframe the above observations in the language of interpretability. We have shown that $T$ interprets the following theory $T'$: The language $L'$ has two sorts, $S_K$ and $S_V$, with the language of fields on the $S_K$ sort, the language of vector spaces on the $S_V$ sort, a symbol for scalar multiplication $S_K\times S_V\to S_V$, and a symbol for inner product $S_V\times S_V\to S_K$. The theory $T'$ says that if $S_V$ contains only one element, then $S_K$ contains only one element. But if $S_V$ contains more than one element, then $S_K$ is a real closed field, and $S_V$ is an inner product space over this field.
Going the other way, $T'$ interprets $T$ by just forgetting about the $S_K$ sort, and defining the ternary relation $\langle x,y\rangle z$ in the obvious way. And if we start with a model $M\models T$, carry out the interpretation to get a model $M'\models T'$, and then carry out the reverse interpretataion to get a model $M''\models T$, we have $M = M''$.
Further, the mutual interpretation between $T$ and $T'$ is a bi-interpretation. We have already shown that if we interpret $M \models T\rightsquigarrow M'\models T'\rightsquigarrow M''\models T$, then there is a definable isomorphism $M\cong M''$ (the identity). Going the other way, taking $M \models T'\rightsquigarrow M'\models T\rightsquigarrow M''\models T'$, the isomorphism on the vector space sort is the identity, and the isomorphism on the field sort sends a field element $c$ to the equivalence class $[v,w]$ of all pairs of vectors with $\langle v,w\rangle = c$. But this is definable (by the formula $x = \langle y,z\rangle$), so we have a bi-interpretation. Note that the above formula works in the trivial case as well.
It follows that $T$ is not finitely axiomatizable. Suppose for contradiction that $T$ is finitely axiomatizable. Then by adding a single new axiom (getting a new theory $T_1$), we can assert that the vector space is $1$-dimensional. The same bi-interpretation as above restricts to a bi-interpretation between $T_1$ and $T'_1$, the theory of a real closed field and a $1$-dimensional inner product space over the field. But this theory $T'_1$ is bi-interpretable with the theory RCF of real closed fields. Since finite axiomatizability is an invariant of bi-interpretation (between theories in finite languages), we could conclude that RCF is finitely axiomatizable. But RCF is not finitely axiomatizable; this is a contradiction.
Finally, two observations: First, there was nothing particularly special about $\mathbb{R}$ here. You could do the same for inner product spaces over $\mathbb{Q}$ or $\mathbb{C}$. Things get more interesting if you consider arbitrary bilinear forms. For example, if $T$ is the theory (in two sorts, like $T'$ above) of an infinite-dimensional vector space over a field, equipped with a non-degenerate bilinear form, then the model companion of $T$ was studied by Granger, who showed it is not simple, and later by Chernikov and Ramsey, who showed it satisfies the combinatorial property $\text{NSOP}_1$. This theory is certainly not bi-interpretable with the theory of algebraically closed fields (even though the field sort in any model is algebraically closed), since the theory $\text{ACF}$ is stable.