48071

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

Конспект

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

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

Русский

2013-12-06

172 KB

10 чел.

В.В. Гуренко

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

§ 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-значных (бесконечнозначных) логических систем и алгебр в качестве их моделей. Предложил собственный язык формализации логических выражений (т.н. «польская запись»).


 

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

36477. Древние Шумеры 30.5 KB
  долина рек Тигр и Ефрат Неблагоприятные условия сухой климат мало полезных ископаемых Тростник и рыба самые доступные ресурсы Население сосредоточено в предморье и не углублялось во влажные равнины Увеличение численности населения перенаселение Технологии Сельскохозяйственные культуры ячмень эммера Одомашнен ряд животных быки овцы козы свиньи и ослы Примитивные технологии обработки меди Колесо Первые постройки из сырого глиняного кирпича Шумеры пытаются вести с х на новых землях строят системы очищения почвы....
36478. Понятия «цивилизация». Подходы к толкованию термина. Цивилизационная теория 93.5 KB
  Понятия цивилизация впервые употребил Виктор Мирабо в 1757 году в значении общего уровня культурного развития. Среди деятелей просвещения цивилизация ассоциировалась с концепцией прогресса стала идеалом интеллектуального и социального развития человечества. Отсюда ясно что цивилизация носила отрицательный оттенок.
36479. Структура цивилизация, ее основные элементы 73 KB
  технологический способ производства: орудия труда источники энергии предметы труда природные ресурсы технологии организация производства в плане технологий экономический способ производства структура воспроизводства обмен распределение экономическое управление социальнополитические отношения: социальные отношения национальные отношения политические отношения государственные отношения правовые духовный мир: наука культура образование мораль идеология или религия Все элементы цивилизационной...
36480. Динамика развития цивилизации, этапы ее развития на историческом примере 46.5 KB
  В истории человечества выделяют следующие глобальные цивилизации: неолитическую раннеклассовую античную средневековую индустриальную и наконец постиндустриальную цивилизации. Условия формирования античной цивилизации. Безусловно их наследие оказало определенное влияние на становление античной цивилизации тем не менее античный период в истории человечества дал рождение совершенно новым экономическим политическим и духовным институтам.
36481. Механизм смены цивилизации. Переход между цивилизациями 35 KB
  Механизм смены цивилизации Основные причины: внутренние противоречия в которых центральное место занимают потребности человека. Для производства материальных и духовных благ цивилизации приходится привлекать новые ресурсы средства труда источники энергии реализовывать новые экономические и политические схемы подавлять социальные конфликты и предлагать новый духовный продукт. Попытки удовлетворения потребностей нарушают сложившийся в цивилизации баланс и она не может удовлетворить потребности всех. Духовный мир чутко реагирует на эти...
36482. Переходный этап в развитии цивилизации на историческом примере перехода от раннеклассовой к античной 27.5 KB
  Переход между цивилизациями происходит в четыре этапа: латентный этап обвального хаоса патовая ситуация завершающий этап. На первом этапе происходит падение эффективности старого общества: возникают социальные противоречия разногласия между управленцами и исполнителями экономической функции и непрерывные войны которые с одной стороны истощали материальные ресурсы а с другой обогащали правящую элиту. Происходит возращение к родоплеменному типу отношений формирование общинного строя предполагающего управление общества вождем советом...
36483. Основные особенности и достижения неолитической цивилизации 32 KB
  Начало неолитической цивилизации связывают с неолитической революцией. Достижения неолитической цивилизации: Возникла первая форма собственности общинная собственность на землю; Появляется объекты собственности сельскохозяйственные земли пастбища охотничьи и рыболовные угодья; Возникает частная собственность при необходимости защита частной собственности; Формирование первых политических институтов крупные межобщинные объединения; Духовный мир выходит на новый уровень возрастает уровень познания окружающего мира;...
36484. Основные особенности и достижения раннеклассовой цивилизации 32.5 KB
  Если в неолитическую эпоху основные изменения были связаны с технологиями то для раннеклассовой цивилизации характеры значительные изменения в экономическом способе производства и социальнополитические отношения. Происходит городская революция создания центров локальной цивилизации в сети крупных городов. Города не только служили центрами ремесла но и позволяли сконцентрировать материальные и духовные ресурсы цивилизации для ее развития.
36485. Цивилизации Древнего Египта: развитие и основные достижения 38.5 KB
  Экономика Древнего Египта в основном базировалась на земледелии. Хорошие плодородные почвы Египта и мастерство земледельцев позволяли не только обеспечивать сельское население продуктами питания но и создавать избыточный продукт. Еще в период Древнего царства сложились торговые пути из Египта в Нубию на Синай в Палестину и Сирию.