Логика предикатов
Понятие ``предикат'' обобщает понятие ``высказывание''. Неформально говоря, предикат – это высказывание, в которое можно подставлять аргументы. Если аргумент один – то предикат выражает свойство аргумента, если больше – то отношение между аргументами.
Пример предикатов. Возьмём высказывания: ``Сократ - человек'', ``Платон - человек''. Оба эти высказывания выражают свойство ``быть человеком''. Таким образом, мы можем рассматривать предикат ``быть человеком'' и говорить, что он выполняется для Сократа и Платона.
Возьмём высказывание: ``расстояние от Иркутска до Москвы 5 тысяч километров''. Вместо него мы можем записать предикат ``расстояние'' (означающий, что первый и второй аргумент этого предиката находятся на расстоянии, равном третьему аргументу) для аргументов ``Иркутск'', ``Москва'' и ``5 тысяч километров''.
Язык логики высказываний не вполне подходит для выражения логических рассуждений, проводимых людьми, более удобен для этого язык логики предикатов.
Пример рассуждения, не выразимого в логике высказываний. Все люди смертны. Сократ - человек. Следовательно, Сократ смертен.
Это рассуждение на языке логики высказываний можно записать тремя отдельными высказываниями. Однако никакой связи между ними установить не удастся. На языке логики предикатов эти предложения можно выразить с помощью двух предикатов: ``быть человеком'' и ``быть смертным''. Первое предложение устанавливает связь между этими предикатами.
Перейдём теперь к формальному изложению логики предикатов.
Язык логики предикатов
``Предикатные формулы'' обобщают понятие пропозициональной формулы, определённое в части 2.
Предикатная сигнатура – это множество символов двух типов – объектные константы и предикатные константы – с неотрицательным целым числом, называемым арностью, назначенным каждой предикатной константе. Предикатную константу мы будем называть пропозициональной, если её арность равна 0. Пропозициональные константы являются аналогом атомов в логике высказываний. Предикатная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Например, мы можем определить предикатную сигнатуру
{ a, P, Q } | (4) |
Возьмём предикатную сигнатуру s, которая включает по крайней мере одну предикатную константу и не включает ни одного из следующих символов:
- объектные переменные x, y, z, x1, y1, z1, x2, y2, z2, ...,
- пропозициональные связки,
- квантор всеобщности " и квантор существования $,
- скобки и запятая.
Терм – это объектная константа или объектная переменная. Строка называется атомарной формулой, если она является пропозициональной константой или имеет вид R(t1, ..., tn), где R – предикатная константа арности n (n > 0) и t1, ... , tn – термы. Например, если мы рассматриваем сигнатуру (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.
Например, если рассматриваемая сигнатура есть (4), тогда
Как и в логике высказываний можно доказать, что множество формул замкнуто относительно правил построения. Теоремы возможности и единственности разбора подобны соответствующим теоремам для пропозициональных формул.
В случае предикатных формул доказательство по структурной индукции имеет следующий вид. Для данного свойства формул мы проверяем, что
- каждая атомарная формула обладает этим свойством,
- для любой формулы F, обладающей этим свойством, ¬F также обладает этим свойством,
- для любых формул F, G, обладающих этим свойством, и любой бинарной связки Д, (F Д G) также обладает этим свойством,
- для любого квантора K, любой переменной v и любой формулы F, обладающей этим свойством, Kv F также обладает этим свойством.
3.2 Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?
3.3 Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?
При записи предикатных формул мы будем опускать некоторые скобки и применять другие сокращения, введённые в части 2. Строку вида
Свободные и связанные переменные
Множество свободных переменных* формулы F определяется рекурсивно, следующим образом:
Определение 22 (Свободные переменные).
- Все переменные, входящие в атомарную формулу, являются свободными переменными этой формулы,
- свободные переменные формулы F являются свободными переменными формулы ¬F,
- переменные, являющиеся свободными для хотя бы одной из формул F или G, являются свободными переменными формулы (F Д G),
- все свободные переменные формулы F кроме v являются свободными переменными формулы Kv F.
Определение 23 (Замкнутая формула). Формула без свободных переменных называется замкнутой формулой, или предложением.
Определение 24 (Связаная переменная). Переменная v связана в формуле F, если F содержит вхождение Kv, где K – квантор.
3.4 Найдите свободные переменные и связанные переменные формулы
Представление предложений русского языка предикатными формулами
Перед тем как мы продолжим изучение синтаксиса логики предикатов, полезно потренироваться в переводе предложений с русского языка в язык предикатных формул. *
В этих упражнениях для перевода рассматривается сигнатура (4). Мы предполагаем, что объектные переменные служат для обозначения натуральных чисел и интерпретируем сигнатуру следующим образом:
- a представляет число 10,
- P(x) выражает условие ``x является простым числом'',
- Q(x, y) выражает условие ``x меньше чем y''.
В каждой из следующих задач представьте данное предложение русского языка предикатной формулой.
3.5 Все простые числа больше чем x.
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) обозначает формулу
Чтобы различать ``плохие'' подстановки, как в последнем примере, от ``хороших'', мы определим, когда терм 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 тогда и только тогда, когда- t не содержит w и является подстановочным для v в F, или
- v не является свободной переменной формулы Kw F.
3.12 Терм, не содержащий ни одной связанной переменной формулы F, является подстановочным в F для любой переменной.
Определение 26 (Универсальное замыкание). Универсальное замыкание формулы F – это предложение
Семантика
Выполнимость
Логическое следование
Выводы в логике предикатов
В логике предикатов вывод определяется так же, как и в исчислении высказываний и секвенции имеют тот же синтаксис. Аксиомы тоже определяются так же, как в логике высказываний. Все правила вывода логики высказываний – правила введения и удаления для пропозициональных связок, правила противоречия и сведения к противоречию – включены в множество правил вывода логики предикатов, с метапеременными для формул понимаемыми теперь как предикатные формулы. В дополнение, есть четыре новых правил вывода: правила введения и удаления для кванторов.
Правила для кванторов всеобщности
|
| ||||||||||||||||
где 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).
Правила для кванторов существования
|
| ||||||||||||||||
где 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) и любой строки t1, ... , tn, если t1, ... , tn принадлежит X, тогда также принадлежит h(t1, ... , tn).
3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?
В логике первого порядка существуют три типа атомарных формул:
- пропозициональные константы,
- строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы,
- строки вида (t1 = t2), где t1, t2 – термы.
Для любых термов t1 и t2, t1 № t2
обозначает формулу ¬(t1 = t2).
Функциональные символы и равенство: семантика
Выводы в логике первого порядка
Определение вывода в логике предикатов с функциональными константами и равенством включает новый тип аксиом и два новых правила вывода. Правила, как и раньше, содержат метапеременные, служащие для обозначения формул и термов.
Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:
|
|
Для каждой из следующих формул найдите вывод из пустого множества посылок.
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(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:
- x' № 0.
- x'= y'Й x = y.
- x + 0 = x.
- x + y'=
(x + y)'.- x ·
0 = 0. - x · y'= x · y + x.
Интерпретация (7) является моделью этой теории. Арифметика первого порядка имеет также другие модели, и некоторые из них совсем не похожи на систему натуральных чисел (задача 3.40).
В следующих формулах 1 обозначает терм 0', 2 – 0'', и 4 – 0''''. Через t1 Ј t2 мы обозначаем формулу $ v(t2 = t1 + v), где v – первая объектная переменная, которая не встречается в t1, t2.
В каждой из следующих задач найдите доказательство данной формулы в арифметике первого порядка.
3.34 2 № 4.
3.35 x' № x.
3.36 x'= x + 1.
3.37 x Ј x.
Нестандартные модели арифметики
Термы 0, 0', 0'', ... называются цифрами. Модель M арифметики первого порядка стандартна, если для каждого c О |M| существует цифра t такая, что tM = c.3.38 Модель арифметики первого порядка (7) стандартна.
В соответствие с задачей 3.40, существуют модели арифметики первого порядка, которые не обладают этим свойством. Чтобы доказать существование такой модели, полезно рассмотреть следующую теорию первого порядка G. Сигнатура G получается из сигнатуры арифметики первого порядка добавлением буквы b в качестве новой объектной константы. Множество аксиом G получается из множества аксиом арифметики первого порядка добавлением формул b № 0, b № 0', b № 0'', ... в качестве новых аксиом.
3.39 G непротиворечива.
3.40 Арифметика первого порядка имеет нестандартную модель.
Существование нестандартных моделей арифметики следует из теоремы Сколема (1920), который обобщил раннюю работу Леопольда Лёвенхейма (1915). Возможность таких моделей резко контрастирует с результатом задачи 1.41. Разница связана с тем, что язык арифметики первого порядка является слишком ограниченным для выражения аксиомы индукции. ``Арифметика второго порядка'', в которой схема индукции заменяется по аксиоме (8), не имеет нестандартных моделей.