Бурбаки - Книга 1. Теория множеств (947355), страница 69
Текст из файла (страница 69)
СТ2. При типизации Т)х, в, А1 х,— переносимый терм. типа !ЬЬ(х!), г! — переносимый терм типа 5)(х, А) и А» — переносимый терм типа ЬЬЬ(А»). Эти критерии немедленно вытекают из определений. СТЗ. Если К и К' — переносимые соотношения, то жв верн!» и для соотношений „не К', К или К'", „К и К'", „К=1»К'"„ „К(=фК'". СТ4. Если термы () и ()' суть переносимые термы типов, соответственно 5 и 5', то ((), 1У) — переносимый терм типа 5Х 5'. Если () и ()' суть переносимые термы типов соответственно (ЬЬ(5) и (ЬЬ(5'), то () '!(()' есть переносимый терм типа 1)з(5Х 5') и 1)з(()) есть переносимый терм типа 4Ь(р13(5)).
СТ6. Если () и (à — переносимые термы одного и того же типа 5, то соотношение () =1У пврекосимо. Если () — переносимый терм типа 5 и 1У вЂ” пвреносимей терм типа 313(5), то соотношение () ~()' пврвносимо. Если () и ()' суть переносимые термы типа 54Ь(5), соотношение ()~(У переносило. Мы предоставляем читателю доказательство этих критериев, вытекающих немедленно из определений и свойств биекций и их канонических распространений (см. 3 1, критерий С5Т2. и гл. !1, 3 3, п' 7).
СТ6. Яля всякой схемы конструкции ступени 5 яад и+т термами 5(х, А) есть переносимый терм типа 54Ь(5(х, А)) для типизации Т)х, а. А1. ГЛ.ИС СТРУКТУРЫ я ПРИЛОЖЕНИЕ. КРИТЕРИИ ПЕРЕНОСИМОСТИ 285 Это вытекает из СТ2 и СТ4 и доказывается шаг эа шагом, следуя эа построением схемы Я. СТ7.
Если К вЂ” такое соотношение, что Т~К истинно е,)', то К переносимо при Т. Если (), О' — дга таких терма, что 'Т=ф(О=О') истинно е,Т, и если О переносимий терм типа 8 при Т, то то же верно и для О'. Вторая часть критерия вытекает из определения переносимого терма и схемы 86 (гл. 1, ф 5, п'1), входящей в теорию д,.
С другой стороны, соотношение Т)х, з, А1 переносимо (при типизации Т)х, з, А1) в силу СТЗ, СТ5 и СТ6; следовательно, соотношение Т!х, з, А!(фТ!у, з', А1 является теоремой теории,T, и, значит, то же верно и для Т! у, з', А!. Предположение об К влечет, что К)х, з1 есть теорема теории <T,; с другой стороны, в силу критерия СЗ (гл.
1, ф 2, п'4), Т)у, з', А1=)ьК)у, з'! есть теорема теории гТ, так как буквы х, и г) не являются константами теории д'; следовательно, К(у, з'1 есть теорема теории Т,, из чего вытекает, что соотношение К!х, з)(фК)у, з'! также является теоремой теории Кы откуда получается первая часть критерия. СТ8. Пусть г — букеа, отличная от констант теории Т и букв, встречающихся е типизации Т(х, з, А1. Пусть 3— гхема конструкции ступени из и+т термов и пусть Т' есть типизация „Т~х, з, А1 и я~8(х, А)". Наконец, пусть К вЂ” соотношение, не содержащее г. При этих условиях, если К переносило (е 7) при типизации Т', то К переносимо при типизации Т е теории г7", полученной добаелением к аксиомам теории,T соотношения 8(х, А) Ф И. Это тотчас же получается методом вспомогательной константы гл.
1, $3, п'3 и ф 4, и'!). Предыдущий критерий применяется обычно в двух следующих случаях: а) ступень Б(х, А) имеет вид ф(Х); б) схема 8 тождественна с одной из схем 87(! < / < р), входящих в типизацию Т. ш В этих двух случаях из критерия СТ8 можно заключить, что К переноснмо в теории Т при типизации Т, нбо 5(х, А) Ф И есть теорема теории ~,. СТ9, Пусть К вЂ” соотношение, переносимое при типизации Т, и пусть К' — такое соотношение, что Т~(К(='РК') — теорема теории гТ. Тогда соотношение К' переносимо при Т.
В самом деле, такое же рассуждение, как и в критерии СТ7, показывает, что соотношения К!х, з1(фК'!х, з! н К!у з'1(=Ф (=~К' !у, з' ! являются теоремами теории ~„так как по предположению соотношение К)х, з~ффК!у, з'1 истинно в дю то же верно и для К'1х, з!ффК'~у, з'~. СТ10. Для типизации Т)х, з, А1 пусть Б — терм типа ф(8), г котором не встречается буква г. Для того чтобы О было переносимым термам при Т, необходимо и достаточно, чтобы соотношение гг~О было аереносимым ари Т.
Условие необходимо в силу СТ5, Обратно, если оно выполняется, соотношение (гт~О ! х,, ..., х„, г,, ..., гг Р э~+и ..., гр!)~ (=)(1'(г1)ЕО!у, у„г,' г~, г',, гр'!) истинно в ~,. Так как в теории г7', отображение $ т биективно, из этого вытекает, что соотношение (1)у, з'1= 1 ! (О ! х, з 1) есть теорема теории К,, что и устанавливает критерий. СТ11. При типизации Т! х, з, А! пусть Π— терм типа Зр г котором не встречается буква г.. Для того чтоби О била переносимым при Т, необходимо и достаточно, чтобы соотношение г.= Б было переносимым при Т.
Рассуждение совершенно аналогично рассуждению критерия СТ!0, и мы предоставляем читателю его проделать. СТ12. Пусть г — буква, отличная от констант теории сТ и букв, встречающихся е типизации Т(х, з, А1, и пусть О— терм типа 8 (соответственно ф(5)) для Т, е котором буква г не встречается. Три следующих условия экеигалентны: а) О есть переносимый терм типа 8 (соответственно ф($)) при Т; б) О есть переносимый терм типа 5 (соответственно ф(5)) при типизации „Т ! х, з, А ! н г Е5(х, А)'.
в) соотношение г = О (соответственно я ~О) переносимо при типизации „Т~х, з, А1 и я~8(х, А)". Эквивалентность б) и в) вытекает из СТ10 и СТ11 и а) влечет, очевидно, б). Кроме того, метод вспомогательной константы показывает, что б) влечет переносимость О при Т в теории, полученной добавлением к Т аксиомы Б(х, А) Ф И. Но если Π— типа 8, соотношение Т влечет по предполоягению (в,T) соотношение 0 ~3(х, А) н, следовательно, соотношение 8(х, А) ф И; таким образом, последнее соотношение есть теорема теории Т,, а это доказывает, что в этом случае 13 переносим при Т в теории Т. Если Π— типа ф(8), соотношение „Т(х, в, А! и 5(х, А)=И" влечет О=И в Т и тогда О переносим при Т в теории, полученной добавлением к,T аксиомы 5(х, А) = И, в силу СТ1; заключение получается теперь методом разделения случаев (гл.
1, $ 3, и' 3) 287 ПРИЛОЖЕНИЕ. КРИТЕРИИ ПЕРЕНОСИМОСТИ 286 ГЛ ПС СТРУКТУРЫ СТ13. Пусть К вЂ” соотношение, переносимое при типизации Т(х, в, А!. Для всякого индекса /(1 (/ р) терм „множество элементов г ~5/(х, А), таких, что К" (гл. 11, 8 1, п'6) есть переносимый терм типа 11г(5/) (при Т), В самом деле, если этот терм обозначить через (), ясно, что () — типа 1!з(5/) и что г в нем не встречается. но в,у' типизация т влечет соотношение (г/Е())(:Ф(г/Е5/(х, А) и К), и соотношение „г ~5/(х, А) и К" переноснмо прн Т (критерни СТ5, СТ6, СТЗ).
С помощью СТ9 и СТ10 получаем требуемое заключение. СТ14. Для типизации Т!х, з, А! пусть К вЂ” переносимое соотношение, () — переносимый терм типа 14г(5/). Тогда соотношения (!г/)(г/с() и К), (Чг/) ((г/ с ()) =)ь К) переносимы при Т. В самом деле, пусть Г есть терм „множество элементов г/~Я/(х, А), таких, что К". В су' соотношение Т влечет соотношение (() с=Г) фф((Чг/) ((г/ с ()) =)ь К) ). Так как, в силу СТ13, терм 1У есть переносимый терм типа ф(Я ) при Т, то второе утверждение критерия вытекает из СТ5 и СТ9; первое же получается с помощью СТЗ и СТ9.
СТ15. Для типизации Т!х, в, А! пусть () — переносимый терм типа 5, à — такой переносимый терм типа 14З(5/), г котором не встречается г.. Тогда терм „множество объектов вида П для г/~(У" (гл. 11, 8 1, п'6) есть переносимый терм типа ьйэ(5) при Т. В самом деле.
пусть г — буква, отличная от букв, введенных до сих пор. Рассматриваемый терм есть множество Ч элементов с~5(х. А), таких, что истинно (=)г) (г ~Г и «=()). Применяя последовательно СТ5, СТЗ н СТ13, видим, что Ч вЂ” переносимый терм типа ф(5) при типизации „Т1х, э, А ! и г ~ 5 (х, А)". С помощью СТ!2 получаем требуемое заключение.
СТ16. Пусть К вЂ” соотношение, переносимое при типизации Т. Если е д соотношение,Т и К" функционально по г/. то льерм т (Т и К) — переносимый терм типа 5/. »/ Пусть Ч вЂ” этот терм; он, очевидно, типа 5 . В д соотношение Т /' влечет (г/ — — Ч)фф(Т и К) и г/ не встречается в Ч; с помощью СТ9 и СТ11 получаем требуемое заключение. 2 Напротив, если не предполагать, что.Т и й' функционально по з., заключение критерия СТ!6 не верно.
Предположим, например, что,у'— теория множеств, что п=р=1, т=б в что Т к й — оба тождественны соотношению г, 6 х,. Еслн бы терм т (й) был переносимым прн Т, соотношение переноса влекло бы равенс~во //(ч, (г,6 х)) = т, (гч/,(х,)). Это влекло бы затем, что для всякого множества Е образом элемента т»(хЕ6) при всякой бнекцни множества Е на множество р является элемент т» (хбр), что абсурдно, так как существуют множества, имеющие два элемента. СТ!7. Пусть К вЂ” переносимое соотношение, () — переносимый терм типа 5/, à — переносимый терм типа 5'. Тогда соотношение (()!г/)К переносимо, а терм (()!г )Г есть переносимый терм типа 55 В самом деле, пусть Ч вЂ” множество элементов г ~ 5 (х, А), таких, что К; Ч вЂ” переносимый терм (СТ13), и соотношение Т влечет (в Д') соотношение ((() ! г/) К) фф(() с Ч) Следовательно, (()!г/) К переносимо (СТ9).
Пусть г — буква, отличная от букв, введенных до сих пор; соотношение г = (() !г/) Г тождественно соотношению (() !з/) (г = 1У) и г = Г переносимо при типизации „Т)х, з, А1 и г Е 5'(х, А)"; таким образом, в силу предыдущего, соотношение г =(()!г ) Г переносимо прн этой типизации.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
