View source for ctaipe

==== valsi ====
ctaipe
==== type ====
fu'ivla
==== creator ====
[[personal/krtisfranks|krtisfranks]]
==== time entered ====
Sat Jun 14 08:31:40 2014
 
== English ==
=== Definition #67782 - Preferred ===
 
==== definition ====
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>.
==== notes ====

Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: " MATH
 $x_3 \vdash x_1 : x_2$
 
<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
 $x_3 \vdash x_2$
 
<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).

==== jargon type ====
type theory (computer science) & proof theory (mathematics/philosophy)
==== gloss words ====

<ul><li>[[natlang/en/proof|proof ; proof theory, general mathematics]]</li><li>[[natlang/en/typed|typed ; type theory, programming]]</li></ul>

==== place keywords ====

	1.
          [[natlang/en/value/proof|value/proof]]
<br/>
	2.
          [[natlang/en/type/proposition|type/proposition]]
<br/>
	3.
          [[natlang/en/context|context ; type theory/proof theory]]
<br/>
	4.
          [[natlang/en/type system/logic|type system/logic]]
<br/>

==== created by ====
[[personal/mudri|mudri]]
==== vote information ====
3
     
==== time ====
Sun Sep  6 19:01:57 2015


=== Definition #56829 ===
 
==== definition ====
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>
==== 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|klerctaipe]], [[klesi|klesi]]
==== gloss words ====

<ul><li>[[natlang/en/data type|data type]]</li><li>[[natlang/en/type|type ; data type]]</li></ul>

==== created by ====
[[personal/krtisfranks|krtisfranks]]
==== vote information ====
0
     
==== time ====
Sat Jun 14 08:31:40 2014



<br/><font size="+1">Examples</font>
<hr/>
<dl>
</dl>

=== Definition #67525 ===
 
==== definition ====
x<sub>1</sub> is a value/proof of type/proposition x<sub>2</sub> in (type/logical) system x<sub>3</sub>
==== notes ====
A better definition; proposed by la .mudri.
==== gloss words ====

<ul><li>[[natlang/en/type|type ; type theory]]</li></ul>

==== created by ====
[[personal/krtisfranks|krtisfranks]]
==== vote information ====
0
     
==== time ====
Sun Sep  6 19:04:20 2015



<br/><font size="+1">Examples</font>
<hr/>
<dl>
</dl>

=== Etymology ===