{ формальные языки - формальные исчисления - теоремы формального исчисления - выводимость в формальном исчислении - свойства выводимости из посылок - формальный язык исчисления высказываний - пропозициональные формулы - подстановки и подстановочные примеры - классическое исчисление высказываний - пример формального вывода - теорема дедукции - синтаксис и семантика - теорема о полноте - критика закона исключённого третьего - интуиционистское исчисление высказываний - неклассические логики - модели Крипке – семантика интуиционистских связок – семантика модальных связок }

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

k-местное правило вывода представляет собой (k+1)-местное отношение между формулами такое, что для любых формул 1, 2, …, k и формулы эффективно решается вопрос о том, находятся ли они в данном отношении. Если R является k-местным правилом вывода и формулы 1, 2, …, k и находятся в отношении R, то формула называется непосредственным следствием формул 1, 2, …, k по правилу R. Формальное исчисление считается заданным, если из множества всех формул выделено подмножество A – множество аксиом исчисления (множество аксиом может быть конечным или бесконечным, но для любой формулы должен эффективно решаться вопрос о том, является ли она аксиомой или нет), определены правила вывода R 1, R 2, …, R p (правило R i предполагается k i -местным, а натуральные числа k 1, k 2, …, k p могут быть произвольными).

Выводом в исчислении называется всякая последовательность формул 1, 2, …, n такая, что любая ее формула i есть либо аксиома исчисления, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода исчисления. Формула называется теоремой исчисления, если существует вывод в этом исчислении такой, в котором последней формулой является формула. Этот вывод называется выводом теоремы или доказательством теоремы. Теоремы исчисления, представляющие собой теоремы формального исчисления, не следует путать с теоремами о формальном исчислении, которые называют метатеоремами. Доказательства метатеорем представляют собой рассуждения на естественном языке, который в подобном контексте может быть назван метаязыком.

Пусть имеется формальное исчисление Y и некоторое множество формул. Выводом из множества в исчислении Y называется всякая последовательность формул такая, что любая ее формула представляет собой либо аксиому, либо элемент множества, либо непосредственное следствие некоторых предыдущих формул по одному из правил вывода исчисления Y. Элементы множества называют при этом гипотезами. Формула называется следствием множества формул в исчислении Y, если в этом исчислении существует вывод из множества гипотез, оканчивающийся формулой (то есть вывод формулы из множества гипотез ). В этом случае говорят, что в исчислении из множества посылок выводится формула, и пишут :. Если представляет собой конечное множество, состоящее из формул 1, 2, …, n, то вместо можно писать 1, 2, …, n. Запись означает выводимость в исчислении формулы из пустого множества посылок (в этом случае является теоремой исчисления). T T T T

Определение всякого формального языка начинается с описания алфавита. Алфавит формального языка логики высказываний состоит из четырёх пропозициональных связок (отрицание, конъюнкция, дизъюнкция, импликация): ¬,, v,, двух скобок (левой и правой): (, ), бесконечного числа пропозициональных букв. Пропозициональными буквами являются заглавные буквы латинского алфавита и такие же буквы с числовыми индексами, например, A, B, C, D, A 1, B 3, C 12, D 172. Из множества всех слов в этом алфавите выделяются правильно построенные слова, которые называются пропозициональными формулами или просто формулами. v

Определение пропозициональной формулы: 1. Пропозициональная буква есть формула. 2. Если φ и ψ формулы, то (¬φ), (φ ψ), (φ v ψ), (φψ) – тоже формулы. 3. Только те слова в алфавите формального языка логики высказываний являются формулами, для которых это следует из пунктов (1) и (2). v Внешние скобки в записи формул принято опускать, а кроме того часто опускают и те скобки, которые легко восстановить, учитывая приоритеты пропозициональных связок: ¬,, v, (сильнее всех связывает отрицание и слабее всех – импликация). Например: v (((A (¬B)) ((¬B) C)) (A C)) ((((A ((¬B) (¬B))) C) A) C) (A ¬B) (¬B C) (A C) A ¬B ¬B C A C v v v v

Говорят, что в формуле выполнена подстановка вместо переменной A формулы, если каждое вхождение переменной A в формулу заменено формулой. Пропозициональная формула называется подстановочным примером формулы, если она получена из формулы подстановкой вместо некоторых пропозициональных переменных каких-либо пропозициональных формул (говорят также, что эта формула является подстановкой в формулу ). Так например, формула имеет, среди прочих, такой подстановочный пример: (A ¬B) ˅ (¬B C) (A ¬(B C)) ˅ (¬(B C) (A ¬B) ˄ (¬B C)) Лемма: Всякий подстановочный пример тавтологии есть также тавтология.

Аксиомами классического исчисления высказываний являются следующие формулы и все их подстановочные примеры: A(BA), (A(BC))((AB)(AC)), A BA, A BB, A(BA B), AA v B, BA v B, (AC)((BC)(A v BC)), (AB)((A¬B)¬A), ¬¬AA. 1) 2) 3) 4) 5) 6) 7) 8) 9) 10) Единственным правилом вывода классического исчисления высказываний является правило modus ponens: _______ ( в соответствии с этим правилом из формул и непосредственно следует формула )., Эти формулы называют схемами аксиом v v v

Лемма: Формула является теоремой классического исчисления высказываний ( какова бы ни была формула ). Выводом формулы является следующая последовательность формул: 1) ((( ) ))((( ))( )) схема аксиом 2, 2) ((( ) )) схема аксиом 1, 3) (( ))( ) modus ponens: 1) и 2), 4)( ) схема аксиом 1, 5) modus ponens: 3) и 4) A(BA), (A(BC))((AB)(AC)). схема аксиом 1: схема аксиом 2:

Теорема дедукции :,. T T Пусть,, - произвольные формулы и - произвольное множество формул. Запись означает, что в классическом исчислении высказываний из множества формул выводится формула, а запись, означает, что U { }. T T Следствие 1:,. 1) гипотеза, 2) гипотеза, 3) гипотеза, 4) modus ponens: 1) и 3), 5) modus ponens: 2) и 4). Следствие 2: ( ),. 1) ( ) гипотеза, 2) гипотеза, 3) гипотеза, 4) modus ponens: 1) и 3), 5) modus ponens: 2) и 4). TT

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

Для классического исчисления высказываний справедливы обе формы теоремы о полноте Сильная форма теоремы о полноте : Для произвольных формулы и множества формул верно: (формула выводится из множества посылок в классическом исчислении высказываний тогда и только тогда, когда она является семантическим следствием этого множества посылок). T Слабая форма теоремы о полноте : Для произвольной формулы верно: (формула является теоремой классического исчисления высказываний тогда и только тогда, когда она является тавтологией). T

Между тем, некоторые законы классической логики могут быть подвергнуты критике, если требовать от рассуждений большей конструктивности. Часто встречаются доказательства существования, которые не позволяют построить те объекты, существование которых они устанавливают. Если признать бесполезными такие доказательства и пытаться их избежать, то придётся отказаться прежде всего от закона исключённого третьего: A v ¬ A. Пример: На самом-то деле верно это

Аксиомами интуиционистского исчисления высказываний являются следующие формулы и все их подстановочные примеры: 1) 2) 3) 4) 5) 6) 7) 8) 9) 10) Единственным правилом вывода интуиционистского исчисления высказываний является modus ponens. Таким образом, отличие от классического исчисления высказываний состоит только в том, что аксиома 10 (закон снятия двойного отрицания, который имеет следствием закон исключённого третьего) заменена более слабой. A(BA), (A(BC))((AB)(AC)), A BA, A BB, A(BA B), AA v B, BA v B, (AC)((BC)(A v BC)), (AB)((A¬B)¬A), ¬A(A B). v v v

В интуиционистском исчислении высказываний выводятся не все тавтологии. Множество теорем этого исчисления определяет интуиционистскую логику. Между интуиционистской и классической логиками имеется целый класс логик, называемых промежуточными или суперинтуиционистскими. Каждая из этих логик по-своему уточняет принципы конструктивных рассуждений. Языки интуиционистского и классического исчислений содержат одни и те же пропозициональные связки (они только понимаются несколько по-разному). Между тем, добавление к традиционным пропозициональным связкам новых связок приводит и к новым логикам. Логики с дополнительными связками возможность и необходимость называют модальным логиками. Рассматриваются также временные логики, логики знаний, логики доказуемости и другие. Вся эта совокупность разнообразных логик (каждая из которых может быть задана соответствующим исчислением или точно описанной семантикой) объединяется под общим названием неклассические логики.

Для описания семантики интуиционистской и модальных логик используются модели Крипке (название происходит от имени американского математика Саула Крипке). Модель Крипке образуют возможные миры, связанные между собой отношением достижимости. Так например, если считать, что сегодня мы живем в мире a, а завтра будем жить в мире b (при одном развитии событий) или в мире c (если события будут развиваться иначе), то возможные миры a, b, c окажутся связаны естественным отношением достижимости: из мира a достижимы миры b и c, но не наоборот. Этой простой модели Крипке из трех возможных миров отвечает диаграмма: В общем случае модель Крипке представляет собой произвольную совокупность возможных миров, связанных каким-либо отношением достижимости. Соответствующая диаграмма имеет вид направленного графа (если стрелок нет, то считается, что они смотрят снизу вверх). a b c

Пусть модель Крипке K имеет множество возможных миров M, связанных отношением достижимости ( a b означает, что из мира a достижим мир b ). Запись a φ означает, что в мире a истинна формула φ. Интуиционистское понимание пропозициональных связок таково: Формула истинна в модели Крипке, если она истинна в каждом мире этой модели. Формула принадлежит интуиционистской логике тогда и только тогда, когда она истинна в каждой модели Крипке. Формула A v ¬ A не принадлежит интуиционистской логике, так как она ложна в такой модели: a A v ¬ A b A c ¬A Модель Крипке также предполагает на- значение истинностных значений пере- менным в каждом мире, причём такое, что истинная переменная в более позднем мире не может стать ложной. A=1 A=0 a ¬φ x M ( a x x φ), a φ ψ a φ и a ψ, a φ v ψ a φ или a ψ, a φψ x M ( a x ( x φ x ψ) ). v

Формальный язык модальных логик содержит две дополнительные одноместные пропозициональные связки: необходимо возможно. Модели Крипке для модальных логик допускают произвольное назначение истинностных значений переменным в каждом мире (истинная переменная в более позднем мире может стать ложной). Связки необходимо и возможно понимаются таким образом: a A b c A=1 A=0 A=1 a φ x M ( a x x φ), a φ x M ( a x x φ). При этом общезначимыми являются следующие формулы: φ ¬ ¬ φ, φ ¬ ¬ φ.