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 of the various logics, similar to the above? I have done a literature search but have not found anything yet. Thank you. Tim Daly
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer