@IgorKhavkine my comment applies specially to you, since what you said looks precisely what I'm looking for.

Hey guys, thanks for the comments! If possible, I'd like some suggestions on these topics you mentioned. I've never studied Lie grous and its representations, I have no idea where to begin.

Does it sound okay?

user347489 in summary, I can use the definition on my post (with arbitrary $V$ and using the universal property) and prove its existence by using the quotient of the tensor algebra with the ideal generatedby $u\otimes u - B(u,v)$ as Greub does. This proves existence. If $V$ is finite-dimensional and $\mathbb{K}$ has characteristic different from 2, taking a symmetric bilinear form with signature $(p,q)$ leads to $\mathcal{Cl}(V,\Phi)$, which is essentially what Greub constructed but with some additional hypothesis. Finally, take $B$ to be the Minkowski inner product to get $\mathcal{Cl}_{1,3}$

user347489, what is your definition of an "orthogonal bilinear form"? Does it mean that $V$ has a basis $\{v_{\alpha}\}_{\alpha \in I}$ where $B(v_{\alpha},v_{\beta}) = 0$ whenever $\alpha \neq \beta$? (I guess you are not thinking of finite-dimensional vector spaces necessarily, right?)

@IgorKhavkine I think I'm getting the idea. I'm going to work out the details!

An additional comment: I just checked the construction on Greub's book and he uses the ideal $u\otimes u -B(u,u)$ apparently. Is this equivalent to your approach?

Also, If you have other references to suggest, where this construction using quotient space is done, I'd appreciate.

Your partial answer is already very useful! So, in short: I can keep my definition using quadratic forms as it is and show that the construction via quotient spaces provide a particular example where the definition holds (i.e. it proves the existence). I guess this is what Greub does. After, I have to choose $B$,$V$ and so on to construct the Dirac algebra. Is that correct? I still need to understand the details about the second part, on how to construct the Dirac algebra from the general quotient construction tho.

@Peter I'm definitely not much trained on this subject so I don't know if I understood you correctly, but here are some comments. This is the most general definition of a Clifford algebra I know and I've seen some proofs of its existence in books. Thus, I'm considering it exists. In any case, if I succeed on showing that the Dirac algebra satisfies the properties of the definition, I'd be indirectly proving its existence again by constructing an explicit example of it. Did I answer your question?

@PedroLauridsenRibeiro I editted the post and corrected what you pointed out: $E$ is defined for $f \in \mathscr{S}(\mathbb{R}^{4})$ instead of $\mathscr{H}$.

$a(E\mbox{Re}(f)-iE\mbox{Im}(f)) = a(C\{E\mbox{Re}(f)+iE \mbox{Im}(f)\}) = a (CEf)$, as proposed by Reed & Simon. But I had to use the fact that $Ef \in \mathscr{H}_{C}$. If not, it is not clear to me how to justify this factor.