Метатеоретические свойства системы исчисления со схемами аксиом и натурального исчисления высказываний
Метатеоретические свойства исчисления высказываний
1. Построенное исчисление со схемами аксиом и натуральное исчисление высказываний являются дедуктивно эквивалентными. Для доказательства этого утверждения необходимо показать, что все схемы теорем и правила вывода в натуральном исчислении производны от дедуктивных средств системы исчисления высказываний со схемами аксиом, и наоборот. Так, единственным правилом вывода в обеих системах исчисления высказываний является правило modus ponens. Также все правила натурального исчисления являются производными в аксиоматическом исчислении.
Правило введения импликации – это modus ponens системы аксиоматического исчисления, а правила введения конъюнкции, исключения конъюнкции и введения дизъюнкции могут быть получены из соответствующих схем аксиом. Например, нам необходимо обосновать средствами исчисления высказываний со схемами аксиом правила введения конъюнкции:
(1) 
– схема аксиом CA5;
(2) A – посылка;
(3) 
– по правилу modus ponens из (1), (2);
(4) B – посылка;
(5) 
– по правилу modus ponens из (3), (4).
Таким образом, осуществлена схема вывода 
, которая и обосновывает наличие в исчислении высказываний со схемами аксиом правила введения конъюнкции. По аналогии можно доказать правила исключения конъюнкции, введения дизъюнкции и исключения отрицания натурального исчисления высказываний. Что касается правила исключения дизъюнкции, то здесь ситуация сложнее, так как для начала необходимо доказать, что формулы 
(отрицание антецендента) и 
являются теоремами.
|
|
|
Доказательство 
– закона отрицания антецендента
(1) A – посылка;
(2) 
– посылка;
(3) 
– частный случай CA1;
(4) 
– частный случай CA1;
(5) 
– modus ponens к (3), (1);
(6) 
– modus ponens к (4), (2);
(7) 
– частный случай CA9;
(8) 
– modus ponens к (7), (6);
(9) B – modus ponens к (8), (5);
(10) 
– теорема дедукции к (2)–(9);
(11) 
– теорема дедукции к (1)–(10).
Теорема доказана.
Доказательство 
(1) 
– закон отрицания антецендента;
(2) 
– частный случай CA1;
(3) 
– CA8;
(4) 
– modus ponens к (3), (1);
(5) 
– modus ponens к (4), (2).
Теорема доказана.
Обоснование правила исключения дизъюнкции 
|
|
|
(1) 
– теорема из предыдущего доказательства;
(2) 
– посылка;
(3) 
– modus ponens к (1), (2);
(4) 
– посылка;
(5) B – modus ponens к (3), (4).
Правило введения импликации представлено в исчислении высказываний со
схемами аксиом теоремой дедукции и является, как мы уже убедились, производным. Правило введения отрицания также производно. Формально оно может быть записано так:
.
Доказательство правила
(1) 
– допущение;
(2) 
– допущение;
(3) 
– CA10;
(4) 
– свойство сечения к (3), (1) и перестановка;
(5) 
– свойство сечения к (3), (2) и перестановка;
(6) 
– теорема дедукции к (4);
(7) 
– теорема дедукции к (5);
(8) 
– выводимость на основе CA9;
(9) 
– сечение к (7), (8);
(10) 
– сечение к (6), (9), перестановка и сокращение.
|
|
|
Все правила натурального исчисления производны в исчислении высказываний со схемами аксиом.
Учитывая дедуктивную эквивалентность данных систем, мы можем использовать в доказательствах все правила натурального исчисления. Все свойства, которые будут установлены для исчисления высказываний со схемами аксиом, справедливы также и для натурального исчисления высказываний.
2. Исчисление высказываний со схемами аксиом является синтаксически и семантически непротиворечивым. Некоторая логическая теория Т называется семантически непротиворечивой, если любая доказуемая в ней формула является тождественно-истинной (общезначимой), т. е. имеет место отношение 
, где запись 
обозначает доказуемость A в Т, а знак « 
» – метаязыковой квантор общности. Это положение доказывается очень просто – при помощи таблиц истинности. Для каждой схемы аксиом строится своя таблица истинности и показывается, что она является тождественно-истинной.
Произвольная логическая теория T является синтаксически непротиворечивой, если в ней невозможно одновременное доказательство некоторой формулы и ее отрицания, т. е. 
, где символы с точками – это метазнаки отрицания, квантора существования и конъюнкции.
|
|
|
3. Исчисление высказываний со схемами аксиом является семантически и синтаксически полным. Некоторая логическая теория T считается семантически полной, если в ней доказуема любая тождественно-истинная (общезначимая) формула, т. е. в ней имеет место отношение 
. Логическая теория T, сформулированная с помощью схем аксиом, считается синтаксически полной, если к ней нельзя присоединить без противоречия ни одной недоказуемой в ней схемы формул. Из этого следует, что синтаксис и семантика рассмотренного аксиоматического исчисления адекватны друг другу. Данное исчисление адекватно формализует содержательное понятие логического закона пропозициональной логики, а также и содержательное понятие логического следования этой логики.
4. Система исчисления высказываний со схемами аксиом является разрешимой. Произвольная логическая теория T называется разрешимой, если существует алгоритм, позволяющий для любой формулы языка теории в конечное число шагов определить, является ли эта формула теоремой или нет. Так как любая формула – это конечный объект, мы можем в конечное число шагов построить таблицу истинности для данной формулы и установить, является ли она тождественно-истинной или нет.
Дата добавления: 2018-04-05; просмотров: 413; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!