https://wiki.lojban.io/index.php?action=history&feed=atom&title=ctaipectaipe - Revision history2026-04-28T02:46:26ZRevision history for this page on the wikiMediaWiki 1.45.3https://wiki.lojban.io/index.php?title=ctaipe&diff=3362&oldid=prevNalvaizmiku: Import words via API2026-01-13T14:39:34Z<p>Import words via API</p>
<p><b>New page</b></p><div>==== valsi ====<br />
ctaipe<br />
==== type ====<br />
fu'ivla<br />
==== creator ====<br />
[[personal/krtisfranks|krtisfranks]]<br />
==== time entered ====<br />
Sat Jun 14 08:31:40 2014<br />
<br />
== English ==<br />
=== Definition #67782 - Preferred ===<br />
<br />
==== definition ====<br />
x<sub>1</sub> is a value / proof of type / proposition x<sub>2</sub> under context x<sub>3</sub> in (type / logical) system x<sub>4</sub>.<br />
==== notes ====<br />
<br />
Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: " MATH<br />
$x_3 \vdash x_1 : x_2$<br />
<br />
<span class="MATH"><i>x</i><sub>3</sub> <img alt="$\vdash$" src="/jbovlaste_export/56MMWcQ56x/img1.png" style="height: 1.61ex; vertical-align: -0.12ex; "/> <i>x</i><sub>1</sub> : <i>x</i><sub>2</sub></span>", with <span class="MATH"><i>x</i><sub>4</sub></span> implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written " MATH<br />
$x_3 \vdash x_2$<br />
<br />
<span class="MATH"><i>x</i><sub>3</sub> <img alt="$\vdash$" src="/jbovlaste_export/56MMWcQ56x/img1.png" style="height: 1.61ex; vertical-align: -0.12ex; "/> <i>x</i><sub>2</sub></span>". <span class="MATH"><i>x</i><sub>1</sub></span> is most likely to be filled by a [[li|li]] construct, or something that potentially reduces to a mathematical expression. Quoted arguments should be dereferenced with [[la'e|la'e]] or similar. <span class="MATH"><i>x</i><sub>1</sub></span> can be filled by [[zi'o|zi'o]], which means that the proposition is unprovable. <span class="MATH"><i>x</i><sub>2</sub></span> can be filled by a set of which the <span class="MATH"><i>x</i><sub>1</sub></span> value is a member. It may be convenient to interpret [[lo'i|lo'i]] as the gadri for types. <span class="MATH"><i>x</i><sub>3</sub></span> will be a conjunction of [[du'u|du'u]] sumti, each possibly containing a bridi based on [[ctaipe|ctaipe]]. <span class="MATH"><i>x</i><sub>4</sub></span> need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent).<br />
<br />
==== jargon type ====<br />
type theory (computer science) & proof theory (mathematics/philosophy)<br />
==== gloss words ====<br />
<br />
<ul><li>[[natlang/en/proof|proof ; proof theory, general mathematics]]</li><li>[[natlang/en/typed|typed ; type theory, programming]]</li></ul><br />
<br />
==== place keywords ====<br />
<br />
1.<br />
[[natlang/en/value/proof|value/proof]]<br />
<br/><br />
2.<br />
[[natlang/en/type/proposition|type/proposition]]<br />
<br/><br />
3.<br />
[[natlang/en/context|context ; type theory/proof theory]]<br />
<br/><br />
4.<br />
[[natlang/en/type system/logic|type system/logic]]<br />
<br/><br />
<br />
==== created by ====<br />
[[personal/mudri|mudri]]<br />
==== vote information ====<br />
3<br />
<br />
==== time ====<br />
Sun Sep 6 19:01:57 2015<br />
<br />
<br />
=== Definition #56829 ===<br />
<br />
==== definition ====<br />
x<sub>1</sub> is an object/construct fulfilling grammatical role/of (syntactic) category x<sub>2</sub> with (sub)typing/data type/of selma'o x<sub>3</sub>, having specific properties/features/definition x<sub>4</sub><br />
==== notes ====<br />
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|klerctaipe]], [[klesi|klesi]]<br />
==== gloss words ====<br />
<br />
<ul><li>[[natlang/en/data type|data type]]</li><li>[[natlang/en/type|type ; data type]]</li></ul><br />
<br />
==== created by ====<br />
[[personal/krtisfranks|krtisfranks]]<br />
==== vote information ====<br />
0<br />
<br />
==== time ====<br />
Sat Jun 14 08:31:40 2014<br />
<br />
<br />
<br />
<br/><font size="+1">Examples</font><br />
<hr/><br />
<dl><br />
</dl><br />
<br />
=== Definition #67525 ===<br />
<br />
==== definition ====<br />
x<sub>1</sub> is a value/proof of type/proposition x<sub>2</sub> in (type/logical) system x<sub>3</sub><br />
==== notes ====<br />
A better definition; proposed by la .mudri.<br />
==== gloss words ====<br />
<br />
<ul><li>[[natlang/en/type|type ; type theory]]</li></ul><br />
<br />
==== created by ====<br />
[[personal/krtisfranks|krtisfranks]]<br />
==== vote information ====<br />
0<br />
<br />
==== time ====<br />
Sun Sep 6 19:04:20 2015<br />
<br />
<br />
<br />
<br/><font size="+1">Examples</font><br />
<hr/><br />
<dl><br />
</dl><br />
<br />
=== Etymology ===</div>Nalvaizmiku