Конструктивная математика (стр. 3 )

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



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

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

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



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

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

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

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

{ a, P, Q }

(4)

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

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

объектные переменные 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.

Строка 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 ··· ∀ vn (n ≥ 0)

будем писать как ∀ v1 ··· vn, и подобным образом для квантора существования.

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

Множество свободных переменных* формулы 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 тогда и только тогда, когда t не содержит w и является подстановочным для v в F, или v не является свободной переменной формулы Kw F.

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

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

∀ v1 ··· vn F,

где v1, ... , vn – все свободные переменные F.

Семантика

Выполнимость

Логическое следование

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

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