>>755
>>>754
>自分でα変換いうてるやん
>定義しってんなら
>∀x∈ℕ.∃(x+1).x<x+1　が
>∀x∈ℕ.∃y.x<y　になるしかないやん

またまた ずさんなことを言うｗ

∀x∈ℕ.∃(x+1).x<x+1
　↓
∀x∈ℕ.∃y.x<y
にするためには、y=x+1と定義しないと。その定義が必要でしょ？

一般に
・∀x∈ℕ.∃(x+1).x<x+1
・∀x∈ℕ.∃y.x<y

この二つの式は意味違うし、そもそも”∃y∈ℕ”とかも要りそうに思うけど
まあ、ともかくあんたの思考は、ずさんそのものだね　；ｐ）

(参考)（α-変換）
https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97
ラムダ計算
ラムダ計算（ラムダけいさん、英語: lambda calculus）は、計算模型のひとつで、計算の実行を関数への引数の評価（英語: evaluation）と適用（英語: application）としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。

歴史
元々チャーチは、数学の基礎となり得るような完全な形式体系を構築しようとしていた。彼の体系がラッセルのパラドックスの類型に影響を受けやすい（例えば論理記号として含意 → を含むなら、λx.(x→α) にYコンビネータを適用してカリーのパラドックスを再現できる）ということが判明した際に、彼はそこからラムダ計算を分離し、計算可能性理論の研究のために用い始めた。この研究からチャーチは一階述語論理の決定可能性問題を否定的に解くことに成功した。

α-変換
アルファ変換の基本的なアイデアは、束縛変数の名前は重要ではない、ということにある。例えば、 λx. x と λy. y は同じ関数を表している。
しかし、ことはそう単純ではない。
ある束縛変数の名前を置換してもよいかどうかには、いくつかの規則が絡んでくる。例えば、ラムダ式 λx. λy. x 中の変数 x を y に置き換えると、 λy. λy. y となるが、これは最初の式とはまったく異なるものを表すことになる。