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; there are multiple possible proofs for some statements. This is not a serious issue.
Category
Identity arrows exist. Composition is allowed, well-typed, and internalized.
| Name | Statement |
|---|---|
| id | ganai broda gi broda |
| syl | ganai broda gi brode & ganai brode gi brodi ⇒ ganai broda gi brodi |
| ganai-comp-lr | ganai ganai broda gi brode gi ganai ganai brode gi brodi gi ganai broda gi brodi |
| ganai-comp-rl | ganai ganai broda gi brode gi ganai ganai brodi gi broda gi ganai brodi gi brode |
Initial Object
Trivial falsehood is the initial object.
| Name | Statement |
|---|---|
| gaiho-init | ganai gai'o gi broda |
Terminal Object
Trivial truth is the terminal object.
| Name | Statement |
|---|---|
| ceihi-term | ganai broda gi cei'i |
Products
Conjunction is the categorical product. Conjunction is a lower bound on the left and right, and indeed the least lower bound; in other words, all binary conjunctions exist. Conjunction is idempotent and commutes. In addition to the standard product, pointwise conjunctions of arrows are possible. Conjunction distributes over disjunction, making Loj into a distributive category.
| Name | Statement |
|---|---|
| ax-ge-le | ganai ge broda gi brode gi broda |
| ax-ge-re | ganai ge broda gi brode gi brode |
| ge-prod | ganai broda gi brode & ganai broda gi brodi ⇒ ganai broda gi ge brode gi brodi |
| ge-idem | go ge broda gi broda gi broda |
| ge-com | go ge broda gi brode gi ge brode gi broda |
| ge-pair | ganai broda gi brode & ganai brodi gi brodo ⇒ ganai ge broda gi brodi gi ge brode gi brodo |
| ge-dist-ga | go ge broda gi ga brode gi brodi gi ga ge broda gi brode gi ge broda gi brodi |
Coproducts
Disjunction is the coproduct. Disjunction is an upper bound on the left and right, and indeed the greatest upper bound; in other words, all binary disjunctions exist. Disjunction is idempotent and commutes. In addition to the standard coproduct, pointwise disjunctions of arrows are possible. Disjunction distributes over conjunction, making Loj into a distributive lattice and therefore a distributive category.
| Name | Statement |
|---|---|
| ga-lin | ganai broda gi ga broda gi brode |
| ga-rin | ganai broda gi ga brode gi broda |
| ga-sum | ganai broda gi brode & ganai brodi gi brode ⇒ ganai ga broda gi brodi gi brode |
| ga-idem | go ga broda gi broda gi broda |
| ga-com | go ga broda gi brode gi ga brode gi broda |
| ga-pair | ganai broda gi brode & ganai brodi gi brodo ⇒ ganai ga broda gi brodi gi ga brode gi brodo |
| ga-dist-ge | go ga broda gi ge brode gi brodi gi ge ga broda gi brode gi ga broda gi brodi |
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
The core is a category.
| Name | Statement |
|---|---|
| go-id | go broda gi broda |
| go-syl | go broda gi brode & go brode gi brodi ⇒ go broda gi brodi |
The core is a subcategory. The core is its own opposite category.
| Name | Statement |
|---|---|
| go-ganai | go broda gi brode ⇒ ganai broda gi brode |
| go-comi | go broda gi brode ⇒ go brode gi broda |
Because Loj is thin, there is an embedding from any pair of inverse arrows to the corresponding core arrow.
| Name | Statement |
|---|---|
| iso | ganai broda gi brode & ganai brode gi broda ⇒ go broda gi brode |
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.
The functor is covariant.
| Name | Statement |
|---|---|
| nakunaku | ganai broda gi naku naku broda |