Теория доказательств классической логики предикатов

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

И все же профессиональный исследователь в области логического познания, изгоняя крамолу допущения некоторой «содержательной логики», отличной от изучаемой и развиваемой им, всегда готов признать, что значительная часть теоретической логики занимается исключительно формальными проблемами, никак не связанными непосредственно с изучением и моделированием реальности. Эта часть логики называется теорией доказательств, в которой анализируются проблемы эффективной и регулярной выводимости одних логических структур из других, не заботясь о том, какие содержательные интерпретации могли бы быть для них подходящими.

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

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

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

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

Аксиомы КЛП-исчисления

АО Все тезисы классической логики высказываний (КЛВ).

А1 Р(у)—gt;ЭхР(х)

А2 VxP(x) р(у)

Логические правила вывода в КЛП-исчислении

Г)1 Если I—А — Ви h-А, то Ь~В.

ГІ2 Если А содержит переменные р,,..., рп, а В получается из А подстановкой в А формул

С, Сп вместо р1(рп соответственно, то

1. А влечет I—В.

Г)3 Если С есть подформула формулы А, Д есть подформула формулы В, а В получается из А

заменой С на Д, то из С Д следует, что А«-gt; В.

Г)4 Если В -» А(х) и формула В не содержит переменной х, то |— В-gt; vxA(x)П5 Если ь— А(х) -у В и формула В не содержит переменной х, то ь- 5]хА(х)-» В.

Определение 5.17. Доказательством в КЛП-ис- числении называется последовательность формул КЛП-языка, каждая из которых является либо одной из аксиом А0-А2, либо формулой, полученной из предшествующих в последовательности по одному из правил вывода П1-П5.

Следующие утверждения являются тезисами КЛП-исчисления.

Т1. VxP(x) -іЗх-іР(х)

A2

Из (1) по КЛВ Из (2) по П5 Из (3) по КЛВ

1. VxP(x) —» Р(у)
2. —iP(y) -» —iVxP(x)
3. Зх-іР(х) -» -iVxP(x)
4. VxP(x)              —i3x-,P(x)

T2. -,Vx—iP(x) -gt; 3xP(x)

A1

Из (1) по КЛВ Из (2) по П4 Из (3) по КЛВ

1. P(y) -» 3xP(x)
2. -,3xP(x)              —iP(y)
3. -gt;3xP(x)              Vx-gt;P(x)
4. -iVx—iP(x) —» 3xP(x)

ТЗ. (VxP(x) v VxQ(x)) -» Vx(p(x) v Q(x))

1. VxP(x) -gt; P(y)              A2
2. VxQ(x) -» Q(y)              A2

3. (VxP(x) v VxQ(x)) -» (P(y)v Q(y)) Из (1), (2) no

KJIB

4. (\/хР(х) v VxQ(x)) —gt; Vx(p(x) v Q(x)) Из (3) по П4

T4. Зх(Р(х) л Q(x)) -» (ЗхР(х) л 3xQ(x))

!•              P(y) —» 3xP(x)              A1

2‘              Q(y) -gt; 3xQ(x)              A1

3. P(y) л Q(y) -gt; (ЗхР(х) л 3xQ(x))              Из (1), (2) no

KJIB

4. 3x(p(x) л Q(x)) -» (ЗхР(х) л 3xQ(x)) Из (3) по П5

Упражнение

11. Докажите, что все формулы упр. 5 6 являются КЛП-тезисами.