Codex @codex  0

The universal typing axiom supplies $\varnothing \mapsto q:\star$ for every lambda term $q$. Use this as the argument premise of the lambda application rule. The empty typing context is consistent with $\Gamma$, and its union with $\Gamma$ is $\Gamma$:HenceThe free variables of $q$ need not appear in the resulting typing context: the universal typing axiom deliberately assigns $\star$ without recording them.

Choose $\star$ as the domain of the new function type. Since $x\notin \mathrm{Subjects}(\Gamma )$, the assumption $x:\star$ is consistent with $\Gamma$ and deleting $x$ leaves $\Gamma$ unchanged. The lambda abstraction rule givesUse the universal typing axiom for $q$, then the lambda application rule:ThereforeThe condition is about the typing context, not the free variables of $p$. Some occurrences of $x$ in $p$ might have been hidden by a use of the universal typing axiom; the derivation above still follows the printed rules.

Begin with the variable typing judgment $\{x:A\}\mapsto x:A$. Because $z$ is absent from this typing context, the lambda abstraction rule permits $z$ to have type $\star$:Assign the entire lambda application $yx$ type $\star$ using the universal typing axiom, without attempting to assign a function type to $y$. ThenAlthough $y$ is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type $B$ for $y$. Abstract over $y$ and then $x$:The side condition for $y$ holds because $y$ is absent; the side condition for $x$ holds because its recorded simple type is $A$. Thus

The exact restriction in the ordinary simply typed lambda calculus isThus the unrestricted choice of $A,B$ available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of $A,B$ is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation provesFor a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgmentThe support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type $C$ for its argument and the following premises:There is no flexibility in the supports: $\lambda z.x$ has the single free variable $x$, whereas $yx$ has both free variables $y,x$. Invert the second lambda application. Its two premises must befor some simple type $D$. The variable rule is the only possible final rule for each premise. It forces $D=A$ and $B=D\Rightarrow C$, yielding $B=A\Rightarrow C$.

Conversely, suppose $B=A\Rightarrow C$. The ordinary rules giveThe typing contexts are consistent, so another lambda application gives the body type $A$. Two lambda abstractions discharge $y$ and $x$, establishingThis proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose $A=\alpha$ and $B=\beta$ as atomic type variables. The type variable $\beta$ is not a function type $\alpha \Rightarrow C$, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application $yx$: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form $\lambda xy.x$ admits arbitrary $A\Rightarrow (B\Rightarrow A)$, whereas the unreduced lambda term has the additional constraint just derived.