Theorem 15.12 Every λ-model satisfies all the provable equations of the formal theory λβ.

Вопрос в том, можно ли выразить свойство Functional completeness в виде простого равенства, чтобы это было применимо. Там же еще потребуется префикс "для любой формулы в лямбде существует формула без лямбды", вот он, подозреваю, не моделируется.

Но в любом случае есть смысл приводить это доказательство в вики, как основной факт об обсуждаемой структуре, не требуя прочесть предварительно 235 страниц монографии.

Вам не трудно сослаться еще и на "дан Тёрнером в 79 году"? Хочу понять, он доказывал для самой лямбды или для моделей?