The Logical Language Group Online Dictionary Query

There are specific tools that make searching this database easier:

la sutysisku dictionary, an offline enabled web app

la vlasisku search engine for the Lojban dictionary

Query string:
Search type:
Database:

Database copyright information
Server information

To improve the quality of results, jbovlaste search does not return words with insufficient votes. To qualify to be returned in search results, a proposed lujvo is required to have received a vote in favor in both directions: for instance, in English to Lojban and in Lojban to English.

In addition, due to it being a very technically hard problem, full text searching (that is, searching of definitions rather than just keywords) is not available at this time.


1 definition found
From Lojban to English :

        Word: ctaipe [jbovlaste]
        Type: fu'ivla
  Gloss Word: proof in the sense of "proof theory, general mathematics"
  Gloss Word: typed in the sense of "type theory, programming"
  Definition: x1 is a value / proof of type / proposition x2 under context x3
       in (type / logical) system x4.
       Notes: Types and propositions are considered equivalent due to the
       Curry-Howard correspondence. Compare to mathematical notation:
       "$x_3 \vdash x_1 : x_2$", with x4 implied by context. In
       proof-irrelevant work (e.g, classical logic), this is usually
       written "$x_3 \vdash x_2$". x1 is most likely to be filled by a
       li construct, or something that potentially reduces to a
       mathematical expression. Quoted arguments should be
       dereferenced with la'e or similar. x1 can be filled by
       zi'o, which means that the proposition is unprovable. x2 can
       be filled by a set of which the x1 value is a member. It may be
       convenient to interpret lo'i as the gadri for types. x3 will
       be a conjunction of du'u sumti, each possibly containing a
       bridi based on ctaipe. x4 need not be consistent. For
       example, almost every programming language has an inconsistent
       type system (by virtue of being Turing-equivalent).
  Place Keywords:
    1. value/proof
    2. type/proposition
    3. context in the sense of "type theory/proof theory"
    4. type system/logic

Questions or comments about this site? Contact [email protected]