Теория доказательств классической логики предикатов
Теоретическую логику иногда называют формальной к огромному неудовольствию большинства исследователей в области логической науки и ее истинных почитателей. Такая неудовлетворенность в терминологии вызвана прежде всего тем, что под термин «формальная логика», преднамеренно или по незнанию, подводят всю современную структуру логики в целом, отказывая ей в какой-либо содержательной значимости.
Однако это, конечно, не так. Теория моделей классической логики предикатов — образца современной логической теории — обнаруживает глубинный содержательный смысл, заложенный в такие семантические категории, как понятие модели или истинности. Содержательные аспекты логического исследования были подробно рассмотрены и изучены в предшествующем разделе.И все же профессиональный исследователь в области логического познания, изгоняя крамолу допущения некоторой «содержательной логики», отличной от изучаемой и развиваемой им, всегда готов признать, что значительная часть теоретической логики занимается исключительно формальными проблемами, никак не связанными непосредственно с изучением и моделированием реальности. Эта часть логики называется теорией доказательств, в которой анализируются проблемы эффективной и регулярной выводимости одних логических структур из других, не заботясь о том, какие содержательные интерпретации могли бы быть для них подходящими.
Теория доказательств, в первом приближении, исследует логические правила образования формальных структур, то есть формализованного языка теории, а также правила преобразования этих структур в другие формальные структуры. Последние являются логическими правилами вывода и доказательства. В разделе 4.2, относящемся к классической логике высказываний, уже затрагивались эти вопросы в рамках изучения дедуктивной теории натурального вывода.
В этом разделе будут сформулированы некоторые вводные положения и замечания, связанные с рассмотрением аксиоматического метода в теории доказательств классической логики предикатов.
Аксиоматический метод является древнейшим в логических исследованиях и методологии научного познания. Еще два с половиной тысячелетия назад аксиоматический метод стал образцом систематизации научного знания и основным ответом на вопрос о принципах его построения.Аксиоматический способ построения научной теории основывается существенным образом на различении ее исходных и производных элементов. Исходные утверждения теории, не анализируемые в ней содержательно, обычно называют аксиомами или постулатами. Исходные понятия теории — это ее концептуальные допущения, взятые без определений. Из аксиом и постулатов теории в процессе доказательства выводится по логическим правилам вывода система дедуктивно-замкнутых утверждений —- теорем теории. Из концептуальных допущений, принятых в теории, по определениям и дефинициям задаются новые, производные понятия, связанные дефиници- ально с исходными и образующие вместе с ними единую концептуальную структуру.
Теория доказательств классической логики предикатов в аксиоматической форме может быть представлена следующим образом.
Аксиомы КЛП-исчисления
АО Все тезисы классической логики высказываний (КЛВ).
А1 Р(у)—gt;ЭхР(х)
А2 VxP(x) р(у)
Логические правила вывода в КЛП-исчислении
Г)1 Если I—А — Ви h-А, то Ь~В.
ГІ2 Если А содержит переменные р,,..., рп, а В получается из А подстановкой в А формул
С, Сп вместо р1(рп соответственно, то
- А влечет I—В.
Г)3 Если С есть подформула формулы А, Д есть подформула формулы В, а В получается из А
заменой С на Д, то из С Д следует, что А«-gt; В.
Г)4 Если В -» А(х) и формула В не содержит переменной х, то |— В-gt; vxA(x)П5 Если ь— А(х) -у В и формула В не содержит переменной х, то ь- 5]хА(х)-» В.
Определение 5.17. Доказательством в КЛП-ис- числении называется последовательность формул КЛП-языка, каждая из которых является либо одной из аксиом А0-А2, либо формулой, полученной из предшествующих в последовательности по одному из правил вывода П1-П5.
Конечная формула последовательности доказательства называется доказуемой формулой КЛП-исчисления или КЛП-тезисом. Обозначается: 1-А.Следующие утверждения являются тезисами КЛП-исчисления.
Т1. VxP(x) -іЗх-іР(х)
A2
Из (1) по КЛВ Из (2) по П5 Из (3) по КЛВ
- VxP(x) —» Р(у)
- —iP(y) -» —iVxP(x)
- Зх-іР(х) -» -iVxP(x)
- VxP(x) —i3x-,P(x)
T2. -,Vx—iP(x) -gt; 3xP(x)
A1
Из (1) по КЛВ Из (2) по П4 Из (3) по КЛВ
- P(y) -» 3xP(x)
- -,3xP(x) —iP(y)
- -gt;3xP(x) Vx-gt;P(x)
- -iVx—iP(x) —» 3xP(x)
ТЗ. (VxP(x) v VxQ(x)) -» Vx(p(x) v Q(x))
- VxP(x) -gt; P(y) A2
- VxQ(x) -» Q(y) A2
- (VxP(x) v VxQ(x)) -» (P(y)v Q(y)) Из (1), (2) no
KJIB
- (\/хР(х) 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
- P(y) л Q(y) -gt; (ЗхР(х) л 3xQ(x)) Из (1), (2) no
KJIB
- 3x(p(x) л Q(x)) -» (ЗхР(х) л 3xQ(x)) Из (3) по П5
Упражнение
- Докажите, что все формулы упр. 5 6 являются КЛП-тезисами.