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
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