# Set theoretic definition of terms of the untyped lambda calculus

I am trying to translate the following definition (in Agda) of intrinsically scoped terms of the untyped lambda calculus into more mathematical (in particular set theoretical) notation:

data _⊢_ : Context → Type → Set where

_ : ∀ {Γ}
→ Γ ∋ ★
-----
→ Γ ⊢ ★

ƛ_  :  ∀ {Γ}
→ Γ , ★ ⊢ ★
---------
→ Γ ⊢ ★

_·_ : ∀ {Γ}
→ Γ ⊢ ★
→ Γ ⊢ ★
------
→ Γ ⊢ ★
`

Variables are represented by De Bruijn indices.

This is my current attempt:

The set of terms in context $$\Gamma$$ (which is just a natural number) is denoted by $$\Lambda(\Gamma)$$ and is inductively generated by the following functions:

• $$\textsf{var}_\Gamma : \{1, \dots, \Gamma\} \to \Lambda(\Gamma)$$
• $$\textsf{abs}_\Gamma : \Lambda(\Gamma + 1) \to \Lambda(\Gamma)$$
• $$\textsf{app}_\Gamma : \Lambda(\Gamma) \times \Lambda(\Gamma) \to \Lambda(\Gamma)$$

I am not happy with this attempt. Here are my thoughts:

• I know that for each $$\Gamma$$, the set $$\Lambda(\Gamma)$$ contains infinitely many terms, but still it seems to be wrong to define each $$\Lambda(\Gamma)$$ in terms of a still undefined set $$\Lambda(\Gamma + 1)$$. See $$\textsf{abs}_\Gamma$$.
• It feels strange to only write down the function signatures without saying what the functions are actually "doing". I could say that $$\{1, \dots, \Gamma\} \subseteq \Lambda(\Gamma)$$ and that $$\textsf{var}_\Gamma$$ is the inclusion map, but this would only solve a part of the problem, I think.

If someone could help me with this, it would be much appreciated.

• > It feels strange to only write down the function signatures without saying what the functions are actually "doing". Do you mean a 'data constructor'? Apr 16 at 10:48
• Yes, I'm talking about the constructors. I know that they just construct the elements of the set of terms, so what they "do" is encoded in the signatures. In set theoretic terms there is a distinction though between a function signature and its definition, isn't it? Apr 16 at 11:01