http://zeit-raffer.livejournal.com/ ([identity profile] zeit-raffer.livejournal.com) wrote in [personal profile] juan_gandhi 2015-05-20 06:59 pm (UTC)

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

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

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

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

Post a comment in response:

This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting