Theorem 15.12 Every λ-model satisfies all the provable equations of the formal theory λβ.
Вопрос в том, можно ли выразить свойство Functional completeness в виде простого равенства, чтобы это было применимо. Там же еще потребуется префикс "для любой формулы в лямбде существует формула без лямбды", вот он, подозреваю, не моделируется.
Но в любом случае есть смысл приводить это доказательство в вики, как основной факт об обсуждаемой структуре, не требуя прочесть предварительно 235 страниц монографии.
Вам не трудно сослаться еще и на "дан Тёрнером в 79 году"? Хочу понять, он доказывал для самой лямбды или для моделей?
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2015-05-20 06:59 pm (UTC)Вопрос в том, можно ли выразить свойство Functional completeness в виде простого равенства, чтобы это было применимо. Там же еще потребуется префикс "для любой формулы в лямбде существует формула без лямбды", вот он, подозреваю, не моделируется.
Но в любом случае есть смысл приводить это доказательство в вики, как основной факт об обсуждаемой структуре, не требуя прочесть предварительно 235 страниц монографии.
Вам не трудно сослаться еще и на "дан Тёрнером в 79 году"? Хочу понять, он доказывал для самой лямбды или для моделей?