§ Определение доказуемой (выводимой) формулы

Вид материала

Документы

Содержание Система аксиом исчисления высказываний. 2 Правило заключения (ПЗ). Определение выводимой (доказуемой ) формулы.

Подобный материал:

• Домашнее задание для 10К на 14-19 февраля, 20.64kb.
• Домашнее задание для 10А на 14-19 февраля, 20.2kb.
• Определение понятия надежность изделия. Схема структуры надежности, свойства, параметры, 24.52kb.
• Построение таблиц истинности сложных высказываний, 104.54kb.
• Р п. Пушкино Советского р-на Саратовской области Учитель: Беляева Наталья Владимировна, 183.69kb.
• Udatex данной расчетной формулы обусловлено неоднократными обращениями и пожеланиями, 123.89kb.
• Лабораторная работа №2 формулы, имена, массивы. Формулы над массивами, 54.99kb.
• Календарно-тематическое планирование Календарно-тематическое планирование (математика), 232.23kb.
• Прикладная математика, 32.53kb.
• 41. Виды задач, решаемых через формулы предельной ошибки выборки Встатистических исследованиях, 122.07kb.

§ 2. Определение доказуемой (выводимой) формулы.

Следующим этапом в построении исчисления высказываний является выделение класса доказуемых (выводимых) формул.

Определение доказуемых формул имеет тот же характер , что и определение формулы.

Сначала определяются исходные доказуемые выводимые формулы (аксиомы), а затем определяются правила вывода, которые позволяют из имеющихся доказуемых формул получить новые доказуемые формулы.

Образование доказуемой формулы из исходных доказуемых формул путем применения правил вывода называется выводом (доказательством) данной формулы из аксиом.В основу исчисления высказываний могут быть положены различные системы аксиом, эквивалентные между собой в том смысле, что определяемый ими класс выводимых формул – один и тот же. Рассмотрим одну из них.

Система аксиом исчисления высказываний.

Система аксиом исчисления высказываний состоит из 11 аксиом (по сути представляющих собой тождественно истинные формулы алгебры логики), которые делятся на четыре группы.

Первая группа аксиом (содержащая только импликацию).

: . :.

Вторая группа аксиом (к импликации присоединилась конъюнкция):

: : . : .

Третья группа аксиом (к импликации присоединилась дизъюнкция):

: : : .

Четвертая группа аксиом (к импликации присоединилось отрицание):

: : :

1. Правила вывода.
   

1 Правило подстановки(ПП).

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

Операция замены в формуле А переменной х формулой В, носит название подстановки и символически записывается так:

или .

Уточним сформулированное правило:

а) если формула А есть собственно переменная х , то подстановка дает , очевидно, В;

б) если формула А есть переменная y , отличная от х ,то подстановка дает А;

в)подстановка формулы В вместо х в отрицание формулы А есть отрицание подстановки , т. е. подстановка дает;

г) если А₁ и А₂- некоторые формулы, то подстановка дает *, где через символ * обозначен любой из символов операций конъюнкция, дизъюнкция или отрицание

Если А- выводимая (доказуемая ) формула, то будем писать, как и ранее, ├А. Тогда ПП можно записать схематически следующим образом:

├А____ .

├

И читается эта запись так: “Если формула А выводима (доказуема), то выводима (доказуема) и формула .

2 Правило заключения (ПЗ).

Если формулы А и А→В выводимы (доказуемы) в исчислении высказываний, то формула В также выводима (доказуема). Схематическая запись этого правила имеет вид:

├А;├А→В (Modus ponens)

├В

Правомерность этого правила очевидна: если импликация и посылка истинны, то заключение в импликации может быть только истинным(см. таблицу истинности операции “импликация”).

2. Определение выводимой (доказуемой ) формулы.
   

а) Всякая аксиома является доказуемой формулой.

б)Формула, полученная из доказуемой формулы путем применения подстановки вместо переменной х произвольной формулы В, есть доказуемая формула.

в) Формула В, полученная из доказуемых формул А и путем применения ПЗ, есть доказуемая формула.

г) Никакая другая формула исчисления высказываний не считается доказуемой .

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