полнота логических исчислений
полнота логических исчислений
ПОЛНОТА ЛОГИЧЕСКИХ ИСЧИСЛЕНИЙ — выводимость в исчислении (логической системе) всех утверждений (предложений, формуЛит.п.), обладающих некоторым подразумеваемым для этого исчисления свойством. Напр., П. классического исчисления высказываний (в какой-нибудь из возможных формулировок) означает выводимость в нем всех тождественно истинных формул логики высказываний. Часто под П. исчисления понимают ее адекватность, т.е. не только справедливость П., но и корректность (soundness), непротиворечивость относительно подразумеваемого свойства: все выводимые утверждения обладают нужным свойством (напр.: все выводимые в классическом исчислении высказываний формулы тождественно истинны). Семантическая П. — П. относительно свойства истинности в модели или классе моделей. Теорема Геделя о П. утверждает, что всякая теория первого порядка (в том числе и логика предикатов, как теория с пустым множеством специальных аксиом) полна: формула этой теории выводима тогда и только тогда, когда эта формула истинна в любой модели, в которой истинны аксиомы этой теории. Напр., множество формул, выводимых в первопорядковой теории групп, совпадает с множеством формул, истинных во всех группах. Аналогичные утверждения справедливы и для иных логических языков; напр., для языка тождеств (формул вида t = s, где t и 5 — термы, выражения), квазитождеств (формул вида fj = Sj &...& tn = sn -> f J = sn+1) и др. Такого рода теоремы о П. позволяют заменить неэффективные понятия истинности понятиями выводимости, имеющими алгоритмическую природу, что используется в автоматическом доказательстве теорем, когда проблема истинности заменяется эквивалентной проблемой выводимости, при создании логических языков программирования (Пролог и т.п.). Проблема семантической П. логических систем (исчислений) имеет различные варианты: а) поиск логической системы (в частности, обладающей некоторыми требуемыми свойствами, напр. наличием конечной аксиоматики), полной относительно данного класса моделей (относительно данной модели); б) поиск класса моделей (модели), относительно которого полным является данное исчисление. При положительном решении этих проблем решается и проблема поиска доказательства П. данной логической системы относительно данного класса моделей. Теорема Геделя о П. решает один из вариантов последней проблемы. Примеры проблем, а). Множество натуральных чисел N с обычными арифметическими операциями сложения и умножения, предикатом равенства и константами 0,1 называют стандартной моделью арифметики. Первая теорема Геделя о неполноте (в упрощенной формулировке) утверждает, что не существует эффективной, т.е. обладающей разрешимым множеством аксиом и правил вывода, теории (логического исчисления), множество выводимых утверждений которой совпадает с теорией натуральных чисел первого порядка. С другой стороны, если исключить из рассмотрения умножение, то получившаяся теория, называемая арифметикой Пресбургера, обладает аксиоматической системой с конечным списком аксиом, т.е. существует эффективная логическая система (также называемая арифметикой Пресбургера), полная относительно модели из натуральных чисел с константами 0,1, функцией (операцией) сложения и предикатом равенства. Теорема Трахтенброта утверждает, что не существует эффективного логического исчисления, полного относительно класса всех конечных моделей (стандартная формулировка — первопорядковая теория конечных моделей не является рекурсивно перечислимой). Примеры проблем, б). Парадоксы наивной теории множеств привели к созданию различных аксиоматических теорий множеств. В отличие от аксиоматической арифметики, называемой формальной арифметикой, теория множеств не обладает стандартной, т.е. всеми принимаемой в качестве стандартной, моделью. Положение усугубляется тем, что имеются многочисленные утверждения, такие как континуум-гипотеза, аксиома выбора, которые равнонепротиворечивы со своими отрицаниями; напр., мы можем к аксиоматической теории множеств присоединять континуум-гипотезу (упрощенная формулировка: в каждом бесконечном множестве действительных чисел элементов либо столько же, сколько натуральных чисел, либо столько же, сколько всех действительных чисел) и можем присоединять ее отрицание: если одна из получившихся теорий непротиворечива, то непротиворечива и другая. По аналогии с логическими исчислениями первого порядка строятся исчисления второго (или даже более высокого) порядка. Доказано, что эти исчисления не обладают свойством П. относительно класса моделей формул их языка. Однако удается доказать П. относительно видоизмененных моделей (относительно главных интерпретаций). Другими примерами являются различные неклассические логики. Так, модальные и релевантные исчисления возникли изначально как аксиоматические и лишь десятилетия спустя для них были предложены теории моделей, относительно которых они полны, и рассматриваемые модели обладают эвристической ценностью, позволяя учитывать интуицию, подразумевавшуюся при построении исчислений. Синтаксическая П. — П. логического исчисления относительно определенного формульного свойства. Так, арифметика Пресбургера обладает кроме семантической также и синтаксической П.: для всякого предложения (замкнутой формулы) А ее языка справедливо, что одна из формул А или —А выводима в арифметике Пресбургера. Из теоремы Геделя о П. и/или из ее доказательств следует, что всякая непротиворечивая теория первого порядка имеет синтаксически полное непротиворечивое расширение. Синтаксическая П. иногда полезна для доказательства разрешимости теории: если теория задана эффективно (рекурсивно или алгоритмически аксиоматизируема) и синтаксически полна, то она разрешима. Этот вид можно переформулировать и для случая логических языков, не содержащих отрицания. Близким к нему видом П. является П. по Посту, применяющаяся чаще всего для пропозициональных логик, в которых действует правило подстановки формул вместо переменных: логика называется полной по Посту, если она непротиворечива, но всякое ее собственное расширение, т.е. содержащее хотя бы одну новую формулу, противоречиво. Так, классическое исчисление высказываний полно по Посту. К синтаксической П. относятся и различные свойства эффективности связок. Напр., говорят, что логическое исчисление обладает свойством дизъюнкции (дизъюнктивным свойством), если из того, что в нем выводима формула AvB, следует, что выводима формула А или выводима формула В. Свойством дизъюнкции не обладает классическое исчисление высказываний (формула р v —,р в нем выводима, но не выводимы нир, ни —р), но обладает интуиционистское исчисление высказываний. Кванторным вариантом свойства дизъюнкции является экзистенциальное свойство: если в данной логической системе выводимо предложение З л х р ( х ), то выводимо и предложение вида с р ( ? ), где t — некоторый не содержащий переменных терм. Последнее свойство используется в приложениях: если доказано существование некоторого объекта, обладающего требуемым свойством, т.е. и способ построения этого объекта. Экзистенциальным свойством обладают многие теории, построенные на интуиционистской (конструктивной) основе. Классическое исчисление высказываний обладает ослабленным свойством дизъюнкции — П. (или разумностью) по Холдену: если выводима AvB, где А и В не имеют общих переменных, то выводима по крайней мере одна из формул А или В. Этим свойством не обладают практически все стандартные модальные логики, но многие из них обладают модальным свойством дизъюнкции: если выводима AvB, то выводима, по крайней мере, одна из формул А или В. А.В. Чагров Лит.: Кпини С.К. Введение в метаматематику. М., 1957; Черч А. Введение в математическую логику. М., 1960; Булос Дж., Джеффри Р. Вычислимость и логика. М., 1994.