3.5. Исчисление предикатов первого порядка

Уже упоминавшийся выше силлогизм “Люди смертны...” не может быть представлен с помощью исчисления высказываний. Действительно, для его формализации необходимо ввести квантифицированную переменную “человек”, причем множественность, отражающаяся в первой посылке силлогизма, указывает на ее универсальность: “Всякий х, который обладает свойством “человек”, смертен”.

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

с ними, называемых индивидными, или предметными переменными. Первая посылка нашего примера в формализованном виде записывается так:

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

Определение исчисления предикатов первого порядка.

1. Алфавит:

• константы:

• индивидные переменные:

• предикаты:

• логические операторы:

• квантор всеобщности: V (читается бы ни

2. Построение формул:

• формулы исчисления предикатов образуются аналогично формулам исчисления высказываний и, кроме того,

• каждому предикату приписывается вес выражение является формулой, если и только если вес равен ;

• выражение представляет собой формулу, в которой есть связанная переменная, а свободные переменные при

3. Аксиомы:

• имеются все три аксиомы исчисления высказываний; а также аксиомы:

где суть формулы, не является свободной переменной в

4. Правила словообразования:

(обобщение), где — свободная переменная в

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

символы Отметим, что известный квантор существования (читается “существует, найдется”) выражается через квантор всеобщности и другие операторы так:

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

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

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

Пример доказательства в исчислении предикатов первого порядка.

Каков бы ни был предикат с весом, равным двум, выполняется следующее:

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

Теперь, положив уже получим

Используя последнее правило словообразования в определении исчисления предикатов, получаем

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

Что и требовалось доказать.

Аналогично могут быть доказаны и приведенные ниже следующие важные теоремы исчисления предикатов:

Первая теорема Геделя: о "полноте” исчисления предикатов (1930 г.)

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

Эта теорема в исчислении предикатов аналогична теореме Поста в исчислении высказываний. Однако в отличие от теоремы Поста теорема Геделя в исчислении предикатов не приводит к эффективной процедуре решения. Более подробно этот вопрос рассмотрен в разд. 6.3.

3.5.1. Формальная арифметика

В этом разделе описывается формальная система, которая была разработана Пеано и которая является расширением исчисления предикатов. Она известна под названием формальная арифметика, или теория чисел.

В формальной арифметике по сравнению с исчислением предикатов дополнительно вводятся одна константа, четыре оператора и девять аксиом. Этой новой константой является О (нуль).

Дополнительные операторы:

— операция “непосредственно следующий” (например, для числа это число ;

“плюс”, оператор сложения;

- “умножить на”, оператор умножения;

= - “равно”, оператор равенства, играющий особую роль среди новых аксиом.

Оператор о имеет вес, равный единице, а три остальных оператора имеют вес, равный двум.

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

для всякой формулы данной формальной системы.

В последней аксиоме формализуется рекуррентное рассуждение, называемое принципом формальной или математической индукции. Многие классические результаты не вошли в явном виде в эту систему аксиом и должны быть специально доказаны, как, например, свойство или в обычной форме записи:

Формальная арифметика играет исключительно важную роль в математической логике.

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

Напомним, что система определяется одной аксиомой и одним правилом вывода где представляют собой какие-либо цепочки символов

Символы этой системы являются ничем иным, как кодами, в качестве которых могут быть использованы любые другие символы и, в частности, цифровые символы 1, 2, 3. В этом случае аксиома выглядит, как 131, а правило выразится следующим образом: если формула, включающая с последующей цифрой 2 с последующей является теоремой, то и формула, состоящая из 2, за которой следует затем 3, затем 2, затем также является теоремой.

Операция “следует за” (“с последующим”, “быть сопровождаемым”) имеет соответствие в формальной арифметике. В обычной арифметике, чтобы построить число х, за которым следует число у, используя десятичную форму представления, достаточно умножить х на соответствующую степень числа 10 и прибавить у. Более строго это записывается так: если у состоит из цифр, т. е. представляет собой число

где число не есть нуль, то в этом случае “число х с последующим у" есть не что иное, как число Чтобы получить результат от применения правила к этой форме, начиная с правого его конца

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

Чтобы получить формулу 2, сопровождаемую начиная с добавляют .

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

Если имеется теорема

где числа содержат соответственно цифр, пусть это будут

то является теоремой и выражение

Таким образом, начиная с теоремы 2213221 при с помощью правила порождают теорему

или

или же 222132221.

Таким образом, исследование системы полностью сводится к исследованию подсистемы формальной арифметики.

Этот же метод может быть использован и для системы Закодировав символы соответственно через 2, 1, 0,

получаем аксиому в виде: 2 1. Правило например, тогда записывается так:

«Если является теоремой содержит цифр), то будет теоремой и выражение

Таким образом, теперь система также “погружена” в формальную арифметику.

При таком подходе доказательство теорем и метатеорем в формальных системах или сводится, следовательно, к доказательствам в формальной арифметике. Разумеется, на этой стадии имеется возможность для каждой арифметизированной формальной системы дать интерпретацию в самой формальной арифметике. Таким образом, в арифметизированной системе интерпретируется как 1, 2 интерпретируется как “последующее число”; 3 интерпретируется как

В этом случае, исходя из теоремы 222132221, получаем “истинное” выражение и в обычном смысле: Таким образом, кольцо замкнулось. Этот тип рассуждений приводит ко второй теореме Геделя.