Архитектура Аудит Военная наука Иностранные языки Медицина Металлургия Метрология Образование Политология Производство Психология Стандартизация Технологии |
Метатеоретические свойства исчисления высказываний
1. Построенное исчисление со схемами аксиом и натуральное исчисление высказываний являются дедуктивно эквивалентными. Для доказательства этого утверждения необходимо показать, что все схемы теорем и правила вывода в натуральном исчислении производны от дедуктивных средств системы исчисления высказываний со схемами аксиом, и наоборот. Так, единственным правилом вывода в обеих системах исчисления высказываний является правило 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 называется разрешимой, если существует алгоритм, позволяющий для любой формулы языка теории в конечное число шагов определить, является ли эта формула теоремой или нет. Так как любая формула – это конечный объект, мы можем в конечное число шагов построить таблицу истинности для данной формулы и установить, является ли она тождественно-истинной или нет. Популярное:
|
Последнее изменение этой страницы: 2017-03-09; Просмотров: 699; Нарушение авторского права страницы