ctaipe fu'ivla

x1 is a value / proof of type / proposition x2 under context x3 in (type / logical) system x4.

Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: "x3 \vdash x", with x4 implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written "x3 \vdash x". 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).


In notes:

cei'i (exp!)
pro-bridi: the universal predicate
gai'o (exp!)
pro-bridi: the empty predicate
mai'i (exp!)
pro-sumti: the universal argument/value; syntactically-contextually and type-permitted maximally generic in its typing
zai'o (exp!)
pro-sumti: the empty argument/value; syntactically-contextually and type-permitted maximally generic in its typing