Курс: Дискретная математика

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

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

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

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



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

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

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



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

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

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

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

{ a, P, Q }

(4)

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

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

• объектные переменные
  x, y, z, x1, y1, z1, x2, y2, z2, ...,
  
• пропозициональные связки,
  
• квантор всеобщности " и
  квантор существования $,
  
• скобки и запятая.
  

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

Терм – это объектная константа или объектная переменная.
Строка называется атомарной формулой,
если она является пропозициональной константой или имеет вид
R(t1, ..., t_n),
где R – предикатная константа арности n (n > 0) и
t1, ... , 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. Строку вида

" v1 ··· " v_n (n і 0)
будем писать как " v1 ··· 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(z2) есть
" y (P(y) Й Q(z2, y)),
что значит ``все простые числа больше чем z2''.
Существует, однако, одно исключение. Формула 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 – это предложение

" v1 ··· v_n F,
где v1, ... , 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) и любой строки
  t1, ... , t_n, если t1, ... , t_n
  принадлежит X, тогда также принадлежит h(t1, ... , t_n).
  

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

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

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

• пропозициональные константы,
  
• строки вида R(t1, ... , t_n)
  где R – предикатная константа арности n (n > 0) и t1, ..., t_n
  – термы,
  
• строки вида (t1 = t2), где t1, t2 – термы.
  

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

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

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

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

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

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

G |– t1 = t2 G |– F(t1) (З=) G |– F(t2)

G |– t1 = t2 G |– F(t2) G |– F(t1)

где t1 и t2 свободные для 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(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2.
Аксиомы арифметики первого порядка
являются универсальным замыканием следующих формул:

1. x' № 0.
   
2. x'= y'Й x = y.
   
3. (F(0) & " v (F(v) Й F(v'))) Й " v F(v)
   для любой формулы F(v).
   
4. x + 0 = x.
   
5. x + y'= (x + y)'.
   
6. x · 0 = 0.
   
7. 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 такая, что
t^M = 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), не имеет нестандартных моделей.

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

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

Недоказуемые теоремы для диофантовых уравнений