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


 

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

34113. Неспецифические аспекты психоаналитической терапии 77 KB
  В данной теме необходимо сформировать четкое представление о неспецифических формах взаимодействия аналитика и пациента. Данный раздел дает четкое представление о вспомогательных формах и методах во взаимодействии аналитика и пациента в рамках психоаналитической терапии. Если он будет это делать с неохотой аналитик может сказать что его интересуют факты. Пациента увязнувшего в неискренней похвале своих родителей можно спросить: Ваши родители действительно замечательные люди Расспрашивание для прояснения очевидности: Вместо того чтобы...
34114. Роль сновидений в психоаналитической терапии и техника работы с ними 73 KB
  Работа сновидения. Роль сновидения в работе психического аппарата. Развитие понимание сновидения и его роли в терапевтическом процессе от З. Классические подходы к пониманию сновидения его роль в общей структуре психики.
34115. Психоанализ и психоаналитическая терапия, основные принципы 67.5 KB
  Основные принципы классического психоанализа разработанного в наследие З. Основные отличия внешние – организационные и методологические основы клинического психоанализа психоаналитической терапии. Обратить особое внимание на основные принципы классического психоанализа разработанного З. Предлагаю обсудить вопрос который постоянно в той или иной форме возникает в ходе как профессиональных так и студенческих обсуждений отголоски этой дискуссии звучат и в раздающихся все чаще и чаще утверждениях о том что под брендом психоанализа скрывается...
34116. Показание и противопоказания психоаналитической терапии 62 KB
  Некоторые особенности российского пациента. Так же следует обратить особое внимание на особенности российского пациента и особенности построения терапии в зависимости от психологической конституции. Фрейд полагал что последние две силы связаны между собой и что существует некоторое соответствие внешней реальности и психологической предрасположенности самого пациента Тем самым предполагалось наличие патогенных компонентов в прошлом которые должны предопределять повышенную чувствительность по отношению к определенным обстоятельствам в...
34117. Сеттинг. Определение, взаимозависимость терапевтической задачи и сеттинга 46.5 KB
  Роль сеттинга в построение переходного пространства в рамках котрого происходит развертывание фантазий пациента и осуществляется работа с переносом и сопротивлением. Следует разобраться в ключевой роли сеттинга для формирования у пациента способности восприимать и продуцировать символическую организацию мира. Пациент лежит на кушетке или софе а психоаналитик сидит позади него оставаясь большей частью вне поля зрения пациента стараясь вмешиваться в процесс мышления пациента настолько мало насколько это возможно и не иначе как посредством...
34118. Структурные изменения, как основная цель психоанализа и психоаналитической терапии 62.5 KB
  Еще в 1894 году в работе “Невропсихозы защиты†он показывает что абсисивный симптом является компромиссом между неприемлемым сексуальным желанием защитой против удовлетворения этого желания и раскаянием или самонаказанием. Давайте попробуем понять фразу: Каждый симптом и каждая невротическая черта характера является компромиссным образованием И попробуенм в связи с этим ответить на два вопроса. Компромиссное образование является патологическим когда оно характеризуется любой комбинацией следующих черт: слишком большое ограничение...
34119. Терапевтические отношения. Форма и содержание 61 KB
  Именно в этом взаимодействие пациент продуцирует материал для анализа а аналитик создает условия для его интеграции в психики пациента что и будет являться основой для терапевтических изменений. Процесс ассимиляции связан с позитивной реакцией пациента на тот способ при помощи которого терапевт испоьзует полученный материал с тем как их усваивает Эго и с теми изменениями которые мы назвали “лечебными факторамиâ€. он представляет собой решающее звено между использованным способом действия терапевта и реальным эффектом для пациента...
34120. Ответы на экзаменационные вопросы Эго-психология 470.5 KB
  Положение ЭГОпсихологии в современной психоаналитической теории. ЭгоПсихология – направление в психоаналитической теории развитие которого как считалось началось с работы З. В какойто степени – это теория конкурирующая с теорией влечений и теорией объектных отношений хотя существует другая точка зрения определяющая Эгопсихологию как интегрирующую концепцию.
34121. Психоаналитическая терапия. Ответы на экзаменационные вопросы 325.5 KB
  Такой подход значительно сужает взгляд на проблему так как из вида упускается важнейший момент содержания терапевтического процесса которое образуется благодаря живому творческому взаимодействию его непосредственных участников – пациента и терапевта их влиянию друг на друга и на ход терапии в целом. Первоначально основатель психоанализа просто использует медицинскую однонаправленную модель в которой значение имеет только личность пациента катарсический метод. В дальнейшем обосновывая и развивая идею переноса Фрейд хотя и вводит в...