I'm trying to prove Axiom correct.
Axiom draws its power from organizing algorithms based on group
theory, adding propositions as the complexity increases. This helps
limit the assumptions needed to provide algorithms.
Recently I've learned a bit about substructural and (super?) structural
logics. So, for example, given the propositions
(W) Weakening
(C) Contraction
(E) Exchange
they can be combined to form (Crary):
W & C & E ==> Persistant logic.
W & ~C & E ==> Affine logic
~W & C & E ==> Strict logic
~W & ~C & E ==> Linear logic
W & C & ~E ==> ?
W & ~C & ~E ==> ?
~W & C & ~E ==> ?
~W & ~C & ~E ==> Ordered logic
In addition, there appears to be a group theory-like organization of
logics above the substructural e.g. predicate, simply-typed lambda,
and lambda calculus (Avigad).
Organizing these logics by the gradual introduction of propositions
and properties would fit exactly into Axiom's structure and make
proof assumptions clear. I want to organize these in Axiom so the
proofs inherit the required logic.
Can you give me any references to a group-theory-like organization