Loj
Loj is a category formed from Lojban syntax. Specifically, it is the poset (WP, nLab) whose:
- objects are equivalence classes of closed well-formed bridi, and
- arrows are implications from one bridi to another.
To read Metamath theorems as statements about Loj, encode:
- objects as members of the {broda} series
- arrows from X to Y as {ganai X gi Y}
- pasting diagrams as applications of ax-mp
- Isomorphisms from X to Y as {go X gi Y}
Note that while Loj is thin, its formal verification in Metamath is non-thin. This is not a serious issue.
Table of proofs
| Metamath statement | Lojban bridi | What it means |
|---|---|---|
| id | {ganai broda gi broda} | identity arrows exist |
| syl | {ganai broda gi brode} & {ganai brode gi brodi} => {ganai broda gi brodi} | composition is allowed and well-typed |
| k-ceihi | {ganai broda gi cei'i} | trivial truth is the terminal object |
| iso | {ganai broda gi brode} & {ganai brode gi broda} => {go broda gi brode} | isomorphisms are allowed |
| ax-ge-le | {ganai ge broda gi brode gi broda} | conjunction is a left lower bound |
| ax-ge-re | {ganai ge broda gi brode gi brode} | conjunction is a right lower bound |
| ga-lin | {ganai broda gi ga broda gi brode} | disjunction is a left upper bound |
| ga-rin | {ganai broda gi ga broda gi broda} | disjunction is a right upper bound |
| garii | {ganai broda gi brode} & {ganai brodi gi brode} => {ganai ga broda gi brodi gi brode} | disjunction is the least upper bound |
| ge-idem | {go ge broda gi broda gi broda} | conjunction is idempotent |
| ga-idem | {go ga broda gi broda gi broda} | disjunction is idempotent |
| ge-com | {go ge broda gi brode gi ge brode gi broda} | conjunction commutes |
| ga-com | {go ga broda gi brode gi ga brode gi broda} | disjunction commutes |
To Do
- Implication, conjunction, disjunction should form a lattice
- Missing ge-ind: deductive form of ax-ge-in
- And also a distributive lattice?
- {ge broda gi ga brode gi brodi} => {ga ge broda gi brode gi brodi}
- Easy implications of being a lattice:
- Associativity: {ge/ga broda gi ge/ga brode gi brodi} => {ge/ga ge/ga broda gi brode gi brodi}
- Absorption: {ge/ga broda gi ga/ge broda gi brode} => {broda}
Core
The core of a category is the groupoid which includes all of its isomorphisms. The core of Loj, written Core(Loj), is the groupoid whose:
- objects are equivalence classes of bridi, and
- arrows are bi-implications from one bridi to another.
To read Metamath theorems as statements about Core(Loj), encode:
- objects as members of the {broda} series
- arrows from X to Y as {go X gi Y}
- pasting diagrams as applications of bi
Table of proofs
| Metamath statement | Lojban bridi | What it means |
|---|---|---|
| go-id | {go broda gi broda} | identity arrows exist |
| go-syl | {go broda gi brode} & {go brode gi brodi} => {go broda gi brodi} | composition is allowed and well-typed |
| go-ganai | {go broda gi brode} => {ganai broda gi brode} | the core is a subcategory |
| go-comi | {go broda gi brode} => {go brode gi broda} | the core is its own opposite category |
Double Negation
Negating a bridi twice, known as double negation (WP, nLab), is a functorial action which maps classical logic to intuitionistic logic. It can also be constructed as an endofunctor on intuitionistic logic, which yields a continuation monad. The functor's image yields a category whose:
- objects are (equivalence classes of) refutations of supposed counterexamples to bridi, and
- arrows are implications from one refutation-equipped bridi to another.
Table of proofs
| Metamath statement | Lojban bridi | What it means |
|---|---|---|
| nakunaku | {ganai broda gi naku naku broda} | the functor exists and is covariant |