План лекций (очень подробный), страница 2

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

формульном, так и словесном виде) записываются без кванторов (квантор-

ных слов), но при этом подразумевается, что они истинны во всей облас-

ти интерпретации (тождества, правила). Такому пониманию формулы b со

свободными переменными x1,...,xn соответствует обозначение i |= b

(формула b истинна в интерпретации i), означающее, что формула В ис-

тинна в i при любых значениях переменных x1,...xn на множестве d

(i|=b[b1,...,bn] при любых b1,...bn).

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

торой a истинна (ложна). Модель/контрпример множества формул - это мо-

дель/контрпример конъюнкции этих формул.

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

тов аксиомы математических теорий (например, евклидовой геометрии) ис-

тинны не во всех интерпретациях: они имеют модели, но к ним можно

построить контрпримеры. Бывают ли формулы, истинные всегда (не имеющие

контрпримеров)? Да, например, a > a: "из a следует a" (в этом можно

убедиться, построив истинностную таблицу). Назовем их общезначимыми

(обозначая |= a). Вопрос: представляют ли такие формулы какой-либо ин-

терес с содержательной точки зрения? Введем понятие логического следо-

вания: a|=b означает, что в любой интерпретации из истинности a следу-

ет истинность b (при этом a1,...,an |= b понимается как a1&...&an|=b).

Например, если a описывает совокупность аксиом некоторой математичес-

кой теории, и в этой теории b - теорема, то их отношение можно запи-

сать как a|=b.

Т1 (теорема о дедукции). Если a и b - замкнутые формулы, то a|=b

<=> |= a>b . Д. следует из определения логического следования и истин-

ностной таблицы для импликации.

Теорема о дедукции показывает, что доказательство теорем в содер-

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

формул. С другой стороны, в некоторых общезначимых формулах можно "уз-

нать" схемы доказательств (от противного, разбор случаев, закон конт-

рапозиции и др.). Таким образом, можно сказать, что общезначимая фор-

мула - это определенная форма записи доказательства.

Пусть x1,...,xn - все свободные переменные формулы b. Тогда a.b

обозначает результат замыкания b кванторами общности, т.е. формулу

a.x1...a.xn b.

Т2. При замыкании формул кванторами общности сохраняется логичес-

кое следование (b|=c <=> a.b|=a.c). Д. следует из определений логичес-

кого следования и отношения i|=b.

Замечание. Для незамкнутых формул Т1, вообще говоря, не верна. Ее

правильное применение требует предварительного замыкания этих формул

кванторами общности.

Ключевые слова к $1: предикат, терм, формула, подформула,

атом=атомарная/элементарная формула, логическая связка, главная=внеш-

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

замкнутая формула, интерпретация, модель, контрпример, пропозициональ-

ная переменная, истинностная таблица, логическое следование, общезна-

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

$2. Исчисление натурального вывода (n-исчисление).

Правила натурального (естественного) вывода моделируют элементар-

ные приемы, используемые в содержательных доказательствах. Натуральный

вывод отличется от содержательного доказательства: 1) большей подроб-

ностью; 2) явным упоминанием всех предположений (гипотез), в том числе

- аксиом и теорем математической теории, в которой выполняется доказа-

тельство; 3) явным выделением понятия "исключаемых" в процессе вывода

гипотез; 4) фиксированным множеством правил вывода. Вывод - это дре-

весная конструкция, построенная из формул по правилам вывода (в корне

дерева располагается выводимая формула, а в листьях - гипотезы). Неко-

торые правила, по определению, исключают гипотезы: посылка правила

считается зависящей от соответствующей гипотезы, а заключение - нет.

Формула a называется выводимой в исчислении n (обознается: |-n a), ес-

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

Знание правил вывода дает возможность отличить правильно построенный

вывод от неправильного, но (вообще говоря) не помогает строить выводы.

Для этого нужны правила поиска вывода, которые описывают переход от

одного (незавершенного) фрагмента вывода к другому и позволяют, начав

с выводимой формулы, построить весь вывод.

Ниже перечислены правила НАТУРАЛЬНОГО ВЫВОДА (формулы над чертой

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

буква i в названии правила означает, что применение правила вводит ло-

гическую связку или квантор, а буква e - что уничтожает; в квадратных

скобках над одной из посылок правила указан вид исключаемых этим пра-

вилом гипотез). Конъюнкция:

f1 f2 f1 & f2 f1 & f2

&i ------- &e1 ------- &e2 -------

f1 & f2 f1 f2

Дизъюнкция:

[їf1] [їf2] [f1] [f2]

f1 f2 Б f1vf2 f3 f3

vi1 ------- vi2 ------- vi3 ------- ve ----------------

f1 v f2 f1 v f2 f1 v f2 f3

Импликация:

[f1] [їf3] [f2]

f2 f1>f2 f1 f1>f2 f1 f3

>i ------- >e1(modus ponens) --------- >e2 ----------------

f1 > f2 f2 f3

Отрицание и ложь:

[f] [їf]

їf f Б Б

Бi ----- їi --- їe ---

Б їf f

Кванторы: [(svw)f]

(svw)f a.v f (svt)f e.v f f1

ai+ ------ ae- ------ ei- ------ ee+ -----------

a.v f (svt)f e.v f f1

Обозначения:

(sxy)f - подстановка: замена в формуле f переменной x на терм y; w -

константа, не встречающаяся в заключениях правил ee+ и ai+ и в гипоте-

зах, от которых эти заключения зависят; t - терм, свободный для v в f

(терм t называется свободным для переменной v в формуле f, если пере-

менная v cвободна в f, и при замене всех вхождений v на t ни одна пе-

ременная из t не оказывается связанной);

Правила ПОИСКА НАТУРАЛЬНОГО ВЫВОДА.

Конъюнкция: Дизъюнкция:

&ai |- f1&f2 => |-f1 / |-f2 vai |- f1vf2 => їf1;їf2 |- Б

&si f1; f2 => f1&f2 vae f1vf2 |- f3 => f1|-f3 / f2|-f3

&se1 f1&f2 => f1 vsi1 f1 => f1vf2

&se2 f1&f2 => f2 vsi2 f2 => f1vf2

Импликация: Отрицание и ложь:

>ai |- f1>f2 => f1|-f2 Бsi їf; f => Б

>ae2 f1>f2|-f3 => їf3|-f1 / f2|-f3 Бdel Б |- f =>

>ae1 f1>f2 |-f2 => |-f1 їai |- їf => f |- Б

>si f2 => f1>f2 їae1 |- f => їf |- Б

>se1 f1>f2; f1 => f2 їae2 їf|- Б => |-f