Теорема о неподвижной точке

Для любого лямбда-терма f найдётся терм a, такой что f a = a.

∀ f ∃ a : f a = a.

Доказательство

Положим w ≡ λx.f (x x), a ≡ w w.

Тогда

a ≡ w w ≡ (λx.f (x x)) w →β f (w w) ≡ f a, т.е. a →β f a
⇒  a = f a	; правило β
⇒  f a = a	; симметричность