rework: definitions need to introduce axioms!

Axioms are the things that constrain interpretations when we consider
entailment. So, the theorems that come out of the definitional
principles need to be treated as axioms, since otherwise there's no
reason an interpretation can interpret the new constant as something
unintended.

With this change, the soundness proof comes through easily.

But, consistency is going to be difficult! Because for consistency we
need to know that the axioms are consistent. This will require some
extra proofs...