21. Свойства выводимости.

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

Свойства выводимости.

1. Если множество Г является Ф из Г выводится |-G => Ф|-G.

2. Если известно, что из Ф|-G и что любого В из Ф выводится Г|-В, то верно что из Г |-G.

3. Если Г бесконечно и из Г |- G, то в Г существует Г’ что из Г’|-G, причем иногда говорят что Г’ конечно, т.к. длина цепочки вывода конечна.

22. Понятие логического следования.

Формула F логически следует из множества формул G или, как говорят, множество формул G влечет множество формул F, G|-F, если для каждой интерпретации, при которой все формулы из G истинны, формула F также истинна. Можно говорить что F это логическое следование из G, ну или F следует из G, когда G и ~F невыполнимы одновременно. Подошли к логическому следованию с точки зрения интерпретации, рассматривая же его как формальный механизм, мы можем вмести понятия пропозиционального вывода, эквивалентного понятию логического вывода. Соответственно понятие пропозиционального вывода множество формул G влечет F, если F может быть выведено из G с использованием определенного набора правил вывода. Заметим, что правило вывода строится так, чтобы выражение F|-G и F выводится из G были эквивалентны. Понятие логического следования основано на смысле и является семантичным, понятие пропозиционального вывода основывается на правилах трактования формул и является синтаксическим.

Секвенция – выражение вида G|-F или F предпосылка G или вида G|-ложь, что значит что посылки G противоречивы. Здесь F – формула, G – некоторое конечное множество формул. Собственно, переход от сформулированных еще Аристотелем силлогических суждений, т.е. правил умозаключений, на естественном языке, т.е. переход к полным формальным правилам вывода был предложен еще Де Морганом в середине 19 века. Де Морган считал, что семантика естественного языка искажает строгий смысл правил умозаключений, поэтому он стремился перейти к манипуляциям с символами, не зависящим от того, какой смысл этим символам приписывается. Правило вывода – предписание, позволяющее из суждения 1 логической структуры, как предпосылок, вывести суждение другой логической структуры, как заключение. Правило вывода записывается в виде схемы, состоящей из верхней и нижней части. В верхней части записываются логические схемы предпосылок, в нижней логические схемы заключений. Сейчас будем использовать понятие вывода более сложное, чем то, которым будем пользоваться дальше, однако в рамках более сложного определения прекрасно укладываются некоторые метатеоремы. Все правила вывода делятся на 2 группы: основные и производные. Основные правила являются очевидными и не нуждаются в доказательстве, их делят, в свою очередь, на прямые и косвенные. Прямые правила непосредственно указывают на выводимость одних суждений из других. Косвенные дают возможность умозаключить о правомерности вывода одних суждений из других. Пример косвенного правила: правило введения дизъюнкции, из (G|-F)/(G|-FvU). Очевидно, т.к. F всегда истинно при истинных G, мы можем через дизъюнкцию приписать все, что угодно. Это правило, как видим, не содержит извлечения какой-либо части из суждений G и F, а просто говорит о формальном праве считать формулу FvU выводимой из G. Есть еще производные правила. Они описывают сокращенный процесс вывода. Выводятся из основных, т.е. если мы построили какую-то универсальную цепочку вывода, в которую может подставлять различные формулы, то этим результатом мы можем пользоваться многократно. Как мы уже говорили, правило вывода строится так, чтобы синтаксическое и семантическое определение логического следования совпадали. В связи с этим, говорят о корректности правил вывода. Правило вывода считается корректным, если для каждого примера этого правила, посылки которого являются тождественно истинными, его заключения также тождественно истинны. В данном случае примером правила будет указание конкретного множества формул G и конкретной формулы F, а также конкретной формулы U.