Remove hardcoding of primitive formulas

[nsbgn]

There is a simplification method right now that strips the operators in formulas to the bare minimum necessary: just implication, φ→ψ.

Rather than being hardcoded, this should be given in the JSON system definition. This way, it will be up to the user to decide which operators should be part of the system and which are merely derived.

A dedicated newtype would help with keeping primitive formulas and derived formulas seperate. This would also include checks to see that a formula is indeed primitive, and making sure that the rule premises and conclusions consist only of primitive formulas.

One idea calls for optional rewrite key in the YAML that gives a translation table for the normalisation process. This provides flexibility and also makes it clear which formulas are not primitive:

rewrite:
    - from: "~A"
      to: "A -> 0"
    - from: "A | B"
      to: "(A -> 0) -> B"
    - from: "A ^ B"
      to: "A -> B -> 0"
    - from: "A & B"
      to: "(A -> B -> 0) -> 0"

[nsbgn]

If this is done, Logic.Judge.Formula.Substitution needs to be changed so that formulas other than Implication can be patterned.