48071

Формальные теории математической логики

Конспект

Математика и математический анализ

Формальные теории. Задано А альфа множество символов теории алфавит Т. Задано В Ф бета множество аксиом теории. Собственные нелогические аксиомы определяют специфику конкретной теории.

Русский

2013-12-06

172 KB

7 чел.

В.В. Гуренко

Математическая логика и теория алгоритмов. Курс лекций

§ 6. Формальные теории.

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

Формальная теория Т [тау] считается определенной при выполнении условий 1 – 4.

1. Задано А [альфа] – множество символов теории (алфавит Т).

2. Задано Ф [фи] – множество слов в алфавите А (формулы Т).

3. Задано В Ф [бета] – множество аксиом теории. Если В  , Т называют аксиоматической теорией.

4. Задано {R1, R2, … Rn}, n < , – множество отношений между формулами Ф (правила вывода).

Пусть {ф1, ф2, …, фj} Ф и {ф1, ф2, …, фj} | Ri (находятся в отношении Ri). Пусть А  Ф. Если {ф1, ф2, …, фj} А | Ri, то А – непосредственное следствие ф1, ф2, …, фj по Ri.

Примечания.

1. Алфавит Аконечный или бесконечный. Возможны индексы.

2. Ф обычно определяется индуктивно (порождающей формальной грамматикой).

3. В – конечное или бесконечное.

При |В| = :


Виды аксиом:

Логические аксиомы являются общими для некоторого класса формальных теорий.

Собственные (нелогические) аксиомы определяют специфику конкретной теории.

Понятие выводимости. Пусть А1, А2, …, Аn, G – формулы теории Т:

1, А2, …, Аn, G} Ф.

Если существует правило вывода R такое, что

1, А2, …, Аn, G} | R,

то говорят, что G непосредственно выводима из формул А1, А2, …, Аn по правилу R.

При этом формулы А1, А2, …, Аn называют посылками вывода, а формулу Gзаключением.  Записывают:


Понятие вывода.  Пусть {А1, А2, …, Аn} Ф,  G  Ф.  Выводом формулы G из формул А1, А2, …, Аn в формальной теории Т называют последовательность формул

Е1, Е2, …, Еk,  

причем  а) Еk = G;

б) для всякой Еi (i < k) верно:

либо Еi  В i – аксиома],

либо Еi = Аj,  i – посылка вывода],

либо  i непосредственно выводима из предыдущих формул].

Если в теории Т существует вывод формулы G из формул А1, А2, …, Аn, этот факт записывают следующим образом:

Формулы А1, А2, …, Аn в таком случае называют гипотезами вывода, а запись читают: «Формула G выводится в формальной теории Т из гипотез А1, А2, …, Аn».

Если гипотезы отсутствуют и G выводится только из аксиом теории, то G называют теоремой теории Т и записывают:

 

В таком случае знак  читают «является теоремой теории Т». Индекс, указывающий теорию, можно опустить, если она явно подразумевается.

Заметим: формула G является теоремой формальной теории Т тогда и только тогда, когда в данной теории существует логический вывод, последняя формула которого – формула G.


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

1. Если  Г Δ  и  Г     А,  то  Δ      А,   где А – формула, Г  Ф, Δ  Ф.

То  же  иначе:

Если Г      А и Г  Ф, Δ  Ф, то  Г, Δ     А, т.е. добавление гипотез не нарушает выводимости.

2. Если  Δ      А  и  для всякой формулы В Δ  Г      В,  то Г      А.

Если А выводима из множества гипотез Δ и любая формула, содержащаяся в Δ, вводима из множества гипотез Г, то А выводима из Г.

Непротиворечивость формальной теории.

Формальная теория Т называется семантически непротиворечивой, если ни одна теорема теории не является противоречием.

Формальная теория Т называется формально непротиворечивой, если в ней невозможна одновременная выводимость формул G и G.


Th. Формальная теория Т формально непротиворечива тогда и только тогда, когда она семантически непротиворечива.

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

Замечание. Два понятия непротиворечивости и Th. в действительности являются технически сложно доказуемыми метатеоремами теории Т.

Разрешимость формальной теории.

Формальная теория Т называется разрешимой, если существует алгоритм, позволяющий для любой формулы G определить, является ли G теоремой теории Т.

Формальная теория Т называется полуразрешимой, если существует алгоритм, для любой формулы G теории дающий ответ «да», если G является теоремой Т, либо не дающий никакого ответа в противном случае (т.е. применимость алгоритма ограничена не всеми формулами теории).


§ 7. Исчисление высказываний методом формальных теорий.

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

Рассмотрим наиболее лаконичную, наглядную и хорошо изученную теорию.

Формальная теория L для исчисления высказываний. Предложена Я. Лукасевичем*).

Т (L):

1. А:

1) пропозициональные буквы (переменные) А, В,… а, b,… А1, Вj,… ak, bi,…;

2) логические связки ,  ;

3) скобки ( ), [ ], { }.

2. Ф:

1) все пропозициональные переменные суть формулы;

2) если А, В – формулы, то А  и  А  В  – формулы.

3. В:

Каковы бы ни были формулы А, В и С,  В = [А1, А2, А3]:

A1:  A (B A)

A2:  (A (B C)) ((A B) (A C))

A3:  (B  A) ((B A) B)

4. R: единственное – Modus ponens (лат.).

Если  А,  A  B,  то  В. Запись:

Правило МР позволяет отделить следствие от истинного условного высказывания при утверждении его основания. Логика МРот утверждения основания к утверждению следствия.   Обратное неверно!


Примечания к введению теории L.

1). |B| = , т.к. А, В, С – любые формулы.  А1, А2, А3 – схемы аксиом.

2). МР можно рассматривать как схему, задающую множество правил. Пример одного из классических правил формальной логики:

Modus tollens (Modus tollendo tollens, лат.),

«путь исключения исключений»:

3). МР сохраняет тавтологичность формул теории.

4). Логические связки, не входящие в описание теории, вводятся следующими определениями:

  •  A & B  – это то же, что и  (A B);
  •  A  B  – это то же, что и  A  B;
  •  A  B  – это то же, что и  (A  B) & (B  A) =  ((A  B)  (B  A)).

Исчисление высказываний путем построения логического вывода средствами некоторой формальной теории (в частности, теории L) составляет содержание метода формальных теорий.

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


Пример.  B  A.

1). А гипотеза или: 1). A  B гипотеза

2). A (B A) A1 2). B  A 1) {A // B, B // A}   ■

3). B  A 1), 2), МР   ■

Замечания. 1. Каждая доказанная теорема теории может быть использована в дальнейшем для построения логического вывода как гипотеза, т.к. формула доказанной теоремы  – неизменно истинное высказывание (тавтология).

2. Множество теорем теории L бесконечно.

В теории L импликация тесно связана с выводимостью:


Th. дедукции (Эрбана).

Если Г – множество гипотез, А, В – формулы и Г, А       В, то  Г      A  B.

Доказательство. Пусть Е1, Е2, …, Еn – вывод В из Г, А. При этом Еn = В. Покажем индукцией по i, что  Г      A  Еi  Тем самым теорема будет доказана.

I. База индукции: i = 1. Надо показать, что Г      A  Е1. Возможны три случая.

1). Е1 – аксиома. Предложим вывод:

Е1 гипотеза

Е1  (A  Е1) A1 1//A, A//B}

A  Е1 1), 2), МР

Имеем:       A  Е1. На основании свойства № 1 выводимости: Г      A  Е1.

2). Е1  Г. Вывод аналогичен случаю 1).

3). Е1 = А. Несложно показать, что     A  А. Используем замену {Е1/А} для 2-го вхождения А.  Получим:   А Е1 и далее  Г     A  Е1.

Во всех трех случаях показано, что Г     A  Е1. База индукции доказана.

II. Положим, что Г     A  Еi для всех i < k. Рассмотрим формулу Еk. Возможны четыре случая:  1) Еk – аксиома;  2) Еk  Г;  3) Еk = А;  4) Еk получена выводом (по МР) из Еi и Еj, причем i, j < k  и  Еj = Еi  Еk  (!).

Случаи 1) … 3) аналогичны рассмотренным выше, имеем  Г     A  Еk.

В случае 4) можно утверждать:

i-й шаг.    Г     A  Еi по индукции

j-й шаг.    Г     A i  Еk), т.к. в конечном итоге Еj следует из А.

Применим аксиому А2 и построим вывод:

n).  (A (Еi  Еk)) ((A  Еi) (A  Еk)) А2 {Еi //B, Еk //C}

n+1).  (A  Еi) (A  Еk) j), n), MP

n+2).  A  Еk i), n+1), MP 

Итак, во всех четырех случаях:  Г     A  Еk  для любого k  и, в частности, для k = n.

Но т.к. Еn = В, получаем:

 Г      A  В. ■


Истинна теорема, обратная теореме дедукции:

Th. Если  Г     A  В,  то  Г, А      В.

Доказательство. Пусть вывод  Г     A  В состоит из n формул. Рассмотрим такое продолжение вывода:

n). A  В имеем в результате n-го шага

n+1). A гипотеза

n+2). B n+1), n), MP

Таким образом, Г, А      В. ■

Следствия из Th. дедукции.

Сл. 1. Если А     В, то      A  В.

Доказательство. Т.к. по условию Г = , по Th. дедукции имеем:

если , А     В, то       A  В. ■

Обратное также очевидно.

Сл. 2 (правило транзитивности). Из формул A  В, В С выводится формула A  С:

A  В, В С     A  С.

Доказательство. Построим логический вывод:

1). A  В гипотеза

2). В С гипотеза

3). А гипотеза

4). В 3), 1), МР

5). С 4), 2), МР

6). A  В, В С, А      С вывод 1)…5)

7). A  В, В С      A  С. 6), Th. дедукции   


Сл. 3 (правило сечения). Из формул A  (B  С), В выводится формула A  С:

A  (B  С), В     A  С.

Доказательство: построением логического вывода.

1). A  С) гипотеза подумайте, как получить?

2). А гипотеза

3). В С 2), 1), МР

4). В гипотеза

5). С 4), 3), МР

6). A  С), В, А      С вывод 1)…5)

7). A  С), В      A  С. 6), Th. дедукции   

Некоторые заключительные замечания относительно введенной теории L.

1. Th. (о полноте). Формула G является теоремой теории L тогда и только тогда, когда G – тавтология.

Из Th. о полноте следует, что всякая теорема L-исчисления является тавтологией и всякая тавтология – теоремой теории L. Иначе говоря, множество теорем теории L совпадает с  множеством тавтологий.

2. Формальная теория L является семантически непротиворечивой, т.к. никакая теорема теории L не является противоречием.

3. Формальная теория L является формально непротиворечивой, т.к. в ней не существует такой формулы G, чтобы формулы G и G были одновременно теоремами данной теории.

Пояснение. Согласно Th. о полноте, каждая теорема теории L – тавтология. Отрицание тавтологии, во всяком случае, не есть тавтология. Следовательно, ни для какой формулы теории L  невозможно, чтобы формула и ее отрицание одновременно были бы теоремами теории L.


§ 8. Примеры других аксиоматизаций логики высказываний.

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

. Авторы: Дэвид Гильберт (1862–1943), Вильгельм Аккерман (1896–1962).

Особенности:

  •  Логические связки: , (для импликации используется тождество: A  В  А  В).
  •  Аксиомы: А  А А;  А А В;  А В В А;   С) ( А В А С).
  •  Правило вывода: МР.

Предложена в 1938 г.

. Автор: Джон Беркли Россер (1907–1989).

Особенности:

  •  Логические связки: &,  (для импликации используется тождество: A  В  (A & В).
  •  Аксиомы: А А & A;  A & B А;  (A  В) ((В & C)  (C & A)).
  •  Правило вывода: МР.

Предложена в 1953 г.

. Автор: Стефан Клини (1909–1994).

Особенности:

  •  Логические связки:  , &, , .
  •  Аксиомы: A (В  А);  A & В  A;  A & В  B;  A (A B);  B (A B);  A  А; … (всего 10 аксиом).
  •  Правило вывода: МР.

Предложена в 1952 г.

Известны также формальные аксиоматические теории: иная Д. Гильберта (11 аксиом, первые две совпадают с А1 и А2 теории L, правило вывода – МР), Г. Фреге, П.С. Новикова и другие.

_________________

*) Лукасевич Ян (Łukasiewicz Jan, 1878–1956) – польский математик и логик. Работы в области проблем индукции и причинности, логических основ теории вероятностей. Автор первой системы многозначной (трехзначной) логики, системы модальной логики, четырехзначной логики и далее – n-значных (бесконечнозначных) логических систем и алгебр в качестве их моделей. Предложил собственный язык формализации логических выражений (т.н. «польская запись»).


 

А также другие работы, которые могут Вас заинтересовать

41068. Речове забезпечення військової частини у воєнний час 84 KB
  Воєнна історія показує нам багато прикладів впливу незадовільного забезпечення речовим майном на хід бойових дій. Непродумана конструкція, погана якість та демаскуючий колір обмундирування неодноразово ставали причинами значних бойових втрат особового складу.
41069. Бойова та мобілізаційна робота речової служби військової частини 122.5 KB
  Бойова та мобілізаційна робота речової служби військової частини. Бойова та мобілізаційна готовність речової служби військової частини. Навчальний час – 2 години Для студентів Навчальна та виховна мета: Ознайомити студентів з порядком проведення заходів по відмобілізуванню та приведенню в бойову готовність речової служби військової частини. Показати важливість своєчасного та повного виконання заходів по відмобілізуванню речової служби для...
41070. Методична підготовка 63.5 KB
  €œОрганізація та планування підготовки молодших фахівців речової служби€ Для студентів спеціальності €œОрганізація об’єднаного забезпечення в наземних військах та авіаціїâ€ Навчальна та виховна мета: Ознайомити студентів зі значенням та завданнями спеціальної підготовки молодших фахівців речової служби. Значення та завдання спеціальної підготовки...
41074. Права та обов’язки замовників екологічної експертизи 67.5 KB
  Права та обов’язки замовників екологічної експертизи Порядок проведення екологічної експертизи Фінансування екологічної експертизи Міжнародне співтовариство в галузі екологічної експертизи
41075. ОСНОВНІ ЕЛЕМЕНТИ ЕКОЛОГІЧНОЇ ЕКСПЕРТИЗИ 83 KB
  Загальна схема процесу екологічної експертизи Елементи процесу екологічної експертизи: доля громадськості і розгляд альтернатив Загальна схема процесу екологічної експертизи У цій лекції ми спробуємо розглянути основні елементи екологічної експертизи проектів ЕЕП.
41076. ЕКОЛОГІЧНА ЕКСПЕРТИЗА: ОСНОВНІ ПОНЯТТЯ І ПРИНЦИПИ 91.5 KB
  Поняття екологічної експертизи Загальні принципи екологічної експертизи та їх зв'язок з принципами сталого розвитку Предмет екологічної експертизи Учасники процесу екологічної експертизи