Упражнения из Барендрегта, глава 15
May. 17th, 2015 08:59 pmОт упражнений остальных глав второй части монографии в 27 уже морщит, как в 50, поэтому перейду сразу к пятнадцатой, где вводится понятие редукции-оракула, которое анализирует доказуемость в осмысленной теории H и говорит, на что еще нет смысла тратить время.
15.4.1. Покажем, что любой терм M Ωη-сильно нормализуем:
η-редукцию всегда можно отложить, при этом
любой терм имеет единственную Ω-нормальную форму и
единственную η-нормальную форму.
15.4.2. Будем писать x \in_R M, если x входит в любой N =R M.
Покажем, что
(i) x \in_βηΩ A x, если A = ω ω, где ω = a, x, z: z (a a (x Ω)):
редукция A x ->>β <...<A (χ^n Ω)>...> не порождает Ω-редексов;
(ii) имеется замкнутый терм O, такой, что
O x [n] z ->>β z Ω~n (O x [n + 1] z) и x \in_βηΩ O x [0]:
возьмем O = Θ (o, x, n, z: (W z n) (o x (S+ n) z)),
где W = Θ (w, z, n: (Zero n) z (w z (P- n) Ω));
(iii) для любого замкнутого F есть замкнутый H, такой, что
H c i a ->>β x: x I (F c a (H c i (S+ a))) и x \in_βηΩ H c x [0]:
возьмем H = Θ (h, c, i, a: (x: x I (F c a (h c i (S+ a)))));
ни в редукции O, ни в редукции H не появляется Ω-редексов.
15.4.3. Пусть у нас есть такая рекурсивная функция f, что
f(n) = 0, если n входит в некоторое множество, иначе f(n) = 1.
Тогда покажем, что
(i)-(ii) λ + {Ω [n] = T | f(n) = 0} + {Ω [n] = F | f(n) = 1} непротиворечива:
λ-определим f через G и вспомним, что терм Ω легкий, поэтому
его можно, в частности, приравнять к n: Zero (G n);
(iii) без нерекурсивных функций не существует и континуума.
15.4.4 (Клоп). Практически решено в указании.
15.4.5. Пусть T = λ + {Ω [0] Z = Ω [1] Ζ | Z замкнут}. Покажем, что
(i) (Якопини) в T недоказуемо Ω [0] = Ω [1]:
заметим, что теория λ + Ω = n: (Zero n) x (y: x y)
непротиворечива из-за легкости Ω и при этом содержит в себе T,
но без аксиомы η недоказуемо равенство x = y: x y;
(ii) если T' = T + (Ω (x: Ω [0] x) = T) + (Ω (x: Ω [1] x) = F),
то T' непротиворечива, а T'ω противоречива:
в T'ω из дополнительных аксиом T следует Ω [0] = Ω [1],
а дополнительные аксиомы T' приведут к T = F, но T # F,
непротиворечивость же T' никому нахуй не сдалась.
15.4.6-15.4.10. Дальше совсем скучно.
15.4.1. Покажем, что любой терм M Ωη-сильно нормализуем:
η-редукцию всегда можно отложить, при этом
любой терм имеет единственную Ω-нормальную форму и
единственную η-нормальную форму.
15.4.2. Будем писать x \in_R M, если x входит в любой N =R M.
Покажем, что
(i) x \in_βηΩ A x, если A = ω ω, где ω = a, x, z: z (a a (x Ω)):
редукция A x ->>β <...<A (χ^n Ω)>...> не порождает Ω-редексов;
(ii) имеется замкнутый терм O, такой, что
O x [n] z ->>β z Ω~n (O x [n + 1] z) и x \in_βηΩ O x [0]:
возьмем O = Θ (o, x, n, z: (W z n) (o x (S+ n) z)),
где W = Θ (w, z, n: (Zero n) z (w z (P- n) Ω));
(iii) для любого замкнутого F есть замкнутый H, такой, что
H c i a ->>β x: x I (F c a (H c i (S+ a))) и x \in_βηΩ H c x [0]:
возьмем H = Θ (h, c, i, a: (x: x I (F c a (h c i (S+ a)))));
ни в редукции O, ни в редукции H не появляется Ω-редексов.
15.4.3. Пусть у нас есть такая рекурсивная функция f, что
f(n) = 0, если n входит в некоторое множество, иначе f(n) = 1.
Тогда покажем, что
(i)-(ii) λ + {Ω [n] = T | f(n) = 0} + {Ω [n] = F | f(n) = 1} непротиворечива:
λ-определим f через G и вспомним, что терм Ω легкий, поэтому
его можно, в частности, приравнять к n: Zero (G n);
(iii) без нерекурсивных функций не существует и континуума.
15.4.4 (Клоп). Практически решено в указании.
15.4.5. Пусть T = λ + {Ω [0] Z = Ω [1] Ζ | Z замкнут}. Покажем, что
(i) (Якопини) в T недоказуемо Ω [0] = Ω [1]:
заметим, что теория λ + Ω = n: (Zero n) x (y: x y)
непротиворечива из-за легкости Ω и при этом содержит в себе T,
но без аксиомы η недоказуемо равенство x = y: x y;
(ii) если T' = T + (Ω (x: Ω [0] x) = T) + (Ω (x: Ω [1] x) = F),
то T' непротиворечива, а T'ω противоречива:
в T'ω из дополнительных аксиом T следует Ω [0] = Ω [1],
а дополнительные аксиомы T' приведут к T = F, но T # F,
непротиворечивость же T' никому нахуй не сдалась.
15.4.6-15.4.10. Дальше совсем скучно.
