無名の自由変数

論理 本編ネタ
  1. \lambda\, x:A.( G(F(x, y), w) ) \;::\; y:B,\; w:D \Rightarrow A \to C
  2. y:B,\; w:D \Rightarrow \lambda\, x:A.( G(F(x, y), w) ) \,:A \to C
  3. y:B,\; w:D \vdash \lambda\, x:A.( G(F(x, y), w) ) \,:A \to C

自由変数を番号にすると：

  1. \lambda\, x:A.( G(F(x, $1), $2) ) \;::\; B,\; D \Rightarrow A \to C
  2. B,\; D \Rightarrow \lambda\, x:A.( G(F(x, $1), $2) ) \,:A \to C
  3. B,\; D \vdash \lambda\, x:A.( G(F(x, $1), $2) ) \,:A \to C

束縛変数も番号にしても構わない。