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

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

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

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

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

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

Следует различать 2 языка, которыми оперируют при рассмотрении логики и исчисления высказываний: объектный язык, метаязык.

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

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

Есть символы высказываний, значения истинности, которые используются для интерпретации, логические связи. Чаще всего будем пользоваться отрицанием, конъюнкцией, дизъюнкцией и тд

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

Определение формул будем давать рекурсивно.

1. Все символы простых высказываний являются формулами.

2. Если F и G – это формулы, то

3. других формул нет

 

В других исчислениях конъюнкцию и дизъюнкцию вводят явно.

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

Утверждение – пусть дана формула, в которую входят пропорциональные символы А1, А2, Аn. Причем формула является тавтологией, тогда при любой подстановки вместо символов А1, А2 Аn в формулу В1, В2 Вn получившаяся формула останется тавтологией, пусть у нее и изменится набор пропозициональных символов.

Формальная аксиоматическая теория (ФАТ)

ФАТ – теория, в которой

- задано некоторое множество символов, из которых строится выражение, то есть алфавит теории

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

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

- заданы правила вывода, позволяющие из одних формул получать другие

Выводом формулы В теории называется такая последовательность формул ФАТ А1, А2.., в которой последняя формула совпадает, получена правилом вывода из предыдущих формул. Формулой называется теорема, если для нее существует вывод в этой теории.

Относительно ФАТ изучаются следующие вопросы:

1. совпадает ли множество теорем данной теории с множеством тождественно истинных утверждений. Полнота в широком смысле

2. полнота в узком смысле – если добавить к множеству аксиом еще какую-то аксиому, увеличится ли множество теорем так, чтобы теория осталась непротиворечивой

3. вопрос о противоречивости – выводится ли в рамках данной теории одновременно формула А и ее отрицание ⌐А. Если да, теория противоречива.

4. разрешимость теории – теория разрешима, если существует алгоритм, который для произвольно взятой формулы теории определяет, является ли она теоремой этой теории. Иначе говоря, является ли множество теорем данной теории разрешимо.

5. независимость системы аксиом – выводится ли аксиомы друг из друга, если да – от некоторых аксиом можно избавиться, а множество теорем останется неизменным

Пусть дано некоторое множество формул Г, тогда формула G выводима из множества гипотез Гамма.

Если есть такая последовательность гипотез А1, А2 Аn(=G), которая последняя формула совпадает с G, а все остальные являются либо аксиомами, либо принадлежат множеству Гамма, либо получены из предыдущих путем применения правила вывода. Если множество Гамма пусто, то формула G является теоремой. Свойство выводимости:

Если известно, что из Гамма выводится формула G и для любой формулы бета, принадлежащей Гамма существует вывод из множества формул, то G выводится из множества Ф

Если множество Гамма бесконечно

Логическое следование

Логическое следование можно определить двумя внешне непохожими, но фактически эквивалентными способами. Первый способ основан на семантике, второй – на синтаксисе.

Формула G логически следует из множества формул Гамма, если для каждой интерпретации, при которой все формулы из Гамма истинны, формула G тоже истинна. Также говорят, что формула G является логическим следствием множества формул Гамма, или множество формул Гамма влечет собой формулу G. Из Гамма следует G т и т т, когда формулы Гамма и отрицание G невыполнимы одновременно.

Семантика ФАТ в логике высказывания определяется с помощью произвольной функции е, сопоставляющей всем пропорциональным символам S одно из значений истина или ложь, причем это отображение распространяется на связки символом следующим образом

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

Секренция – выражение вида

где F формула, G конечное множество формул.

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

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

косвенное правило.

Производные правила можно сформулировать на основе дерева доказательств. Дерево доказательства определяется рекурсивно.

1) деревом доказательства является пустое дерево доказательства, состоящее только из корня, то есть аксиоматической секренции. Пусть Т1, Т2, Тк деревья доказательства с корнями R1,R2,Rк, тогда Т1..Тк под чертой S, дерево доказательства если S может быть получено из R1..Rк с помощью одного из правила вывода.

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

Для высказываний рассмотрим:

- Рис 15 – это правило называется modus Panendo Poneus (MP)

Если из P следует Q и Р истинно, то и Q истинно

- рис 16. если из P следует Q и оно ложно, то и Q ложно. Modus tollendo Tollens

- рис 17 если П и Кю одновременно ложны, при этом П истинно, то Кю ложь – исключающее или

- рис 18 – включающее или. Если либо П, либо Кю является истинным и П не истинно, то Кю истинно.

(1 Modus Ponendo Ponens: «Если истинна импликация А—>В и А истинно, то B истинно».

2 Modus Tollendo Tollens: «Если истинна импликация А—>В и В ложно, то А ложно».

3 Modus Ponendo Tollens: «Если А истинно и конъюнкция АВ имеет результатом ложь, то В ложно».

4 Modus Tollendo Ponens: «Если А ложно и дизъюнкция AB истинна, то В является истиной».)

 

⇐ Предыдущая12345Следующая ⇒

Поделиться:

Воспользуйтесь поиском по сайту: