Last active
July 26, 2026 23:33
-
-
Save mstewartgallus/5816ba61ffed78fb0d386d7988ba50d6 to your computer and use it in GitHub Desktop.
Draft of antisymmetric logic
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Trying to figure out an odd kind of anti-symmetric calculus. Just very awkward to work with substructural logic. | |
| The trouble is that a double category sort of thing where the source object is the composition of several spans is really awkward to work with. Anti-symmetry is an attempt to approach things from the opposite perspective of apartness instead of equivalence and groupoids. | |
| t ::= π» | 1 | tβ β§ tβ | βt | |
| βββ id | |
| t β’ t | |
| Ξ, tβ, Ξ, tβ, Ξ£, tβ, Ξ β’ tβ | |
| βββββββββββββ 1/2-exchange | |
| Ξ, tβ, Ξ, tβ, Ξ£, tβ, Ξ β’ tβ | |
| βββ 1-intro | |
| β’ 1 | |
| Ξ β’ t | |
| Ξ β’ 1 | |
| ββββββ 1-elim | |
| Ξ, Ξ β’ t | |
| Ξ, tβ, Ξ, tβ, Ξ£ β’ tβ | |
| ββββββββββ β-intro | |
| Ξ, tβ, Ξ, tβ, Ξ£ β’ βtβ | |
| Ξ, tβ, Ξ, tβ, Ξ£ β’ *tβ | |
| ββββββββββ β-elim | |
| Ξ, tβ, Ξ, tβ, Ξ£ β’ tβ | |
| Ξ β’ tβ | |
| Ξ β’ tβ | |
| ββββββββ β§-intro | |
| Ξ, Ξ β’ tβ β§ tβ | |
| tβ, tβ, Ξ β’ tβ | |
| Ξ β’ tβ β§ tβ | |
| ββββββββ β§-elim | |
| Ξ, Ξ β’ tβ | |
| Derived types and terms. | |
| Define | |
| Ο β‘ β1 | |
| tβ β¨ tβ β‘ β(βtβ β§ βtβ) | |
| β | |
| Lemma | |
| Ο odd | |
| Ο β’ Ξ β’ βt | |
| ββββββ β-Ο-elim | |
| Ξ β’ t | |
| Proof | |
| Group theory Β―\_(γ)_/Β― | |
| β | |
| Lemma | |
| Ο odd | |
| Ξ β’ βt | |
| ββββββ β-Ο-inv-elim | |
| Ο β’ Ξ β’ t | |
| Proof | |
| Β―\_(γ)_/Β― | |
| β | |
| Lemma | |
| Ξ β’ Ο | |
| Ξ β’ Ο | |
| βββββ Ο-elim | |
| Ξ, Ξ β’ 1 | |
| Proof | |
| ββββ H2 | |
| - Ξ β’ Ο | |
| ββββββ H1 | |
| Ξ β’ Ο | |
| βββββ β-Ο-inv-elim | |
| - Ο β’ Ξ β’ 1 | |
| βββββββ 1-elim | |
| Ο β’ Ξ, Ξ β’ Ο | |
| βββββββββ {equivalent for some Ο'} | |
| Ο' β’ (Ξ, Ξ) β’ Ο | |
| βββββββ β-Ο-elim | |
| Ξ, Ξ β’ 1 | |
| β | |
| Theorem | |
| Ξ β’ tβ | |
| Ξ, tβ, K β’ tβ | |
| βββββββ cut | |
| Ξ, Ξ, K β’ tβ | |
| FIXME |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment