Упражнения из Барендрегта, глава 4

Немного отклонюсь от плана "Как читать Барендрегта" и от третьей главы монографии внезапно перейду аж сразу к четвертой. Внимание: будут ссылки на упражнения второй главы.

4.3.1. См. упр. 2.4.12 (i).

4.3.2 (Виссер). Замкнутый терм M называется легким, если для всех замкнутых термов N теория λ + (M = N) непротиворечива. В предположении легкости терма M докажем следующие утверждения.
(i) M N легкий для любого замкнутого терма N:
в непротиворечивой λ + (M = K M) выводимо M N = K M N => M N = M,
откуда следует, что λ + (M N = Q) непротиворечива для любого замкнутого Q;
(ii) M неразрешим, иначе бы M N1 ... Nn = I для некоторых Ni,
а из (i) следовало бы, что λ + (I = K) непротиворечива, но I # K (упр. 2.4.2 (i));
(iii)-(iv) если функция f(n) = #Pn рекурсивна, то она представима некоторым лямбда-термом F, таким, что F [n] = Pn, и
тогда в непротиворечивой λ + (M = F) выводимы M [n] = F [n] => M [n] = Pn для всех n;
если же f(i) не является рекурсивной функцией, то я в эти игры не играю, потому что не считаю вопрос "Есть ли Б-г на Марсе?" уместным в этой теме.
(v) λ + {M = N | M и N легкие} непротиворечива:
мы уже знаем о непротиворечивости осмысленной теории H, которая приравнивает все неразрешимые термы, а в пунтке (ii) мы доказали, что все легкие термы неразрешимы.

4.3.3. Модельные соображения не включены в программу намеренно.

4.3.4. Покажем, что не существует такого M, чтобы для любых N теория H + (M = N) была непротиворечивой:
в 4.3.2 (ii) мы доказали, что M должен быть неразрешимым, но
в H все неразрешимые термы приравнены к W3 = (x: x x x) (x: x x x), а
из упр. 2.4.12 (ii) мы знаем, что I # W3.