Weird analogy between quadratic forms and formal systems

Question

A fundamental connection between provability and consistency for formal systems is that, if $Q$ is a formal system and $A$ is a sentence in the language of $S$, then

$Q$ proves $A$ if and only if $Q + \neg A$ is inconsistent

(see for example Franzén's excellent Gödel's theorem: An Incomplete Guide to its Use and Abuse, p.19.)

In quadratic form theory (more precisely: for nondegenerate quadratic forms over a field of characteristic $\neq 2$), an equally fundamental connection between representability (a quadratic form $q$ is said to represent a scalar $a \in K$ if there is a nonzero vector $v$ in the vector space on which $q$ is defined s.t. $q(v) = a$) and isotropy (a quadratic form is isotropic if it represents $0$) is that

$q$ represents $a$ if and only if $q \oplus \left<-a\right>$ is isotropic

(see for example Lam's equally excellent Introduction to Quadratic Forms over Fields, p. 11).

My question is simply: what's up with that?

To be more specific: is there a general relevant framework which allows us to link formal systems and the sentences they prove on the one side, and quadratic forms and the scalars they represent on the other?

The two theories having quite distinct flavours, I would find such a framework really fascinating.

(I've asked the exact same question on MSE, without success.)

Answer 1

I like this question, and I think there is a general relevant framework which links the two cases, but it is so general that you may be disappointed.

Let me start by reformulating the two settings a little. First, if you factor out tautological equivalence, then the set of sentences of a theory forms a Boolean algebra. Given a set of sentences, the sentences provable from them can be regarded as those which are "generated" via formal derivations.

Second, every quadratic form can be diagonalized, i.e., put in the form $\sum a_ix_i^2$, and so can be represented by the multiset $\{a_1, \ldots, a_n\}$. The scalars represented by the form can be viewed as those which are "generated" from this multiset via taking linear combinations with coefficients which are squares.

So, very generally, in both cases we have a set with some algebraic structure (field or Boolean algebra) which includes a negation operation, and we have a notion of elements generated by a subset (or multisubset).

Now in both cases one implication is rather easy. If $Q$ proves $A$, then $Q + \neg A$ is inconsistent --- that is just because $Q + \neg A$ proves $A \wedge \neg A$ and $A \wedge \neg A$ implies $\perp$ (falsehood). If $q$ represents $a$ then $q \oplus \langle -a\rangle$ is isotropic --- this is just because $q \oplus \langle -a\rangle$ represents $a + (-a) = 0$. (Note that in the multiset representation $q \oplus \langle -a\rangle$ becomes $q \cup \{-a\}$.)

The reverse implications are more interesting. If $Q + \neg A$ is inconsistent, i.e., it proves $\perp$, then $Q$ proves $A$ --- this is a special case of the fact that $Q + B \vdash C$ implies $Q \vdash B \to C$. Because $Q + \neg A \vdash \perp$ implies $Q \vdash \neg A \to \perp$ and $\neg A \to \perp$ equals $\neg\neg A$, which under tautological equivalence is the same as $A$. The analogous statement for quadratic forms is that if $q \oplus \langle b\rangle$ represents $c$ then $q$ represents either $c$ or $cx^2 - b$ for some scalar $x$. So that if $q \oplus \langle -a\rangle$ represents $0$ then either $q$ represents $0$ and hence $a$ (it is a theorem that if nondegenerate $q$ represents $0$ then it represents everything) or else $q$ represents $0 -(-a) = a$.