# formal semantics

Mentioned under hardliners (some parts of which could be incorporated here).

In linguistics, formal semantics is the business of modeling the meaning of utterances in terms of lower-level units; for example, modeling the meaning of sentences in terms of the meanings of their words. "Formal" means that the models should ideally be rigorous and mathematical.

A complete formal semantics for a language would have to model both individual word meanings (or morphemes, or some other low-level unit) and the language's compositional semantics, which is how bigger meanings are built up out of the small ones. In practice, I get the impression that linguists in this area largely concentrate on the compositional semantics. But it's a big biz in linguistics, and I'm sure there are all kinds.

A complete formal semantics is far beyond the state of the art for any natural language. I also happen to believe that it is far beyond the state of the art for Lojban. If it can be done at all with current knowledge, I think it would be necessary to design a new language starting from scratch for the purpose. On the other hand, partial semantic models can still be cool. The book provides some, here and there, and we may be able to discover or retrofit others into Lojban. But I also believe that too much bending and cutting to retrofit a formal semantic model, no matter how cool, would risk breaking the language. *mi'e jezrax*

And now for something completely different!

In formal logic, the **semantics** of some syntax is a homomorphism from that syntax. There can be more than one semantics for a given syntax. As a special case, when syntax and semantics both form categories, then the homomorphism is a functor, leading to categorical semantics. This can all be generalized to a more generic connection between type theories and categories.

Lojban can easily be construed to form a syntactic theory. CLL gives several instances of equivalent bridi which can be used to bootstrap logical implication at the syntactic level. Several common features of such categories are on display, including a lattice of implications under conjunction and disjunction. As type theories go, Lojban doesn't have very strong typing rules, but because Lojban features SOL (second-order logic), untyped expressions are preferable.

The most obvious target category is Set, the category of sets and functions. The selbri can be mapped to relations, which are implemented as spans of functions or (equivalently) as subsets of Cartesian products. The terbri would then be mapped to elements of sets. This interpretation has been developed in la brismu.