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

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

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