Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 49

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 49)

Отсюда мы сделали заключение, что построение какой-либо системы вычислимых арифметических функций ср„..., фб, для которой можно доказать, что всякая цифра р обладает свойством )к)(р, сры ..., срб), вместе с тем доказывает, что формула 5 неопровержима. Это н составляет содержание критерия !'. Но !) Сы. с. 217. В Д. Гальберт, П. Бернайс критеРИи ОПРОВеРжимости $4! е-СИМВОЛ И ЛОГИЧЕСКИП ФОРМАЛИЗМ (гл ги из него, если дано некоторсе опровержение формулы 5, можно лишь заключить, что невозможно найти такую сиетему вычислимых функций ф,, ..., ф,, для которой удастся доказать, что для всех цифр р имеет место отношение 1А4(р, (р,, ..., (р ); или, другими словами, что какую бы систему вычислимых функций фт, ..., (р мы ни взяли, нельзя будет доказать, что для всех цифр р имеет место отношение ) Я)1р, (р„..., (р,).

Но это еще не говорит о том, что для любой системы вычислимых функций ф„..., (р, можно найти какую-либо цифру р, для которой имеет место отношение Ае)р, (р„..., р,) Аналогичным образом обстоит дело и с критериями 2 и 2*, а также с критериями 3 и 3». Таким образом, с финитной точки зрения критерии опровержимости 1 — 3 сильнее, чем критерии неопровержимости 1* — 3*, получающиеся из них путем неформального применения контра- позиции.

Следует также заметить, что все эти критерии, относящиеся непосредственно лишь к формулам рассмотренного нами специального вида Уй .. УЗД))т " =1))46(ЕЛ " ))в), где ь„..., ~„вт, ..., ))в — полный список индивидных переменных, а т и В Отличны от нуля, могут быть также применены и к исследованию опровержимости (соответственно неопровержимости) произвольных формул исчисления предикатов. Действительно, пусть (в — какая-либо формула исчисления предикатов.

Тогда для формулы ) 6 можно построить некоторую дедуктивно равную ей сколемовскую нормальную форму, причем эту форму можно выбрать так, чтобы она не содержала свободных индивидных переменных. Тогда отрицание этой формулы будет переводимо в некоторую формулу 5 вида чйл ... ~3„ЪЛ ... -)(ЪЕ(Х„..., Рв), где Г„..., е„))„..., ))е — полный список входящих в нее индивидных переменных, Так как формула ) (в дедуктивно равна формуле )5, то по опровержению 6 можно будет получить опровержение $, и наоборот; таким образом, исследование неопровер.

жимости формулы (Х равносильно исследованию неопровержимости 5. Если в кванторной приставке этой формулы имеются только кванторы всеобщности или только кванторы существования, то вопрос о том, является эта формула опровержимой или нет, можно разрешить элементарным образом'). Если же в кван- т) См. уже цитировавшееся недавно место т.

1, с, 239 — 243, торной приставке имеются и кванторы всеобщности, и кванторы существования, то можно воспользоваться только что сформулированными критериями неопровержимости. Но можно и прямо получить обобщения критериев 1 — 3 на случай произвольных предваренных формул исчисления предикатов, а также на случай формул, являющихся конъюнкциями предваренных. Первым шагом на пути к этому обобщению является допущение в формуле 5 свободных индивидных переменных. Модификация этих критериев на случай, когда в формуле 5 содержатся свободные переменные, заключается в том, что свободные переменные этой формулы надо будет заменить отличными друг от друга цифрами и что, кроме того, в критерии 3 к условию, требующему, чтобы система функций ф„..., фв была разделяющей, надо будет добавить еще одно условие, требующее, чтобы значения этих функций были отличны от цифр, подставленных вместо свободных переменных формулы 6.

Обоснование этих модифицированных критериев вытекает из того простого факта, что формула цт, получающаяся из какой- либо формулы 6 исчисления предикатов при замене свободных индивидных переменных какими-либо отличными друг от друга цифрами, выводима средствами исчисления предикатов тогда и только тогда, когда то же самое можно сказать относительно самой формулы 6. В остальном доказательство протекает совершенно так же, как и раньше; только теперь в дизъюнкцин') Лл. (1(1) 1(1) (111) 1(!)) ф (1(1) 1()))) 14 ... Л,) ЛЛ(11в)), „11м), ф,1'11м), ..., 11м)), ..., ф,~11м), ..., 11м))) термы 1(и ...

1'. ) ... 11"') ... 11(в) сами могут быть цифрами или же могут содержать их, и, в соответствии с этим, переход к дизъюнкции Ь должен быть видоизменен так, чтобы цифрой О заменялись только те из термов 1(), ..., 1( ), ..., 11в'), ..., 1(м), которые еще не являются цифрами и не совпадают ни с каким из термов ф,(111), ..., 111)) 11 1, ..., 6; )=1, ..., Вл). добавление упомянутого выше условия, налагаемого на систему функций ф„ ..., фв, необходимо для того, чтобы сохранялась возможность вывода формулы (х из дизъюнкции царе~ в).

') См. с. 2!3. е) бм. с. 2!5 — 2!7, 8* 229 «-СИМВОЛ И ЛОГИЧЕСКИИ ЬОРМЛЛИЗМ !гл, ги КРИТЕРИИ ОПРОВЕРЖИМОСТИ «4! С точки зрения исследования опровержимости рассмотрение формул со свободными переменными равносильно рассмотрению формул, начинающихся кванторами существования. Действительно, ведь опровержимость какой-либо формулы исчисления предикатов 6(а„..., а!), где а„..., а! — полный список входящих в нее свободных инди- видных переменных, означает выводнмость формулы )Е(а,, ..., а!).

Но эта формула дедуктивно равна формуле ~!4у, "!Уу! )Е(ГИ " Г!), получающейся из нее в результате замены свободных переменных связанными. Тем самым опровержимость формулы 8(а, ..., а!) равносильна опровержимости формулы Зу, "ЛугВ(ум ", у!). Таким образом, мы всегда можем избежать вхождений свободных индивидных переменных в формулы, опровержимостью которых мы будем интересоваться, если вместо формул со свободными переменными рассматривать формулы, начинающиеся кванторами существования. И наоборот, для применения этих критериев мы будем устранять кванторы существования, заменяя связанные переменные свободными; эти свободные переменные надо будет заменить затем цифрами.

Обычно цифры берутся подряд, начиная с 0 или с 1. А теперь мы укажем обобщение критериев 1 — 3 на случай произвольных предваренных формул 5 без свободных индивндных переменных. Для этого нет необходимости формулировать эти критерии заново, так как вносимые при этом изменения будут незначительными; они заключаются в следующем: 1, Сопоставление функциональных знаков йм ..., 49 =1-переменным формулы 5 в критериях 1 и 3 мы теперь возьмем таким, чтобы каждой Л-переменной 9!, которой предшествует хотя бы одна 4«-переменная, снова соответствовал некоторый функциональный знак 42!, однако только в качестве аргументов мы будем брать те цифры и, р ..., п„), которые стоят на местах каких- либо У-переменных формулы 5, предшествующих переменной ро Аналогичным образом в критерии 2 при выборе цифр 1! Р которые в различных, подлежащих совместному выполнению выра- кениях фигурируют вместо переменной 9! формулы 5, необходимо следить за тем, чтобы в том случае, когда два набора и...

и !'! '''Ф «! и и,,, и, 1* совпадают относительно цифр, стоящих на местах каких-либо 4г-переменных, предшеспюующих в формуле 5 переменной 4!ь совпадали также и цифры 1; 1 и 1! 1.. 2. Если формула 5 содержит такие п-переменные, которым не предшествует ни одна ч-переменная, то в подлежащих совместному выполнению выражениях следует подставлять вместо этих переменных какие-либо отличные друг от друга цифры. В этом случае на функции 4ри ..., Ч должно быть наложено дополнительное условие, требующее, чтсбы все значения этих функций отличались от этих цифр, берущихся для замены Л-переменных без предшествующих нм !»-переменных.

Замечание. В формулировке этих критериев можно избежать особого положения, занимаемого Л-переменными без предшествующих им !«-переменных, разрешив иметь среди функциональных знаков 4р,, ..., 494 знаки без аргументов, соответствующие 3-переменным без предшествующих им т-переменных. Их значения суть цифры, которые надлежит подставлять вместо соответствующих им Л-переменных. В этом случае в критерии 3 не надо будет налагать никаких дополнительных ограничений на фигурирующую там разделяющую систему функций. Указанных модификаций достаточно и для того случая, когда формула 5 представляет собой конъюнкцию предваренных формул.

В этом случае надо только под «предшествованием» какой-либо !«-переменной соответствующей 1-переменной всякий раз понимать предшествование в том конъюнктивном члене, в который входит эта 1-переменная. При этом связанные переменные, фигурирующие в различных членах конъюнкции, следует рассматривать как различные, даже в том случае, если они имеют одинаковые обозначения.

Чтобы проиллюстрировать эти модификации наших критериев, мы рассмотрим случай формулы 5, имеющей вид 7х3у=1г!гиЛо21 (х, у, г, и, о) Й ЛхЗУЧга (х у г). В этом случае наши критерии формулируются следукяцим абра зом. (Во всех приводимых ниже предложениях 1, 2 и 3 под и, 1, п,,), п,,) следует понимать тройку цифр с номером ! в нумерации троек по величине наибольшей цифры, а при равных наибольших цифрах — в лексикографическом порядке.) 1. Если формула 5 опровержима, то для всякой пара цифр 14, 4, и для всякой тройки вычислимых арифметических функций р„!Р„<р» на основе опровержения формулы 5 можно найти такую 23! ЕЗО З-СИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ 1гл и! ПРИМЕИГИИЕ К ПРОБЛЕМЕ РАЗРЕШИМОСТИ 4 51 цифру р, для которой формулы з!(Ез.! фз(пз.!) фз(пг,!) Е,г фз(пз.! и .!))е«6(1, 1, ез, ) 1=0, .", 0+ !)' — ! не являются совместно выполнимыми.

2. . Если формула й опровержима, то на основе ее опровер- жения для любой пары цифр )з, 1» и для любой свободно стано- вящейся последовательности троек цифр 1, 1, 1 с з ,;, связанных с тройками и,, п,,), и,, следугощими условиями: а) если пс! совпадает с пг,!», то 1ь совпадает с 1ь; ° и 1, совпадает с 1,, ° ', 5,1 г,) ° И б) если пь! совпадает с иь ! и и,,! совпадает с и... то 1,, совпадает с 15,, ,' з. з.

!'~ 5.1 можно построить такую цифру р, что формулы 2! (пь) 1ь ! 1».1 пз, ! 1з,1) ог 8()г !м пз. 1) 1=0 (Р+ !)з — 1 не являются совместно выполнимыми. 3. Е ели для некоторой цифры р, некоторой пары циф и некоторой тройки вычислимых арифметических фун Р м,з (ото н нкций ф„ гр, аз ел ( диого аргумента) и ф, (от двух аргументов) образу р д яющую систему функций, значения которых всегда отличны от цифр ~,, и )„формулы 'Д(пг,), фг(пг,!), фз(пз)!), и,, гр,(пьр п,,))658(!и г„пз, ) 1 = О, ..., (р+ 1)' — ! не являются совместно выполнимыми, то может быть построено опровержение формулы й в исчислении предикатов. Доказательство того, что сформулированные обобщения р ! — имеют место, не требует никаких новых идей.

Чита- кри- тель может без труда провести его сам, используя доказательство для рассмотренного частного случая и наше доказательство тео- ремы Эрбрана') $ б. Применение полученных критериев к проблеме разрешимости а) Общие сведения о выполнимости. Теоретико-модельная сколемоаская нормальная форма. Полученные нами критерии опровержимости дают формулировку теоремы Эрбрана для чистого исчисления предикатов, основанную на содержательном истолковании формул этого исчисления. з) См., в частности, с. 190 — 199. Эта формулировка особенно приспособлена для применений теоремы Эрбраиа к проблеме разрешимости. Рассмотрение этих применений дает нам повод вернуться к рассмотрению вопросов, связанных с выполнимостью и опровержимостью логических формул.

Характеристики

Список файлов книги