Дискретно-непрерывная математика (стр. 8 )

Рассмотрим для примера доказательство в С2 теоремы

1.- подстановка в аксиому (2): вместо и вместо r/p,

2.- подстановка в аксиому (1): вместо

3.- из 1 и 2 по правилу МР.

4.- подстановка в аксиому (1): вместо q/p.

5.из 3 и 4 по правилу МР.

Таким образом,

В качестве «вспомогательного» правила весьма полезной является теорема дедукции, когда какое-нибудь утверждение B

доказывают в предположении верности другого утверждения А, после чего заключают, что верно утверждение «если A, то B»:

Теорема дедукции. Если Г — множество формул, А и В — формулы и то B частности, если В, то

(Теорема дедукции называется стандартной, если для импликации выполняются свойства утверждения консеквента и самодистрибутивности (см. выше).)

Исходя из синтаксического представления логики высказыва­ний, последняя зачастую отождествляется с множеством теорем или, что более принято, с отношением выводимости . Итак, при семантическом подходе формулы интерпретируются как функции на множестве из двух элементов {0, 1}, и нас интересуют тавтологии и противоречия, а при синтаксическом - как определенный набор символов, и различаются только теоремы и не теоремы. Однако, несмотря на такое различие, оба подхода к построению логики высказываний, по существу, эквивалентны и, как говорят, являются адекватными друг другу. Это значит, что понятия логического следования и вывода равнообъемны. Рассмот­рим в связи с этим весьма примечательную теорему.

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

когда

(Теорема адекватности в виде: для всякой формулы т. т.т., когда - носит название «строгой теоремы адекватности».)

Доказательство в одну сторону, а именно: для всех А, если то— носит название теоремы о корректности. Это

минимальное условие, которое мы требуем от логического исчис­ления и которое состоит в том, что представленная нами семантика корректна для выбранной аксиоматизации. Для доказательства теоремы нужно проверить, что все наши аксиомы (1) — (10) являются тавтологиями, что легко устанавливается непосредствен­ной проверкой с помощью истинностных таблиц. А наши правила вывода выбраны таким образом, что они сохраняют тавтологию (см. [Чёрч I960) в том смысле, что если посылка (или посылки) является тавтологией, то и заключение - тавтология. Поэтому все формулы последовательности, образующей вывод какой-либо теоремы исчисления С2, в том числе и сама доказанная теорема, являются тавтологиями, Из этой теоремы следует важнейшее свойство исчисления высказываний С2, свойство непротиворечивости: не существует формулы А такой, чтобы А и

были теоремами. Согласно теореме о корректности, каждая

теорема С2 является тавтологией. Как уже говорилось, отрицание тавтологии не есть тавтология, Следовательно, ни формула А, ни формула не могут быть одновременно теоремами в С2.

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

Имеет место и обратное утверждение о том, что каждая тавто­логия доказуема, т. е. для всякой формулы А, если то Доказательство этой теоремы не столь тривиально и носит назва­ние теоремы о полноте (дедуктивной) исчисления высказываний относительно предложенной семантики. По существу здесь утвер­ждается, что логических средств, т. е. аксиом и правил вывода исчисления высказываний С2 вполне достаточно для доказатель­ства всех тавтологий. Таким образом, главная цель достигнута: используя минимальные средства, можно обозреть всё множество тавтологий.

1.5. Историческая справка

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

была представлена аксиоматизация С2 Г. Фреге в 1879 г. (см. [Фреге 2000]. Она была значительно упрощена Я. Лукасевичем [Lukasiewicz and Tarski 1930]:

1.

2.

3. (обратная контрапозиция).

Правила вывода: МР и подстановка.

Детально эта аксиоматизация С2 исследуется А. Чёрчем [Чёрч I960].

(Нам она понадобится при сравнении С2 с трехзначной логикой Лукасевича В следующей главе мы покажем, что эта аксиоматизация обладает свойством независимости аксиом, что приводит к появлению трехзначных логик.)

В терминах современного символического языка аксиомати­зация С2 впервые появилась в «Prmcipia Mathematica» А. Уайтхеда и Б. Рассела [Whitehead and Russell 1910-1913], где в качестве исходных связок взятыУ Фреге и здесь вопрос о полноте просто не возникал. Их целью было показать, что вся логика, а в действительности вся математика, может быть развита внутри их системы, основанной на классической логике. Первая публикация доказательства функциональной и дедуктивной полноты С2 принадлежит Э. Посту [Post 1921], который исходил из системы Уайтхеда и Рассела. Для доказательства теоремы адекватности Пост использовал двузначные истинностные таблицы (приведенные выше). Основы алгебры логики заложены в 1847 г. в работах Дж. Буля и А. де Моргана.

Алгебраические, аспекты С2 рассмотрим в гл. 4.

1.6. Логика предикатов

Изложение этой темы имеется во всех учебниках по современной логике, среди которых одним из лучших является [Мендельсон 1984], которому мы и будем в основном следовать. См. также работу [Hodges 2001], специально посвященную элементарной логике предикатов.

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

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

Существуют такие виды логических рассуждений, которые не могут быть обоснованы в рамках логики высказываний. Например, «Все люди смертны», «Сократ — человек». Следовательно, «Сократ смертен».

Корректность этого рассуждения покоится не только на истинностно-функциональных отношениях между входящими в них высказываниями, но и на внутренней структуре самих высказываний, а также на понимании таких выражений, как «все», «всякий», «некоторый» и т. д. Поэтому удобно ввести специальные обозначения для определенных часто встречающихся выражений. Если Р(х) означает, что х обладает свойством Р, то посредством будем обозначать утверждение: «все х обладают свойством Р». Записьбудет обозначать, что «существует предмет х,

обладающий свойством Р». В выражении часть

называется квантором всеобщности, а частьв выражении называется квантором существования. Как отмечается в [Гильберт и Бернайс 1979, в эвристических целях лучше трактовать всеобщность как распространенную на всю индивидную область (быть может, бесконечую) конъюнкцию, а существование - как распространенную на всю индивидную область дизъюнкцию. Именно такое понимание кванторов часто используется в многозначной логике.

Пусть s обозначает «Сократ», М(х) обозначает «х есть человек», a D(x) обозначает «х смертен». Тогда вышеприведенное рассуждение можно записать следующим образом: из посылок и M(s) следует D(s). Заметим, что справедливость этого заключения не зависит от того, какой конкретный смысл имеют символы s, М и D.