5.5 Аксиоматическое построение лп. Исчисление предикатов

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

Как и в алгебре логики, формальное аксиоматическое построение в ЛП называется исчислением предикатов (ИП).

Принципы задания ИП те же, что и у ИВ. При выборе аксиом {A} можно принять

а) систему независимых аксиом, содержащую минимальное их количество, либо

б) расширенную систему аксиом, позволяющую упростить проверку истинности конкретных формул.

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

венные признаки систем.

Рассмотрим построение ИП по Э.Мендельсону.

I.Множество логических связок {f} = {, }.

II. В определении формул по сравнению с ЛП должно быть

учтено более узкое множество логических связок. Их вво-

дят следующим образом:

210

1. Если (t₁ , ..., t_k) - термы, (х₁ , ..., х_m) - множество пере-менных, входящих в них, а Р- предикатная переменная, то Р( t₁ , ..., t_k ) - назовем элементарной формулой или атомом, а (х₁ , ..., х_m ) - его свободными переменными.

2. Если А и В - формулы, то выражения вида F = АВ, F = А тоже являются формулами. Свободные переменные формул А и В являются свободными переменными формулы F.

3.Если А - формула со свободными переменными (х₁,...,х_m ), то выражения вида F = х_i А(х₁ , ..., х_m ), F = х_i А(х₁ , ..., х_m ) - тоже являются формулами, в которых переменная х_i связана, соответственно, кванторами  и  , а переменные (х₁ , ..., х_m ) \ х_i -свободны в F.

III.Множество аксиом А₁, А₂, А₃, А₄, А₅ = {A} следующее:

А₁: А  (В  А);

А₂: (А  (В  С))  ((А  В)  (А  С));

А₃: ( В   А)  (( В  А)  В);

А₄: х А(х)  А(у), где А(х) есть формула теории, а у - терм

теории, свободный для х в А(х);

А₅: х(А  B) ( А хB), если формула А не содержит свободных вхождений х.

IV. Множество правил вывода {P}:

а) modus ponens ,б) правило обобщения (свёртывания кван-тора общности):А хA.

В данной системе аксиомы независимы, их число ми-нимально. Однако это приводит (как и в ИВ) к тому, что в ней усложняется построение выводов. Поэтому рассмат-риваются построения ИП и с расширенными наборами ак-сиом.

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

В теориях первого порядка (К) допускаются кванторы и предикаты по предметным переменным. Они позволяют описывать логику достаточно содержательных математи-

211

ческих дисциплин - например, арифметики. Теории, в кото-рых эти ограничения сняты, имеют более высокий порядок. Рассмотрим аксиоматическое построение теорий первого порядка.

1.Определения терма и формулы остаются в силе.

2. Все множество аксиом делится на две части:

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

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

3. В качестве правил вывода в любой теории К достаточно принять правила вывода, применяемые в ИП, поскольку вы-вод формул является чисто логическим действием и пра-вильность его определяется тождественной истинностью тавтологий, используемых в них.

Простейшие примеры теорий первого порядка можно построить на основании отношений эквивалентности и по-рядка, применяемых в теории множеств.

I. Теории первого порядка с равенством. Пусть на некото-ром предметном множестве М задано некоторое множество предметных переменных Х, предметных констант A , функ-циональных переменных F.

Множество предикатных переменных содержит логи-ческую функцию Р = Р(х,у) = ‘ х эквивалентно у ’ (либо ‘x=y’). В общем случае отношение эквивалентности удов-летворяет аксиомам:

1) рефлексивности: х Х (х  x) ,

2) симметичности: х,у  Х (если (х  у),то (у  x ) ,

3) транзитивности: х,у,z  Х (если х у и у z, то x z).

Для того, чтобы обеспечить выполнение данных свойств в теориях с равенствами, их можно было бы непо-

212

средственно добавить в качестве аксиом к логическим ак-сиомам. Однако обычно вместо них используют упрощён-ный набор аксиом следующего вида:

1) x (x = x) - рефлексивность равенства,

2) (x = y) (A(x,x)  A(x,y)) - подстановочность равенства.

Справедливость обычных аксиом симметричности и транзитивности можно вывести из 1)- 2) с использованием тавтологий ИВ.

II.Теория частичной упорядоченности.

Пусть М - некоторое множество объектов, Х – мно-жество предметных переменных на М.

Предметных констант нет: A = .

Функциональных переменных нет: F = .

Множество предикатных переменных Р = Р(х,у)=‘х строго предшествует у ’ = ‘ х < у ’.

Бинарное отношение строгого порядка удовлетворяет аксиомам:

1) антирефлексивности: х Х (х  x) ,

2) асимметичности: х,у  Х (если (х  у),то (у  x ) ,

3) транзитивности: х,у,z  Х (если х у и у z, то x z).

Подход к аксиоматическому заданию теории частич-ной упорядоченности, включающей данное отношение, ана-логичен включению отношения эквивалентности. Вместо полного добавления к аксиомам ИП аксиом 1)-3) присое-диняются только аксиомы 1) антирефлексивность и 3) тран-зитивность. Асимметричность можно вывести из получив-шегося набора аксиом. В теориях частичной упорядочен-ности отношение строгого порядка на элементах пред-метного множества всегда вводит строгий частичный поря-док (строгий полный - не всегда).

Задачи.

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

213