 Home
 Get A Printable Dictionary
 Search Best Words
 Recent Changes
 How You Can Help
 valsi  All
 valsi  Preferred Only
 natlang  All
 natlang  Preferred Only
 Languages
 XML Export
 user Listing
 Report Bugs
 Utilities
 Status
 Help
 Admin Request
 Create Account

Dictionary record
This is a "best guess" listing for the word "ctaipe"
in
language English,
meaning that only one of
the definitions for this word will be shown
(the one with the
highest total votes).
See all the definitions for
ctaipe.

Back to the main
valsi listing.

valsi 
ctaipe 
type 
fu'ivla 
creator 
krtisfranks 
time entered 
Sat Jun 14 08:31:40 2014 
Examples


English


Definition #67782
 Preferred
[edit]


definition 
x_{1} is a value / proof of type / proposition x_{2} under context x_{3} in (type / logical) system x_{4}. 
notes 
Types and propositions are considered equivalent due to the CurryHoward correspondence. Compare to mathematical notation: "
x_{3} x_{1} : x_{2}", with x_{4} implied by context. In proofirrelevant work (e.g, classical logic), this is usually written "
x_{3} x_{2}". x_{1} 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. x_{1} can be filled by zi'o, which means that the proposition is unprovable. x_{2} can be filled by a set of which the x_{1} value is a member. It may be convenient to interpret lo'i as the gadri for types. x_{3} will be a conjunction of du'u sumti, each possibly containing a bridi based on ctaipe. x_{4} need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turingequivalent).

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 



Examples

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]





