# Weird analogy between quadratic forms and formal systems

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.