Simply typed lambda calculus

Does anyone have an idea how to prove in lambda calculus that bool contains two terms? I am quite new to it and I haven't succeeded in doing so. I came up with two terms so far, which would guarantee existence: $\lambda x_{\alpha}.\lambda y_{\alpha}.x$ and $\lambda x_{\alpha}.\lambda y_{\alpha}.y$. These terms are clearly of the type $Bool$.

But how can we prove that there are no other ones? I have tried induction on terms, induction on types, but everything failed so far. Any tips are welcome, thanks.

• – Hanno Mar 21 '17 at 7:59

At any rate, you want to do an induction on normal forms. The statement you want to prove can be formulated as $$\forall t\in \mathcal{N}. t\text{ has type } Bool\iff(t = \lambda x_\alpha.\lambda y_\alpha. x \lor t = \lambda x_\alpha.\lambda y_\alpha. y)$$ where $\mathcal{N}$ is the set of ($\alpha$-equivalence classes of) normal forms and (thus) equality, here, means $\alpha$-equivalence. $\mathcal{N}$ is roughly an inductively defined set and so to prove a statement about all its elements requires induction. However, since the terms include binding forms things get a bit hairier. In particular, and this will be a common move, you need to strengthen the induction hypothesis to hold for open terms. So instead of doing induction over normal forms, you want to do induction over "normal-forms-in-context". (We can simplify significantly for this particular problem [how?], but I will work more generally.) What's happening is that closed terms (and normal forms) do not form an inductively defined set (at least not in a natural way), but terms-in-context do.
Given a list of types called $\Gamma$, we can define $\mathtt{vars}(\Gamma)\equiv\{x^i\mid i < \#\Gamma\}$ to be a corresponding set of variables where $\#\Gamma$ is the length of $\Gamma$. Finally, define $$\alpha^\Gamma \equiv \begin{cases}\alpha, & \Gamma = \cdot\\\beta\to\alpha^\Delta, & \Gamma = \beta,\Delta\end{cases}$$ and $$\mathtt{abstract}(\Gamma,x)\equiv\begin{cases}x, &\Gamma = \cdot\\\lambda x^{\#\Delta}_\beta.\mathtt{abstract}(\Delta,x), & \Gamma = \beta,\Delta\end{cases}$$ The strengthened (but not quite correct) induction hypothesis is now $$\forall \Gamma.\forall t\in \mathcal{N}.\ \cdot\vdash t:\alpha^\Gamma\iff t \in\{\mathtt{abstract}(\Gamma,x)\mid x \in \mathtt{vars}(\Gamma)\land \Gamma\vdash x:\alpha\}$$ where $\Gamma\vdash t : \alpha$ means $t$ has type $\alpha$ in context $\Gamma$. As stated, this is not true, but if we restrict $\Gamma$ to lists of "atomic" types, it is. The original theorem is recovered in the $\alpha,\alpha,\cdot$ case.
• The main change is that we only need to consider lists of types containing only $\alpha$ at which point we only need to know the length of the list. Thus all the recursions and the induction of $\Gamma$ can be replaced with recursions/induction of the number of $\alpha$'s to the left of the arrow in the type. This is mostly a notational savings, though we can drop the $\Gamma\vdash x:\alpha$ condition. For example, instead of $\alpha^\Gamma$, we'd have $$\alpha^n\equiv \begin{cases}\alpha, & n= 0 \\ \alpha\to\alpha^m, & n= m+1\end{cases}$$ – Derek Elkins Mar 21 '17 at 7:02
• Yes, right nested arrow types, i.e. $\alpha$, $\alpha\to\alpha$, $\alpha\to(\alpha\to\alpha)$, etc. Unrelatedly, I made some significant but small corrections, see the edits. Also, technically I could get rid of $\mathcal{\Gamma}$ and just use $\mathcal{N}$, or I could get rid of $\alpha^\Gamma$ and keep $\mathcal{N}_\Gamma$ and say $\Gamma\vdash t:\alpha$ which would require a lemma $\Gamma\vdash t:\alpha \iff \cdot\vdash t:\alpha^\Gamma$ which is usually true (via $\eta$-conversion) to connect it to the original problem statement – Derek Elkins Mar 21 '17 at 7:39
• Bingo. Yes, you do. Your original statement is false if "atomic" doesn't exclude types with normal forms. For example, if $\alpha=\mathbb{N}$ then there is an infinite number of normal forms. If $\alpha=1$ (the unit type) and you have $\eta$-conversion for it, then $\lambda x_1.\lambda y_1.x = \lambda x_1.\lambda y_1.\langle\rangle = \lambda x_1.\lambda y_1.y$ and you only have one $\beta\eta$-normal form. So what we really need from $\alpha$ is for it to not have any normal form terms. – Derek Elkins Mar 21 '17 at 8:10
• It's over normal forms because we want to know something about all normal forms (of the appropriate type), namely that they are contained in a particular finite set. If the statement had been about arbitrary terms, then it would have been an induction over terms-in-context. That said, there are an infinite number of (arbitrary) terms for any inhabited type. For any term $t$ of that type, $(\lambda x_\alpha.x)t$ is another term. We usually identify values of a type with the normal forms at that type. Non-norrmal terms are essentially intermediate stages of calculation in this view. – Derek Elkins Mar 21 '17 at 8:29