Логика предикатов

Понятие ``предикат'' обобщает понятие ``высказывание''. Неформально говоря, предикат – это высказывание, в которое можно подставлять аргументы. Если аргумент один – то предикат выражает свойство аргумента, если больше – то отношение между аргументами.

Пример предикатов. Возьмём высказывания: `` Сократ - человек '', `` Платон - человек ''. Оба эти высказывания выражают свойство ``быть человеком''. Таким образом, мы можем рассматривать предикат `` быть человеком '' и говорить, что он выполняется для Сократа и Платона .

Возьмём высказывание: `` расстояние от Иркутска до Москвы 5 тысяч километров ''. Вместо него мы можем записать предикат `` расстояние '' (означающий, что первый и второй аргумент этого предиката находятся на расстоянии, равном третьему аргументу) для аргументов `` Иркутск '', `` Москва '' и `` 5 тысяч километров ''.

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

Пример рассуждения, не выразимого в логике высказываний. Все люди смертны. Сократ - человек. Следовательно, Сократ смертен.

Это рассуждение на языке логики высказываний можно записать тремя отдельными высказываниями. Однако никакой связи между ними установить не удастся. На языке логики предикатов эти предложения можно выразить с помощью двух предикатов: `` быть человеком '' и `` быть смертным ''. Первое предложение устанавливает связь между этими предикатами.

Перейдём теперь к формальному изложению логики предикатов.

Язык логики предикатов

``Предикатные формулы'' обобщают понятие пропозициональной формулы, определённое в части 2 .

Предикатная сигнатура – это множество символов двух типов – объектные константы и предикатные константы – с неотрицательным целым числом, называемым арностью , назначенным каждой предикатной константе. Предикатную константу мы будем называть пропозициональной , если её арность равна 0. Пропозициональные константы являются аналогом атомов в логике высказываний. Предикатная константа унарна , если её арность равна 1, и бинарна , если её арность равна 2. Например, мы можем определить предикатную сигнатуру

{ a, P, Q } (4)

объявляя a объектной константой, P – унарной предикатной константой, и Q – бинарной предикатной константой.

Возьмём предикатную сигнатуру s , которая включает по крайней мере одну предикатную константу и не включает ни одного из следующих символов:

объектные переменные x, y, z, x 1 , y 1 , z 1 , x 2 , y 2 , z 2 , ...,
пропозициональные связки,
квантор всеобщности " и квантор существования $ ,
скобки и запятая.

Алфавит логики предикатов состоит из элементов из s и четырёх групп дополнительных символов, указанных выше. Строка – это конечная последовательность символов из этого алфавита.

Терм – это объектная константа или объектная переменная. Строка называется атомарной формулой , если она является пропозициональной константой или имеет вид R ( t 1 , ..., t _n ), где R – предикатная константа арности n ( n > 0) и t 1 , ... , t _n – термы. Например, если мы рассматриваем сигнатуру ( 4 ), то P ( a ) и Q ( a, x ) – атомарные формулы.

Множество X строк замкнуто относительно правил построения (для логики предикатов), если

каждая атомарная формула принадлежит X ,
для любой строки F если F принадлежит X , то ¬F тоже принадлежит,
для любых строк F, G и любой бинарной связки Д , если F и G принадлежат X , то также принадлежит ( F Д G ),
для любого квантора K , любой переменной v и любой строки F если F принадлежит X , то также принадлежит Kv F .

Строка F является (предикатной) формулой, если F принадлежит всем множествам, которые замкнуты относительно правил построения.

Например, если рассматриваемая сигнатура есть ( 4 ), тогда

( ¬P ( a ) Ъ $ x ( P ( x ) & Q ( x, y ))) – формула.

3.1 Является ли " x формулой?

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

В случае предикатных формул доказательство по структурной индукции имеет следующий вид. Для данного свойства формул мы проверяем, что

каждая атомарная формула обладает этим свойством,
для любой формулы F , обладающей этим свойством, ¬F также обладает этим свойством,
для любых формул F, G , обладающих этим свойством, и любой бинарной связки Д , ( F Д G ) также обладает этим свойством,
для любого квантора K , любой переменной v и любой формулы F , обладающей этим свойством, Kv F также обладает этим свойством.

Тогда это свойство выполняется для всех формул.

3.2 Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?

3.3 Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?

При записи предикатных формул мы будем опускать некоторые скобки и применять другие сокращения, введённые в части 2 . Строку вида

" v 1 ··· " v _n ( n і 0) будем писать как " v 1 ··· v _n , и подобным образом для квантора существования.

Свободные и связанные переменные

Множество свободных переменных ^* формулы F определяется рекурсивно, следующим образом:

Определение 22 (Свободные переменные).

Все переменные, входящие в атомарную формулу, являются свободными переменными этой формулы,
свободные переменные формулы F являются свободными переменными формулы ¬F ,
переменные, являющиеся свободными для хотя бы одной из формул F или G , являются свободными переменными формулы ( F Д G ),
все свободные переменные формулы F кроме v являются свободными переменными формулы Kv F .

Определение 23 (Замкнутая формула). Формула без свободных переменных называется замкнутой формулой , или предложением .

Определение 24 (Связаная переменная). Переменная v связана в формуле F , если F содержит вхождение Kv , где K – квантор.

3.4 Найдите свободные переменные и связанные переменные формулы

$ y P ( x, y ) & ¬ $ x P ( x, x )

Представление предложений русского языка предикатными формулами

Перед тем как мы продолжим изучение синтаксиса логики предикатов, полезно потренироваться в переводе предложений с русского языка в язык предикатных формул. ^*

В этих упражнениях для перевода рассматривается сигнатура ( 4 ). Мы предполагаем, что объектные переменные служат для обозначения натуральных чисел и интерпретируем сигнатуру следующим образом:

a представляет число 10,
P ( x ) выражает условие ``x является простым числом'',
Q ( x, y ) выражает условие ``x меньше чем y''.

В каждой из следующих задач представьте данное предложение русского языка предикатной формулой.

3.5 Все простые числа больше чем x.

Ответ: " y ( P ( y ) Й Q ( x, y )).

3.6 Существует простое число, которое меньше чем 10.

3.7 x равно 2 . см. Указания

3.8 x равно 11 . см. Указания

3.9 Существует бесконечно много простых чисел.

Подстановка

Определение 25 (Подстановка терма). Пусть F – формула и v – переменная. Результат подстановки терма t вместо v в F – формула, определённая рекурсивно следующим образом:

результат подстановки t вместо v в атомарную формулу F получается из F одновременной заменой всех вхождений v на t ,
если результат подстановки t вместо v в F есть F' тогда результат подстановки t вместо v в ¬F есть ¬F' ,
если результат подстановки t вместо v в F и G есть F' и G' тогда результат подстановки t вместо v в ( F Д G ) есть ( F' Д G' ),
если результат подстановки t вместо v в F есть F' и w – переменная, отличающаяся от v , тогда результат подстановки t вместо v в Kw F есть Kw F' ,
результат подстановки t вместо v в Kv F есть Kv F .

3.10 Найдите результат подстановки константы a вместо x в формулу из задачи 3.4 .

Когда мы намереваемся рассмотреть подстановки вместо переменной v в некоторую формулу, удобно обозначать эту формулу выражением F ( v ), и обозначать результат подстановки терма t вместо v в этой формуле через F ( t ) .

3.11 Если v не является свободной переменной F ( v ) , тогда F ( t ) равно F ( v ).

Пусть F ( x ) обозначает формулу

" y ( P ( y ) Й Q ( x, y )), предложенную выше как перевод условия ``все простые числа больше чем x '' (задача 3.5 ). Формула вида F ( t ), где t – терм, обыкновенно выражает то же условие применённое к значению t . Например, F ( a ) есть " y ( P ( y ) Й Q ( a, y )), что значит ``все простые числа больше чем 10'', F ( z 2 ) есть " y ( P ( y ) Й Q ( z 2 , y )), что значит ``все простые числа больше чем z 2 ''. Существует, однако, одно исключение. Формула F ( y ), то есть, " y ( P ( y ) Й Q ( y, y )), выражает (неправильное) утверждение ``каждое простое число меньше чем оно само''. Проблема с этой подстановкой в том, что, когда мы подставляем переменную y вместо x в F ( x ), y ``захватывается'' квантором. Чтобы выразить утверждение ``все простые числа больше чем y '' предикатной формулой, мы будем использовать связанную переменную отличную от y и писать, например, " z ( P ( z ) Й Q ( y, z ))

Чтобы различать ``плохие'' подстановки, как в последнем примере, от ``хороших'', мы определим, когда терм t является подстановочным для переменной v в формуле F . ^*

Если F – атомарная, тогда t является подстановочным для переменной v в F,
t является подстановочным для переменной v в ¬F тогда и только тогда, когда t является подстановочным для v в F,
t является подстановочным для v в ( F Д G ) тогда и только тогда, когда t является подстановочным для v и в F и в G,
t является подстановочным для v в Kw F тогда и только тогда, когда
1. t не содержит w и является подстановочным для v в F , или
2. v не является свободной переменной формулы Kw F .

3.12 Терм, не содержащий ни одной связанной переменной формулы F, является подстановочным в F для любой переменной.

Определение 26 (Универсальное замыкание). Универсальное замыкание формулы F – это предложение

" v 1 ··· v _n F, где v 1 , ... , v _n – все свободные переменные F .

Выводы в логике предикатов

В логике предикатов вывод определяется так же, как и в исчислении высказываний и секвенции имеют тот же синтаксис. Аксиомы тоже определяются так же, как в логике высказываний. Все правила вывода логики высказываний – правила введения и удаления для пропозициональных связок, правила противоречия и сведения к противоречию – включены в множество правил вывода логики предикатов, с метапеременными для формул понимаемыми теперь как предикатные формулы. В дополнение, есть четыре новых правил вывода: правила введения и удаления для кванторов.

Правила для кванторов всеобщности

G |– F ( v )
(В " )

G |– " v F ( v )

G |– " v F ( v )
(У " )

G |– F ( t )

где v не является свободной где t является
переменной для любой формулы в G подстановочным для v в F(v)

В каждой из следующих задач выведите данную формулу из пустого множества посылок.

3.19 ( P ( a ) & " x ( P ( x ) Й Q ( x ))) Й Q ( a ).

3.20 " xy P ( x, y ) Й " x P ( x, x ).

Правила для кванторов существования

G |– F ( t )
(В $ )

G |– $ v F ( v )

G |– $ v F ( v ) G И { F ( v ) }|– C
(У $ )

G |– C

где t – подстановочный где для C и любой формулы из G
для v в F(v) v не является свободной переменной

В каждой из следующих задач выведите данную формулу из пустого множества посылок.

3.21 ( P ( a ) Ъ P ( b )) Й $ x P ( x ).

3.22 ¬ $ x P ( x ) є " x ¬P ( x ).

Корректность и полнота логики предикатов

Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.

Теорема корректности. Если существует вывод замкнутой формулы F из множества формул G , тогда G влечёт F.

Теорема полноты. Для любой замкнутой формулы F и любого множества предложений G , если G влечёт F, то существует вывод F из некоторого подмножества G .

Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.

Функциональные символы и равенство: синтаксис

Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется ``логикой первого порядка'', и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, ``функциональных констант''. Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.

Наше наиболее общее понятие сигнатуры определяется следующим образом.

Определение 28 (Сигнатура,константы). Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью , связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна , если её арность равна 1, и бинарна , если её арность равна 2. Пропозициональная константы , так же как унарные и бинарные предикатные константы, определены как выше.

Определение 29 (Терм). Возьмём сигнатуру s , не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов , если

каждая объектная константа принадлежит X ,
каждая объектная переменная принадлежит X ,
для каждой функциональной константы h арности n ( n > 0) и любой строки t 1 , ... , t _n , если t 1 , ... , t _n принадлежит X , тогда также принадлежит h ( t 1 , ... , t _n ).

Строка является термом , если она принадлежит все множествам, которые замкнуты относительно правил построения. ^*

3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?

В логике первого порядка существуют три типа атомарных формул :

пропозициональные константы,
строки вида R ( t 1 , ... , t _n ) где R – предикатная константа арности n ( n > 0) и t 1 , ..., t _n – термы,
строки вида ( t 1 = t 2 ), где t 1 , t 2 – термы.

Взяв в качестве множества атомарных формул данное множество, мы получаем, что определение формул (первого порядка) совпадает с определением предикатных формул в начале этой части.

Для любых термов t 1 и t 2 , t 1 № t 2 обозначает формулу ¬ ( t 1 = t 2 ).

Выводы в логике первого порядка

Определение вывода в логике предикатов с функциональными константами и равенством включает новый тип аксиом и два новых правила вывода. Правила, как и раньше, содержат метапеременные, служащие для обозначения формул и термов.

Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:

G |– t 1 = t 2 G |– F ( t 1 )
(З=)

G |– F ( t 2 )

G |– t 1 = t 2 G |– F ( t 2 )

G |– F ( t 1 )

где t 1 и t 2 свободные для v в F ( v ). ^*

Для каждой из следующих формул найдите вывод из пустого множества посылок.

3.27 x = y Й f ( x, y ) = f ( y, x ).

3.28 " x $ y ( y = f ( x )).

3.29 $ y ( x = y & y = z ) Й x = z.

3.30 $ x ( x = a & P ( x )) є P ( a ).

Теории первого порядка

Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G , называется моделью G . Если теория первого порядка G выполнима, мы также говорим что она непротиворечива . Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G .

Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G , тогда F является теоремой G . В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G , существует доказательство F в G .

Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.

Арифметика первого порядка

Мы будем упрощать запись формул сигнатуры арифметики первого порядка ( 6 ) введением следующего обозначения: a будет записываться как 0, s ( t ) как t' , f ( t 1 , t 2 ) как t 1 +t 2 , и g ( t 1 , t 2 ) как t 1 · t 2 . Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:

x' № 0.
x'= y' Й x = y.
( F (0) & " v ( F ( v ) Й F ( v' ))) Й " v F ( v ) для любой формулы F ( v ).
x + 0 = x.
x + y'= ( x + y ) '.
x · 0 = 0.
x · y'= x · y + x .

Интерпретация ( 7 ) является моделью этой теории. Арифметика первого порядка имеет также другие модели, и некоторые из них совсем не похожи на систему натуральных чисел (задача 3.40 ).

В следующих формулах 1 обозначает терм 0 ' , 2 – 0 '' , и 4 – 0 '''' . Через t 1 Ј t 2 мы обозначаем формулу $ v ( t 2 = t 1 + v ), где v – первая объектная переменная, которая не встречается в t 1 , t 2 .

В каждой из следующих задач найдите доказательство данной формулы в арифметике первого порядка.

3.34 2 № 4.

3.35 x' № x.

3.36 x'= x + 1.

3.37 x Ј x.

Нестандартные модели арифметики

Термы 0, 0 ', 0 '', ... называются цифрами . Модель M арифметики первого порядка стандартна , если для каждого c О |M| существует цифра t такая, что t ^M = c .

3.38 Модель арифметики первого порядка стандартна.

В соответствие с задачей 3.40 , существуют модели арифметики первого порядка, которые не обладают этим свойством. Чтобы доказать существование такой модели, полезно рассмотреть следующую теорию первого порядка G . Сигнатура G получается из сигнатуры арифметики первого порядка добавлением буквы b в качестве новой объектной константы. Множество аксиом G получается из множества аксиом арифметики первого порядка добавлением формул b № 0, b № 0 ', b № 0 '', ... в качестве новых аксиом.

3.39 G непротиворечива.

3.40 Арифметика первого порядка имеет нестандартную модель.

Существование нестандартных моделей арифметики следует из теоремы Сколема (1920), который обобщил раннюю работу Леопольда Лёвенхейма (1915). Возможность таких моделей резко контрастирует с результатом задачи 1.41 . Разница связана с тем, что язык арифметики первого порядка является слишком ограниченным для выражения аксиомы индукции. ``Арифметика второго порядка'', в которой схема индукции заменяется по аксиоме , не имеет нестандартных моделей.

Теорема неполноты Гёделя

Пусть M – нестандартная модель арифметики первого порядка. Может случится что M ``не отличима'' от модели в том смысле, что для любой замкнутой формулы F арифметики первого порядка F истинно при M тогда и только тогда, когда F истинно при . Но некоторые нестандартные модели не обладают этим свойством: может существовать предложение F такое, что при M предложение F истинно, а при ¬F истинно. Так как и M и интерпретация являются моделями арифметики первого порядка, значит ни F , ни ¬F не являются теоремами, а это означает, что арифметика первого порядка неполна. Этот факт, известный как теорема неполноты Гёделя, был доказан Куртом Гёделем в 1931 году.