# What does $x : X$ mean?

I've tried to learn type theory a few times, but the notation $x : X$ always trips me up. Does it mean:

1. $x$ represents a fixed but arbitrary inhabitant of the type $X$?
2. The variable $x$ is just "associated" to the type $X$, but not necessarily fixed. In particular, we can now write $\forall xPx$ as shorthand for $(\forall x : X)(Px),$ similarly we can write $\lambda x f x$ as shorthand for $(\lambda x : X)(f x)$ etc.
3. Something else?

Thanks.

• The "meaning" of $x : X$ is that $x$ is of type $X$, no more, no less. You can think of it as being like $x \in X$ if you like but this is misleading. More importantly, types are not like sets: whereas you can ask, "what are the members of this set?", you cannot ask, "what are the inhabitants of this type?" Aug 29, 2013 at 13:01
• @ZhenLin, when you say that we cannot ask, "what are the inhabitants of this type?" what precisely do you mean? Are you basically saying that that although $x : X \vdash [\mbox{whatever}]$ makes sense, nonetheless $\neg(x : X) \vdash [\mbox{whatever}]$ is meaningless? Thus $x : X$ is devoid of a truthvalue. Oct 1, 2013 at 8:02
• In the first place, $\lnot (x : X)$ is not a well-formed formula. But I would not go so far as to say that $x : X$ has no truth value. (My own view is that $x : X$ is well-formed in a given context if and only if $x$ is a term of type $X$ in that context, so it is true if well-formed.) Oct 1, 2013 at 8:18

When you formalize type theory it is probably easiest to work with expressions $C \vdash J$, where $C$ is a context, and $J$ is a judgement. A context is of the form $x_1 : A_1, \ldots, x_n : A_n$ where $x_i$ are free variables and $A_i$ are types. A judgement is either $t : A$ or $t \equiv s : A$ where $A$ is a type and $t$ and $s$ are terms. The terms $s$ and $t$ can contain free variables, but we only consider $C \vdash J$ when every free variable occurring in $J$ already appears in $C$.

When we see $x : A$ as part of a context it is an assumption, so we think of it as saying "for every $x$ of type $A$." However, exactly the same expression $x:A$ can also appear as the judgement $J$ (since each free variable is in particular a term). In this case we read it as saying "$x$ is an object of type $A$."

To give an easy example, we can prove in type theory $x:A, y:B \vdash (x, y) : A \times B$. This says that, given an object $x$ of type $A$ and an object $y$ of type $B$, the term $(x, y)$ is of type $A \times B$. We can also think of this as a function, that takes two inputs (one from $A$ and one from $B$) and produces an element of $A \times B$.

• Thanks, this is helping a lot. So..... can we write things like $x : \mathbb{N} \vdash \forall x(x+1 \neq 0)$? Aug 29, 2013 at 13:07
• The variable $x$ on the RHS is bound by $\forall$, so you should write either $\vdash \forall x : \mathbb{N} . x + 1 \ne 0$ or $x : \mathbb{N} \vdash x + 1 \ne 0$. Aug 29, 2013 at 13:34
• Like Zhen Lin said, $x$ should not be bound on the right hand side. Another issue is that $x + 1 \neq 0$ is not a valid judgement, because every judgement is either of the form $t : A$ or $t \equiv s : A$. To express what you want, you need to use identity types.
– aws
Aug 29, 2013 at 13:46
• A valid expression would be $x : \mathbb{N} \vdash t : I_\mathbb{N}(x + 1, 0) \rightarrow \bot$, where $I_\mathbb{N}(x + 1, 0)$ is the type of "proofs that $x+1$ and $0$ are equal", $\bot$ is the empty type and $t$ is a term that you need to find.
– aws
Aug 29, 2013 at 13:48
• Note also that $\Pi_{x:\mathbb{N}}A$ is a type not dependent on $x$ and finding a proof of $\Pi_{x:\mathbb{N}}A$ in the empty context is equivalent to finding a proof of $A$ in the context $x:A$.
– aws
Aug 29, 2013 at 15:51

x such that the set X; ":" operator denotes "such that". It is basically its type.

$$a : b$$ and the description following the colon is actually the definition (b) of a.

• Wait, in type theory? Aug 29, 2013 at 12:21
• In type theory and programming language theory, the colon sign after a term is used to indicate its type, sometimes as a replacement to the symbol. Aug 29, 2013 at 12:23