- Using Hilbert's axioms
- Also tried Principia, Rosser, Lukasiewicz

- Axioms
for propositional connectives (as functors)
- HELP! Do I really need
`! [X] : not(not(X)) = X` - HELP! Having them all. Does it hurt?

- HELP! Do I really need
- Rules
for modus ponens and modus tollens
- HELP! This seems to be an axiom to me.
- HELP! Modus tollens dependent on idempotence of
`not`, but not vice versa. Which to use?

- Definitions for operators
- HELP! Having them all. Does it hurt?

- Propositional logic as above
- Rules and
axioms
for the chosen axiomatization, e.g.,
`S5=KM4B.sys` - Add
`necessarily`versions of axioms for PC based S1 (`S1=PCS1M.sys`)- HELP! ... what about PC tautologies