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

После пятнадцатой главы в плане "Как читать Барендрегта" остается только одна, самая главная - шестнадцатая. В ней, наконец-то, показано, что HP-полное расширение всех осмысленных λ-теорий - это H*, и другого не дано.

16.5.1. Покажем, что
(i) для любого замкнутого терма Z в теории H доказуемо
Z Ω~n = Ω для некоторого n:
если Z неразрешим, то он равен Ω по определению H, иначе
Z имеет головную нормальную форму x1,..., xn: xi Z1 ... Zn, и тогда
Z Ω~n неразрешим и равен Ω по определению H;
(ii) если A x ->> z: z (A (x Ω)), то A Z = A Z' доказуемо
в теории H* для любых термов Z и Z', а
в теории H только для замкнутых Z и Z':
ввиду (i) для некоторого n имеем
A Z ->>βηΩ z1: z1 (...(zn: zn (A Ω))...) <<-βηΩ A Z',
в HP-полной H* содержится, в частности,
непротиворечивая Hω ввиду ее осмысленности,
поэтому там выводимо также следствие A Z = A Z',
но в H правило ω не имеет места.

16.5.2. Покажем, что в H имеет место ext0, но не имеет места ext:
ext влечет правило η, а оно не имеет места в H;
пусть теперь M x = N x, где M и N замкнуты, тогда
M x = N x = Ω может быть только по причине M = N = Ω,
а в противном случае M = x1,..., xm: xi M1 ... Mn и N = y1,..., yn: yj N1 ... Nn,
для которых даже в λ доказуемо M = N (см. упр. 2.4.13).

16.5.3-16.5.7. Обойдемся без альтернативных доказательств теорем,
рисования редукционных графов, рассмотрения оригинальных
построений Морриса и теоремы Мальцева.

16.5.9. Покажем, что терм M разрешим тогда и только тогда,
когда теория λ + (M = Y K) противоречива:
(=>) если M разрешим, то для некоторых термов N1,..., Nn
M N1 ... Nn = K, при этом Y K N1 ... Nn = Y K, но K # Y K (см. упр. 6.8.3);
(<=) если λ + (M = Y K) противоречива, то M разрешим, иначе
в непротиворечивой H выводилось бы M = Ω = Y K.