I am writing a proof assistant, in which a user can define a propositional calculus, and start creating theorems, which are automatically verified.
The problem I have ran into, comes from that I want the user to be able to define arbitrary additional (meta) notation on top of the propositional calculus, for convenience.
For example, suppose the user creates a Hilbert system, which only uses the operators $\{\neg,\to\}$, and would like to define dysjunction as $A\vee B:=\neg A\to B$. This, by itself, is no problem, because I can simply compile formulas which contain these meta-symbols down into formulas which only contain $\neg$ and $\to$.
But how to I enforce, or formalize, that definitions must not inflict with the underling logic? For example, a user could define $A:=\neg A$, and by the principle of explosion, prove any theorem they'd like (even false theorems)?
An initial but naïve idea would be to assert that the LHS of the definitions must contain only new operators. But this too can be abused. For example, here's another "proof" which leads to the principle of explosion. Define $B\circ B:=A\to B$
$$ \begin{align} \text{1. }&B\to B\text{ (instance of identity)}\\ \text{2. }&(B\to B) \to B\circ B\text{ (by definition of $\circ$)}\\ \text{3. }&B\circ B\text{ (by (1) and (2) from modus ponens)}\\ \text{4. }&B\circ B \to (A\to B)\text{ (by definition of $\circ$))}\\ \text{5. }&A\to B \text{ (by (3) and (4) from modus ponens))} \end{align} $$
thus we have "proven" that $A\to B$ is always true (which it is obviously not, especially in our Hilbert system).
Any and all advice would be greatly appreciated.