Metavariables

In Lojban

Lojban has metavariables for various semantic objects:

  • sumti: {ko'a}, {fo'a}, etc.
  • selbri: {broda}, etc.

Lojban also has quantified bound variables:

  • first-order: {da}, etc.
  • second-order: {bu'a}, etc.

In Metamath

Metamath cannot substitute a grammar production without designated metavariables. Thus, we have embraced many experimental cmavo in order to make our logic more flexible, and restricted semantic metavariables to serve as specific portions of syntax.

The current mapping is as follows:

  • sumti: {ko'a}, etc.
  • selbri: {bu'a}, etc.
  • brirebla: {bo'a}, etc.
  • bridi: {broda}, etc.
  • numbers: {ku'i'a}, etc.
Metamath typecmavo
brireblabo'a
brireblabo'e
brireblabo'i
brireblabo'o
brireblabo'u
bridibroda
bridibrode
bridibrodi
bridibrodo
bridibrodu
selbribu'a
selbribu'e
selbribu'i
sumtida
sumtide
sumtidi
sumtifo'a
sumtifo'e
sumtifo'i
sumtifo'o
sumtifo'u
sumtiko'a
sumtiko'e
sumtiko'i
sumtiko'o
sumtiko'u
PAku'i'a
PAku'i'e
PAku'i'i