ラムダ計算の正式な記述を読むとき、変数のセットは常に無限に数えられるように定義されているようです。なぜこのセットが有限にならないのかは明らかです。変数のセットを有限として定義することは、許容できない形で用語構造を制限することになります。しかし、なぜ無限に無限になることを許さないのですか？ラムダ計算の変数のセットは、通常、無限に数えられると定義されていますか？
現在のところ、私が受け取ったこの質問に対する最も賢明な答えは、数え切れないほど無限の変数を選択すると、自然なアルファ書き換えのように新鮮な変数を選択する方法を記述する変数を列挙することができるということです。
私はこの質問に対する決定的な答えを探しています。
このセットを数える必要がある理由は非常に簡単です。あなたが変数でいっぱいのバッグを持っていたと想像してください。このバッグに含まれる変数の数を数えない方法はありません。
袋は袋に同形であることに注意してください。
数学とロジックのほとんどの定義と構造には、目的の目的を達成するために必要な最小限の装置しか含まれていません。あなたが指摘しているように、有限個以上の変数が必要になることがあります。しかし無数の無限大が必要なので、なぜもっと多くを許可するのですか？
数え切れないほどのものは通常uncomputable elementsのようです。私は確信していませんすべて無数のコレクションはこのプロパティを持っていますが、私は彼らが強く疑う。
結果として、合理的な方法でこれらの要素の名前を書き出すことさえできませんでした。たとえば、piのような数字とは異なり、ある数字の桁数を超えて数字Chaitin's constantを書き出すプログラムを作成することはできません。計算可能な実数のセットは無限であるため、得られる「追加の」実数は計算できません。
私はまたあなたが無限に無限であるセットから何かを得るとは思わない。だからあなたは、（私が見る限り）計算できない名前を有益に導入するだろう。
変数の可算数、およびそれらとℕ間計算の全単射を持って、私たちはΛとℕ間の全単射を作成することができます：
表記⌜L ⌝はLの符号化を表す教会の数字であるc _ {＃L}を表す。すべての集合Sについて、＃Sは集合{#L | L∈S}である。
これは、ラムダ計算は決定可能でないことを証明するために私達を許可する：
非自明な（ない∅またはΛ）もαの下で閉じセットとβ平等は（L∈AとL場合みようβ= M、M∈A）。 Bを集合{L | L←L∈A}である。集合#Aがrecursiveであると仮定する。 f（x∈Aの場合はf（x）= 1、x∉Aの場合は0）はμ-recursive functionでなければなりません。すべてのμ-再帰関数は、*λが定義されているので、そのためにFが存在する必要があります：
F⌜L⌝= C_1⇔⌜L⌝∈A
F⌜L⌝= C_0⇔⌜L⌝∉A
G≡λnとする。 M_0はB中の任意のλ項であり、M_1はB中にない任意のλ項である。ただし、＃nは計算可能であり、従ってλ定義可能であることに注意されたい。
「今はBでG⌜GIsですか？」という質問をしてください。はいの場合、G⌜G⌝= M_1∉Bなので、G⌜G⌝はBには属していない可能性があります（Bはβ=で閉じていることに注意してください）。そうでなければ、G⌜G⌝= M_0∈Bであるので、Bに入っていなければならない。
これは矛盾しているため、Aは再帰的ではない可能性があるため、閉鎖不能β=非自明集合再帰的です。
{L | Lβ= true}はβ=および非自明で閉じられるので、再帰的ではない。これはラムダ計算が決定できないことを意味します。
*すべての計算機能がλ定義可能であることを証明（我々はλ項FようにFのC_ {N1} C_ {N2} ... = C_ {F（N1、N2を有することができ、 ...）}）と、この回答の証拠は、"Lambda Calculi With Types" by Henk Barendregt（セクション2.2）にあります。