48071

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

Конспект

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

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

Русский

2013-12-06

172 KB

9 чел.

В.В. Гуренко

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

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


 

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

81415. Социологическое знание в социальной работе. Категории индивид, личность, группа, общность, общество. Понятия «социальный факт», «социальная реальность» и «социальное действие» 37.24 KB
  Социологические исследования в социальной работе выполняют многообразные функции. Социологические методы и техника изучения проблем социальной работы выполняют двоякую функцию расширения и углубления социологического и социального образования в целом и получения важной первичной социальной информации без чего невозможны анализ практической социальной работы накопление опыта его обобщения и в целом повышение ее эффективности. Влияние социологии на социальную работу: использование результатов изучения социологами социальной структуры...
81416. Социологические проблемы социального взаимодействия в социальной работе. Понятия: социальная структура, социальные изменения, конфликты интересов основных социальных групп 37.54 KB
  Понятия: социальная структура социальные изменения конфликты интересов основных социальных групп. Социальные изменения представляют собой смену состояний свойств и связей социальных систем. В соответствии со строением и главной характеристикой любой системы можно выделить следующие виды изменений вообще и социальных изменений в частности: Содержательные изменения Под содержанием в науке понимают совокупность элементов системы поэтому здесь речь идет об изменении элементов системы их возникновении исчезновении или изменении ими своих...
81417. Социология в теории социальной работы наука об обществе как целостной системе и об отдельных социаль 34.67 KB
  Социология в теории социальной работы наука об обществе как целостной системе и об отдельных социальных институтах рассматриваемых в их связи с общественным целым. Влияние социологии на социальную работу: использование результатов изучения социологами социальной структуры общества и других фундаментальных проблем социологического знания и практической деятельности применение этих данных в подготовке и переподготовке социальных работников анализ самой социальной работы сточки зрения участия в ней разных групп социальных работников...
81418. Социологические парадигмы в анализе социальной работы 38.2 KB
  Парадигма социальных фактов связана с именем Э. Парадигма понимания или социологии действия связана с именами М. Парадигма социального поведения представлена социальным бихевиоризмом Б. Парадигма социальноисторического детерминизма связана с именами К.
81419. Структурно-функциональные социологические парадигмы в анализе социальной работы 35.85 KB
  Основное внимание социологов данного направления сосредотачивается на исследовании того какой вклад различные части общества структуры вносят в интеграцию целостного социальной системы. Конфликтная модель общества Р. В результате обострение противоречий внутри общества может быть обусловлено рядом причин: диспропорция в распределении власти и отсутствие свободных каналов перераспределения власти. Суть его концепции в следующем: ав каждый момент общество переживает социальный конфликт социальный конфликт вездесущ; б любое общество...
81420. Парадигмы социального поведения при анализе социальной работы 39.02 KB
  Для социального бихевиоризма Скиннера сформировавшегося под влиянием воззрений представителей ортодоксального неопозитивизма и отчасти утилитаризма характерно отождествление механизмов коллективного поведения животных и людей которое рассматривается...
81421. Основные социологические теории и возможность их применения для анализа социальной работы 37.06 KB
  Понимание познание социального действия через его субъективный смысл который вкладывает в данное действие сам субъект. Суть использования понимания состоит в том чтобы поставить себя в положение других людей для того чтобы увидеть какое именно значение они придают своим действиям или каким целям по своему убеждению служат. Исследование значений человеческих поступков это в какойто степени просто развитие наших повседневных попыток понять действия множества различных окружающих нас людей. Действие которое соотносится с действиями...
81422. Конформация пептидных цепей в белках (вторичная и третичная структуры). Слабые внутримолекулярные взаимодействия в пептидной цепи; дисульфидные связи 108.54 KB
  Слабые внутримолекулярные взаимодействия в пептидной цепи; дисульфидные связи. βлисты складчатые слои несколько зигзагообразных полипептидных цепей в которых водородные связи образуются между относительно удалёнными друг от друга 0347 нм на аминокислотный остаток в первичной структуре аминокислотами или разными цепями белка а не близко расположенными как имеет место в αспирали. Стабильность вторичной структуры обеспечивается в основном водородными связями определенный вклад вносят и главновалентные связи пептидные и...
81423. Основы функционирования белков. Активный центр белков и его специфическое взаимодействие с лигандом как основа биологической функции всех белков. Комплементарность взаимодействия молекул белка с лигандом. Обратимость связывания 102.95 KB
  Активный центр белков и его специфическое взаимодействие с лигандом как основа биологической функции всех белков. Каждый индивидуальный белок имеющий уникальную первичную структуру и конформацию обладает и уникальной функцией отличающей его от остальных белков. Набор индивидуальных белков выполняет в клетке множество разнообразных и сложных функций.