• 5

48. Функциональное исчисление первого порядка с равенством.

Функциональное исчисление первого порядка с равенством есть логистическая система, полученная из функционального исчис­ления первого порядка добавлением бинарной-функциональной константы / и определенных аксиом (или постулатов, в зависи­мости от точки зрения), которые содержат I. Его можно описать и иначе, сказав, что оно получено добавлением дополнительных

аксиом к прикладному функциональному исчислению первого порядка, среди исходных символов которого имеется бинарная функциональная константа /. Пп-формулы полученной системы совпадают с пп-формулами первоначального прикладного функ­ционального исчисления первого порядка, но появляются, конеч­но, дополнительные теоремы, как следствие добавленных аксиом.

Мы будем говорить о чистом функциональном исчислении первого порядка с равенством, если в число элементарных символов входят все пропозициональные и функциональные переменные (перечисленные в § 30) и не входят никакие функциональные константы, помимо I; мы будем говорить о прикладном функцио­нальном исчислении первого порядка с равенством, если, кроме /, имеются другие функциональные константы; о притом приклад­ном функциональном исчислении первого порядка с равенством, если, кроме /, имеются другие функциональные константы, но нет функциональных переменных. Помимо этого, имеется простое исчисление равенства, получаемое добавлением соответствующих аксиом к простому прикладному функциональному исчислению первого порядка, единственной функциональной константой кото­рого является I.

Если функциональное исчисление первого порядка рассматри­вается в формулировке § 30, то должны быть добавлены следующие аксиомы: аксиома

1(х, х)

и бесконечный перечень аксиом, заданных аксиомной схемой

/(a, b)D,ADB,

где^а — индивидная переменная или индивидная .константа, b — индивидная переменная или индивидная константа, а В получено из А заменой на b некоторого частного вхождения а, которое не находится ни в области какого-либо квантора (а), ни в области какого-либо квантора (Ь). Формулировку функционального ис­числения первого порядка с равенством, которая получается добавлением функциональной константы I и вышеописанных аксиом к исчислению F1, мы будем называть F7. В частности, формулировка F/p чистого функционального исчисления первого порядка с равенством получается добавлением функциональной константы I и указанных аксиом к исчислению F1P.

Для простого исчисления равенства мы можем начать с фор­мулировки F1 простого прикладного функционального исчисления первого порядка, единственной функциональной константой кото­рого является I. К нему мы можем добавить аксиому 1(х, х) и все те аксиомы, которые задаются указанной выше аксиомной схемой, получая таким образом формулировку Ё простого исчис­ления равенства. Однако достаточно добавить лишь три следую-

щие аксиомы:

1(х, х).

1(х, у) 3 /(У, х).

(Закон рефлексивности равенства.) (Закон коммутативности равенства.)

1(х, у) 3. /(у, г) 3 I(x, z). (Закон транзитивности равенства.)

Полученную таким образом формулировку простого исчисления равенства мы называем Е.

Мы можем использовать для чистого функционального исчис­ления первого порядка также формулировку F£p из § 40. Добав­ляя к нему функциональную константу / и две аксиомы

мы получаем формулировку чистого функционального исчисления первого порядка с равенством, которую будем называть F|p.

Во всех этих исчислениях можно ввести более привычные, чем /, обозначения =: и ф с помощью следующих определений:

Разумеется, остаются в силе все определения и методы сокращения пп-формул, введенные для функционального исчисления первого порядка в § 30.

Подразумевается, что в главной интерпретации всех этих систем I долж­но обозначать отношение равенства или тождества между предметами.

Например, в случае чистого функционального исчисления первого порядка после того, как некоторый непустой класс выбран в качестве области индивидов, мы фиксируем главную интерпретацию с помощью тех же семан­тических правил а — f, что ив § 30, и двух следующих дополнительных правил:

Если а — индивидная переменная, то значением /(а, а) для всех зна­чений переменной а является t.

g2. Если а и Ь — различные индивидные переменные, то значением /(а, Ь) является t, если значение переменной а совпадает, со значением пере­менной Ь, и значением /(а, Ь) является f, если значение переменной а не совпадает со значением переменной Ь.

Синтаксическое определение общезначимости и выполнимо­сти (§ 43), так же как и метатеорема о том, что всякая теорема об­щезначима (**434), могут быть очевидным образом распространены на чистое функциональное исчисление с равенством, и мы будем предполагать, в особенности в некоторых следующих дальше упражнениях, что это сделано.

1(х, х), I(x, y)D,F(x)DF(y),

D 18. [а = Ь] /(а, Ь). D 19. [a=fcb]->~ /(а, Ь).

Упражнения к § 48

48.0.   В формулировке Е простого исчисления равенства ком­мутативный и транзитивный законы равенства можно заменить законом Эвклида, который гласит, что „вещи, равные одной и той же вещи, равны между собой", и который следующим об­разом выражается в обозначениях системы:

1{х, z)l{y, z)z> 1{х, у).

Таким образом получается формулировка Ё простого исчисления равенства, в которой вместо трех дополнительных аксиом имеются только две. Покажите, что системы Е и Ё эквивалентны в том смысле, что их теоремы совпадают.

48.1.   Покажите для систем Е и Ё, что дополнительные аксиомы, содержащие I, независимы.

48.2.   Покажите, что две формулировки Ё и Е простого исчисле­ния равенства эквивалентны друг другу в том смысле, что их теоре­мы совпадают. (В доказательстве можно использовать неко­торые соображения из доказательства метатеоремы *340.)

48.3.   Покажите, что две формулировки FJp и F|p чистого функционального исчисления первого порядка с равенством эквивалентны друг другу в том смысле, что их теоремы совпадают. (Можно воспользоваться тем же самым методом, с помощью кото­рого была доказана эквивалентность систем F1P и F|p. Однако заметьте, что наличие дополнительных аксиом ставит некоторые новые вопросы в связи с правилом подстановки.)

48.4.   Покажите, что для формулировки простого прикладного функционального исчисления первого порядка с равенством, число функциональных констант которого конечно, достаточно конечное число следующих аксиом: законы рефлексивности, ком­мутативности и транзитивности равенства; для каждой сингуляр­ной константы t одна аксиома

'(*> y)3.f(x)z>f(y);

для каждой бинарной функциональной константы f две аксиомы I(x, У)Э.!(х, z)Df(y, z), /(х, y)3.t(z, *)DI(2, у);

для каждой тернарной функциональной константы три аналогич­ных аксиомы; и т. д., пока аксиомы такого рода не будут введены для всех функциональных констант. (Опять исследуйте метод доказательства метатеоремы *340.)

18 2007 -

48.5.   Используя метод, аналогичный методу предыдущего упра­жнения, но применяемый не к функциональным константам, а к функциональным переменным, покажите, как для всякой пп-формулы А исчисления F7p найти соответствующую ей пп-фор- мулу А' исчисления Flp, которая общезначима тогда и только тогда, когда общезначима пп-формула А, и которая является теоремой исчисления F1P тогда и только тогда, когда А является теоремой исчисления F/p. Тем самым распространите теорему Гёделя о пол­ноте, **440, на чистое функциональное исчисление первого порядка с равенством.

48.6.   С помощью того же метода докажите следующее рас­пространение метатеоремы **450 на чистое функциональное исчисление первого порядка с равенством: если пп-формула исчисления F/p общезначима во всякой непустой области и обще­значима в некоторой счетно-бесконечной области, то она обще­значима во всякой непустой области.

48.7.   Найдите и докажите аналогичные распространения мета­теорем **453 и **455 на чистое функциональное исчисление пер­вого порядка с равенством.

48.8.   Докажите непротиворечивость исчисления Fx, используя, как в § 32, пфпи пп-формул.

48.9.   Распространите метатеорему **323 на исчисление FJ.

48.10. Распространите метатеорему **325 на исчисление F7.

48.11. Распространите принципы дуальности *372—*374 на исчисление F1. (Пп-формулы исчисления FJ .следует переписать с помощью D18 и D19 таким образом, чтобы символ I не встре­чался в них явно. Затем, при дуализации, знаки = и 4= должны взаимно заменяться, так же как и знаки 3 и дизъюнкция и конъюнкция, = и С и Jd, у и |, V и 3.)

48.12. Используя найденное в упражнении 48.5 сведёние, решите проблему разрешения для случая пп-формул исчисления FJp, имеющих такую предваренную нормальную форму, в префиксе которой ни один квантор существования не предшествует никакому квантору общности. (Заметьте, что это охватывает, в частности, бескванторные формулы исчисления F7p.)

48.13. Решите проблему разрешения для бескванторных формул исчисления FJp непосредственно, используя метод, как можно более сходный с разрешающей процедурой истинностных таблиц, с помощью которой определяется, является ли бескванторная фор­мула исчисления Flp тавтологией. На этой основе дайте новое решение проблемы разрешения для частного случая из 48.12 в форме, как можно более близкой к *460—**463.

48.14. Решите проблему разрешения для сингулярного функцио­нального исчисления первого порядка с равенством, т. е. для класса тех пп-формул исчисления F/p, в которых встречаются только сингулярные функциональные переменные.

Указание. Следуя Бэману, мы можем добавить к шагам све­дения (а)—(g) упражнения 39.6 еще следующие шаги, (а) Замена пп-части (а)[а = Ь] на (а) (с) [а = с], если а и b — отличные друг от друга индивидные переменные, ас — первая в алфавитном порядке индивидная переменная, отличная от а и от Ь. (£) Замена пп-части (а)[а 4= Ь] на (а)[а 4= а], если а и b — отличные друг от друга индивидные переменные, (у) Замена пп-части (a) [а 4= Ьх 3

a =t= Ь2 з ш ... а 3= ЬЛ 3 а = Ь] на конъюнкцию А,,^ = b2 3 [bx = b, 3 Aft_1]...[b« = b3At_1][b1 = ba3abi = b33 A„_a] [bx = bg3. bx = b4 3 An..s] . . . [b„._2 = b 3. bn_x = b„3 A,_2] [b,^! = b„3. b„_! = b3 A„_2]... [bx s= b23. bx =s b3 3.

... bx = b 3 A0], если a, b1( b2, .. ., b„, b — отличные друг от друга индивидные переменные, с1( с2, ..., с„, с — первые в алфавитном порядке п 4- 1 индивидных переменных, отличных как друг от друга, так и от переменных a, bx, Ь2,..b„, b, a Ai есть

(•)(с1)(ея)-(<Ч)(с).а*с1э.в*с|э.. . а=Цс{3. сх=Цс23. сх1|=сз3.... cx=t:ci3. ^ЦгсЗ. с2=Цс33.  с(фсэа = с

(i = 0, 1,2,..., п). (й) Замена пп-части (а)[а = а 3 А] на (а)А. (£) Замена пп-части (а)[а = b 3 А] на

S£ A j,

если а и b — отличные друг от друга индивидные переменные, а А не содержит кванторов. (£) Замена пп-части (а)[аЗ=аЗА] на (а) [а = а], (rj) Замена пп-части (а) [а ф Ьх 3. а Ь2 3. • • •

a=t= b„3 А] на конъюнкцию An[bx 3 A„_J [В2 3 А„_х]... [В,г3 А,^] Ьх = Ь„3 A„_1][b1 = b33 An_1]...[bn_1=b„3 А„_х] [Bj3. В23 К-Л [ВхЗ. вз з Ап_2] ... [В.,.! 3. в, з А„_3] [Ьг = Ь2 з. вз з An-J tbi = b2=>. В43 А„_2] ... [bn_! = b„ з. в„_2 з A„_2] [ba = b2 3. bj = b33 A„_,] [bx = b23. bx = b, з An_2] .. .

[bn-, = bn 3. bft_2 = bn_13An_2] [bn_2 sr bn_x 3. bn_2 = bn3 [A„_2] ... [B^. B2 3.... в„3 A0], если a, b1; b2,..., Ьд -

отличные друг от друга индивидные переменные, сг, с2, .. ., сп — первые в алфавитном порядке п индивидных переменных, отлич­ных как друг от друга, так и от переменных a, b,, Ь2, ..., bn, если 18* - 4

далее А не содержит ни кванторов, ни отличных от а индивидных переменных, если Bi и Ci суть соответственно

SbasA| и S*A| (i = 1, 2, ..., п) и если Aj есть

(а)(с,)(с1)...(е().а*с1э.а*с,э.... а*с43. с^с.,3. с^сз э.о • • ci_1=t=ci 3. ~ Сх 3. ~ С2 3.

(г = 0, 1, 2, ..., п) [таким образом, в частности, А0 есть (а)А].

48.15. Решите проблему разрешения для таких пп-формул А исчисления FJp, у которых в каждой элементарной части, не со­держащей /, не более чем одна переменная имеет вхождения, по которым она является связанной переменной пп-формулы А.

48.16. (1) Распространяя метод из упражнения 46.8, решите проблему разрешения для пп-формул исчисления FJp, имеющих предваренную нормальную форму (ЭЬ)(с)М, где М — основа, не * содержащая никаких индивидных переменных, кроме b и с. Проиллюстрируйте решение, применив его к следующим частным примерам:

(2)       (Эх)(у). F(x) 3 [F(y) Dx = y]D, F(x) = G(y) 3. F(y) = G(x)

(3)       (3x)(y). [F(x) = G(x)] v [F(y) = G(y) = x = у].

48.17. (1) Распространяя метод упражнения 46.11 (2), решите проблему разрешения для пп-формул исчисления Fip, имеющих предваренную нормальную форму (а)(ЭЬ)(с)М, где М — основа, не содержащая никаких индивидных переменных, кроме а, Ь, с. Проиллюстрируйте решение, применив его к следующим частным \ примерам:

(2)       (x)(3y)(z). F(x, х)3. F(x, 2)3x = yvy = 23. F(x, z) = F(x, y) = F(y, у) 3 . F(y, y) = F(z, z).

(3)       (x) (3y) (2). F(x). 3 G(x) 3. F(y) 3 [G(y) 3 x = y] 3. x * z 3. G(y) = F(z) 3. F(y) = G(z).

(4)       (x)(3y)(z).x*zvy*z.

48.18. Примените разрешающую процедуру из упражне­ния 48.14 к примеру 48.16 (2) и к примеру 48.17 (3).

48.19. (1) Решите проблему разрешения для пп-формул ис­числения F/p, имеющих предваренную нормальную форму (а1)(а2)(ЭЬ)(с)М, где М — основа, не содержащая никаких индивид­ных переменных, кроме а1} а2, Ь, с. Проиллюстрируйте решение, показав с помощью полученной разрешающей процедуры, что следующие пп-формулы являются теоремами исчисления FJp:

(2)       (хх) (х2) (Э у) (z). F(xv х2) 3. F(xv z) = F(y, у) 3.

2)3% у)]3.

F(xlf у) V F(x„ z) 3 F(x2, x2).

(3)       (Xj) (x2) (3y) (2). F(xj) 3. F(x2) 3. G(xx) 3. 0(x2) 3.

x, ф у 3 [F(z) 3 G(z)] 3. H(xx) 3 H(x2) 3 [G(y) 3 F(y)] 3.

G(y) = F(z)3.F(y) = G(z).

48.20. Примените разрешающую процедуру из упражне­ния 48.15 к примеру 48.19 (2).

48.21. (1) Сформулируйте и решите частный случай проблемы разрешения исчисления FJp, аналогичный случаю V' проблемы разрешения исчисления Flp. (Ср. 46.15.) (2) Проиллюстрируйте решение, применив его к следующему конкретному примеру:

(ЭХ) (ЗУ) (z). ~ F(x, х) v F(x, z) у F(y, z) v [х = 2 = . F(x, x) = F(z, z)] v . у = z = .F(y, y) = F(z, z).

48.22. Докажите следующую метатеорему. Пусть Г есть (ко­нечный или бесконечный) класс пп-формул исчисления FJp. Пусть а1; а2, а„ ... — полный перечень свободных индивидных переменных, встречающихся в пп-формулах из Г. Пусть р1( р2, р„ ... — полный перечень встречающихся пропозициональных переменных, fx, f2, f3, ... — полный перечень встречающихся функциональных переменных (разумеется, некоторые или даже все эти перечни могут быть бесконечны), и предположим, что fi есть hi-арная функциональная переменная (г = 1, 2, 3, ...). Пред­положим, далее, что класс Г совместно выполнен в области поло­жительных целых чисел системой значений vlt v2, v3, ..т1( т2, т3, ..Фъ Ф2, Ф3, ... переменных alf а2, а3, ..., рх, р2, р3, ..!lf f2, f3, ... . Тогда в области целых чисел (т. е. положительных це­лых, отрицательных целых и 0) существуют такие пропозицио­нальные функции W2, W3, ..., что Wi является Лгарной про­позициональной функцией целых чисел (t = 1, 2,3,...), для произ­вольных положительных целых чисел uv и2, .. ., щ, истинност­ное значение Wi(ult и2, . .., uhi) совпадает с истинностным значе­нием Фг(иъ и2, ..., и^) и класс Г совместно выполнен в области целых чисел системой значений v2, . •., т2, т3, ..

Ух,

W2, ..., переменных ах, а2, а3, ..рх, р2, р3,..tx, f2,

f           451)

1„ . . .

Указание. Без потери общности мы можем предположить, что переменными alf а2, а3,..., если таковые вообще имеются, являются переменные zx, z2, z3, ... . Добавим к классу Г все пп-формулы Xj =t= xk, в которых / и к — отличные друг от друга положительные целые числа, все пп-формулы

ft(Xu,, Хщ, . . ., Хщ4),

для которых Фг(щ, щ, ..., uhl) есть истина, а также все ип-фор- мулы

для которых Ф (цъ щ, ..., uhi) есть ложь. Обозначим полученный таким способом класс пп-формул через Г', и пусть класс Г" полу­чается из класса Г' присоединением всех пп-формул у, 4= xk, где / и к — произвольные положительные целые числа, и всех пп-формул у,- ф У к, где / и к — отличные друг от друга положитель­ные целые числа. Покажите, что класс Г' непротиворечив, и отсю­да — что непротиворечив каждый конечный подкласс класса Г". Затем покажите с помощью результата из упражнения 48.7, что Г" совместно выполним в счетно-бесконечной области Индивиды области 3> которые служат значениями для хх, х2, х3, ..., могут быть отождествлены с положительными целыми числами 1, 2, 3,. .. соответственно. Помимо них, область 3 необходимо содержит еще бесконечно много других индивидов, которые могут быть произ­вольным образом отождествлены с неположительными целыми числами 0, —I, —2, ....

48.23. Докажите следующую метатеорему как следствие пре­дыдущей. Пусть Г — (конечный или бесконечный) класс пп-формул исчисления FJp, и пусть одной из функциональных переменных, встречающихся в пп-формулах из Г, является бинарная функцио­нальная переменная s. Предположим, что класс Г совместно вы­полним в области положительных целых чисел таким образом, чтобы значением переменной s было отношение непосредственного следования, т. е. такое отношение а, что а(и, v) есть истина тогда и только тогда, когда и + 1 = v. Тогда класс Г таким образом сов­местно выполним в некоторой счетно-бесконечной области % с Ф в качестве значения переменной s, что не существует взаимно однозначного отображения области $ в положительные целые числа, при котором отношение Ф переходило бы в отношение а 452).

48.24. Докажите, что если класс пп-формул исчисления FIp совместно выполним в какой-либо конечной области, но не явля­ется совместно выполнимым в некоторой счетно-бесконечной об­ласти, то существует наибольшая конечная область, в которой этот класс совместно выполним.

Авторы: 1379 А Б В Г Д Е З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Э Ю Я

Книги: 1908 А Б В Г Д Е З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Э Ю Я