a lojban dictionary editing system

Get A Printable Dictionary
Search Best Words
Recent Changes
How You Can Help
valsi - All
valsi - Preferred Only
natlang - All
natlang - Preferred Only
XML Export
user Listing
Report Bugs
Admin Request
Create Account
Dictionary record
Back to the main valsi listing.
valsi ctaipe
type fu'ivla
creator krtisfranks
time entered Sat Jun 14 08:31:40 2014

Definition #67782 - Preferred [edit]
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: " x3 $\vdash$ x1 : x2", with x4 implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written " x3 $\vdash$ x2". 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).
jargon type type theory (computer science) & proof theory (mathematics/philosophy)
gloss words
place keywords 1. value/proof
2. type/proposition
3. context ; type theory/proof theory
4. type system/logic
created by mudri
vote information 2
time Sun Sep 6 19:01:57 2015


Example #1:

li no ctaipe lo'i kacna'u

(by mudri) [edit]

Example #2:

li bai'ei xy. ctaipe lo'i kacna'u lo du'u li xy. ctaipe lo'i kacna'u

(by mudri) [edit]
Definition #67525 [edit]
definition x1 is a value/proof of type/proposition x2 in (type/logical) system x3
notes A better definition; proposed by la .mudri.
gloss words
created by krtisfranks
vote information 1
time Sun Sep 6 19:04:20 2015


Definition #56829 [edit]
definition x1 is an object/construct fulfilling grammatical role/of (syntactic) category x2 with (sub)typing/data type/of selma'o x3, having specific properties/features/definition x4
notes Quote versus la'e+quote is important in x1; x2 can have arguments of "brivla", "sumti", "cmavo", etc.. Type error results from contextual abuse of x3. See also: klerctaipe, klesi
gloss words
created by krtisfranks
vote information 0
time Sat Jun 14 08:31:40 2014



Currently, jbovlaste will accept data for 69 languages.
You are not logged in.

  recent changes jbovlaste main
This is jbovlaste, the lojban dictionary system.
The main code was last changed on Wed 07 Oct 2020 05:54:55 PM PDT.
All content is public domain. By submitting content, you agree to place it in the public domain to the fullest extent allowed by local law.
jbovlaste is an official project of the logical language group, and is now headed by Robin Lee Powell.
E-mail him if you have any questions.
care to log in?