Голованов М.И. Нестандартные логики. Реляционная семантика

Подождите немного. Документ загружается.

Федеральное агентство по образованию

Федеральное государственное образовательное учреждение

высшего профессионального образования

"Сибирский федеральный университет"

М.И. Голованов, В.Р. Кияткин, В.В. Рыбаков, Е.М. Юрасова

КУРС ЛЕКЦИЙ

Дисциплина "Нестандартные логики. Реляционная семантика "

(наименование дисциплины в соответствии с ФГОС ВПО и учебным планом)

Укрупненная группа 010000 - Физико-математические науки и

фундаментальная информатика

(номер и наименование укрупненной группы)

Направление 010300.68 Математика и компьютерные науки

(номер и наименование направления, специальности)

Институт Математики

Кафедра Алгебры и математической логики

Красноярск

2008

1 Лекция 1. Введение. Краткий экскурс в историю

логических исследований.

Слово "логика"и слова вида "...логия"происходят, согласно общепринятой точке зре-

ния, от греческого слова "logos слово, понятие, учение. В самом широком смысле

можно выделить три основных значения современного употребления этого слова:

1) наука о законах и формах мышления;

2) ход рассуждений, умозаключений;

3) разумность, внутренняя закономерность.

В свою очередь, из логики, как науки, выделяют формальную логику - науку,

изучающую формы мыслей и формы сочетаний их, отвлекаясь от конкретного со-

держания суждений, умозаключений, понятий, и математическую логику - раздел

математики, развиваемый математическими методами. В формальной логике пред-

полагается, что правильность рассуждения определяется только его формой и не

зависит от конкретного содержания входящих в него утверждений. Правильное рас-

суждение от истинных посылок всегда ведёт к истинному заключению. Математи-

ческая логика является разновидностью формальной логики и возникла на опреде-

лённом этапе развития формальной логики. Математическая логика играет важную

роль в вопросах обоснования математики; находит многочисленные приложения в

вопросах конструирования и применения электронных вычислительных машин, при

изучении свойств и построении языков программирования, в задачах информатики

и искусственного интеллекта.

К современному пониманию логики и её проблематики человечество пришло не

сразу. Начало логических исследований историки обычно относят к середине I ты-

сячелетия до нашей эры. Некоторые авторы выделяют два этапа развития логики:

традиционная формальная логика (с V в. до н.э. до середины XIX в.) и современная,

или символическая, логика (с середины XIX в. до наших дней). Иногда период раз-

вития традиционной формальной логики разделяют на два более коротких периода:

1) античная логика (V в. до н.э. - начало н.э.), вклад в развитие которой наиболее

часто связывают с именами таких греческих философов как Парменид (540-480 до

н.э.), Зенон Элейский (490-430 до н.э.), Сократ (469-399 до н.э.), Платон (427-347 до

н.э.), Аристотель (284-322 до н.э.), 2) схоластическая логика (начало н.э. - середина

XIX в.), в развитие которой внесли вклад аль-Фараби (870-950), Ибн-Сина (Авицен-

на; 980-1037), Михаил Пселл (1018-1078), Ф. Бэкон (1561-1626), Р.Декарт (1596-1650),

Г.В. Лейбниц (1646-1716), М.В. Ломоносов (1711-1765). В создание и развитие совре-

менной логики внесли вклад А. де Морган (1806-1871), Дж. Буль (1815-1864), Э.

Шрёдер (1841-1902), П.С. Порецкий (1846-1907), Г. Фреге (1848-1925), Дж. Пеано

(1858-1932), А. Уайтхед (1861-1947), Д. Гильберт (1862-1943), Б. Рассел(1872-1970).

Конечно, здесь перечислена лишь незначительная часть имён, с которыми связа-

но развитие логики. Но уже из этого перечисления мы видим сколько усилий было

затрачено на то, чтобы разобраться в том, как из одних утверждений вытекают

другие, как правильно рассуждать, какова в этом плане природа естественного че-

ловеческого языка.

Ещё Г.В. Лейбниц мечтал о том, чтобы рассуждения заменить вычислениями. Но

его метод математизации логики оказался неудачным. Современный математический

подход к логике, её алгебраизация, создание алгебры логики начинается с работ Дж.

Буля, У. Джевонса, Ч. Пирса, Э. Шрёдера, П.С. Порецкого. Но в алгебре логики

с математической точки зрения рассматриваются только способы конструирования

сложных придложений (высказываний) из простых и методы вычисления истинности

сложных предложений по заданным значениям истинности простых предложений.

Иными словами, изучается роль и свойства таких логических связок как "и", "или",

"если ..., то ...", "не". Строятся алгебры высказываний и с другими логическими

связками, в том числе и достаточно искусственными.

В конце XIX начале XX века возникает исчисление предикатов. В исчислении

предикатов строится математическая модель простого предложения, раскрывается

его структура. И одновременно, благодаря этому более внимательному рассмотре-

нию структуры простых предложений, в математическое изучение вводятся новые

логические связки - кванторы, т.е. такие логические связки (операторы) как "все",

"некоторые", "каждый", "существует". Создаётся формальный язык, на котором с

использованием современной математической символики можно записывать свой-

ства арифметических операций и отношений. Г. Фреге в своей работе "Исчисление

понятий"строит на новом уровне формализации и строгости исчисление высказыва-

ний и исчисление предикатов. Благодаря созданию исчисления предикатов начинают

развиваться теория доказательств (Д. Гильберт, П. Бернайс, К. Гёдель, Ж. Эрбран)

и теория моделей (Л. Левенгейм, Т. Скулем, К. Гёдель, А.И. Мальцев, А. Тарский).

Итогом этого развития стало создание в начале XX века классической математи-

ческой логики. В основе этой логики лежит предположение, что каждое высказыва-

ние либо истинно, либо ложно. То есть все возможные высказывания разбиваются на

два непересекающихся класса: класс истинных высказываний и класс ложных выска-

зываний. Основными принципами классической логики являются принцип непроти-

воречивости: высказывание и его отрицание не могут быть оба истинны, и принцип

исключённого третьего: истинно либо данное высказывание, либо его отрицание. Вто-

рой отличительной чертой классической логики является то, что в ней используются

только логические связки "и", "или", "если ..., то ...", "не", либо сводящиеся к ним,

и кванторы всеобщности и существования.

Однако в естественном языке встречаются и другие логические связки: "возмож-

но", "необходимо", "хорошо", "плохо", "запрещено", "разрешено"и т.д. С помощью

этих слов даётся оценка некоторому высказыванию. Высказывания, содержащие та-

кие оценки, называют модальными, не содержащие - немодальными. Рассмотрим

следующий набор предложений.

«Все студенты знают логику.»

«Необходимо, чтобы все студенты знали логику.»

«Хорошо, что все студенты знают логику.»

«Плохо, что все студенты знают логику.»

«Возможно, что все студенты знают логику.»

«Запрещено всем студентам знать логику.»

«Разрешено всем студентам знать логику.»

В первом предложении (немодальном) утверждается некоторый факт. В остальных

предложениях (модальных) выражается некоторое отношение к этому высказыва-

нию или его оценка.

Впервые модальность высказываний начал изучать Аристотель, рассматривав-

ший модальности "необходимо"и "возможно". В Древней Греции модальности рас-

сматривал также Диодор Крон в связи с введённой им временн´ой переменной. Ари-

стотель строил свою модальную силлогистику аналогично немодальной, исходя из

двузначной логики. Уже Аристотель писал о том, что закон исключённого третьего

не всегда применим. Кроме того, он вплотную подошёл к идее многозначной логики.

Я. Лукасевич, изучая аристотелевскую теорию случайных силлогизмов, отметил в

ней ряд серьёзных ошибок и показал, что модальная логика не может быть двузнач-

ной. В 1920г. Лукасевич впервые построил недвузначную логику. В этой логике было

три значения истинности: "ложно", "истинно", "нейтрально". В 1918г. К.И. Льюис

впервые предложил модальное исчисление на современном уровне формализации,

следуя логической системе Principia Mathematica Рассела и Уайтхеда.

В начале XX века в связи с обнаружением парадоксов классической теории мно-

жеств возник интуиционизм - концепция, направленная на преодоление кризиса в ос-

нованиях логики и математики. Основное требование интуиционизма - интуитивная

убедительность существования как исходных объектов теории, так и каждого ша-

га построения новых объектов. При этом понятие "интуитивной убедительности"не

уточняется. Следствием такой концепции явился отказ от использования актуаль-

ной бесконечности и закона исключённого третьего. Одним из первых формаль-

ных интуиционистских исчислений было интуиционистское исчисление предикатов

А.Гейтинга, предложенное им в 1930г. и в настоящее время наиболее широко извест-

ное.

Ещё одно направление критики классической логики - критика понимания импли-

кации и абсурда, заложенных в булевых алгебрах и в логической системе Principia

Mathematica. В классической логике высказывание "если А, то В"ложно только при

условии, что А истинно, а В ложно. Получается, что истинное высказывание сле-

дует из любого высказывания: "если крокодил голоден, то Луна - спутник Земли".

Во-вторых, из ложного высказывания следует всё что угодно: "если помидор не по-

мидор, то крокодил живёт на дереве". Оба высказывания противоречат нашей ин-

туиции. Обычно предполагается, что между посылкой и заключением существует

некоторая связь и поэтому высказывания такого рода воспринимаются как парадок-

сы. Указанные парадоксы были названы парадоксами материальной импликации и

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

ки построить исчисления аналогичные исчислению высказываний Рассела и Уайтхе-

да, но лишённые парадоксов материальной импликации. Одним из первых построил

логическую формальную систему, лишённую парадокса материальной импликации,

Льюис. Однако в его системе был найден другой парадокс, неприемлемый с точки

зрения нашей интуиции.

Нас далее больше будет интересовать другой аспект критики - критика принципа

"противоречие влечёт всё что угодно". Если принять этот принцип, то оказывает-

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

которой доказуемы все утверждения, будем называть тривиальной. Таким образом,

признавая принцип "противоречие влечёт всё что угодно", мы обязаны констатиро-

вать, что тривиальная теория - единственная, которая может содержать противоре-

чия. С другой стороны, даже в непротиворечивых теориях из указанного принципа

вытекает, что все противоречия эквивалентны друг другу, а это тоже не всегда при-

емлемо. Ещё в 1925 г. А.Н. Колмогоров отмечал, что принцип "противоречие влечёт

всё что угодно"появился только в формальном представлении классической логики и

в математической практике не используется. А.Н. Колмогоров и И. Иогансон пред-

ложили свои варианты формализации логики, в которых принцип "противоречие

влечёт всё что угодно"отсутствовал и многие другие формализации можно получать

из этих добавлением аксиом, новых логических связок или правил вывода.

Проиллюстрируем приведённые описания с помощью более строго заданных фор-

мальных систем логического вывода.

Классическое исчисление высказываний задаётся следующим множеством акси-

ом:

A1 (p

→ (p

→ p

))

A2 ((p

→ (p

→ p

)) → ((p

→ p

) → (p

→ p

)))

A3 ((p

∧ p

) → p

)

A4 (p

∧ (p

→ q))

A5 ((p

→ p

) → ((p

→ p

) → (p

→ (p

∧ p

))))

A6 (p

→ (p

∨ p

))

A7 (p

→ (p

∨ p

))

A8 ((p

→ p

) → ((p

→ p

) → ((p

∨ p

) → p

)))

A9 ((p

→ p

) → ((p

→ ¬p

) → ¬p

)

A10 ¬¬p → p

В качестве правил вывода возьмём два правила: правило подстановки и modus

ponens.

В приведённой логике доказуема формула p ∨ ¬p, т.е. справедлив закон исклю-

чённого третьего. Доказуема также формула (p ∧ ¬p) → q, т.е. справедлив принцип

"противоречие влечёт всё что угодно". Заменив аксиому A10 на другую аксиому: A11

(p → (¬p → q)), которая является другой формой принципа "противоречие влечёт

всё что угодно", получим исчисление, в котором закон исключённого третьего не

справедлив. Это исчисление называют интуиционистским исчислением высказыва-

ний, или логикой Гейтинга. Добавляя к аксиомам логики Гейтинга другие аксиомы,

мы будем получать новые логики, содержащие логику Гейтинга. Эти логики мы

будем называть суперинтуиционистскими. В частности, добавив к логике Гейтинга

формулу A10, мы вновь получим классическое исчисление высказываний. Можно

доказать, что все непротиворечивые суперинтуиционистские логики ямляются про-

межуточными между логикой Гейтинга и классическим исчислением высказываний.

Наконец, оставив только аксиомы A1-A8, получим исчисление, в котором ни одна

из формул p ∨ ¬p, (p ∧ ¬p) → q не доказуема. Множество доказуемых формул этого

исчисления будем называть позитивной логикой. Добавляя к этому исчислению в

качестве аксиом новые формулы, мы будем получать множества доказуемых фор-

мул (логики), которые а) могут содержаться в логике Гейтинга, б) могут содержать

логику Гейтинга, в) пересекаясь с логикой Гейтинга по некоторому собственному под-

множеству, содержат некоторые формулы, не доказуемые в логике Гейтинга. Далее

при изучении логик, содержащих связки только из совокупности ∧, ∨, →, neg, мы

будем рассматривать лишь расширения позитивной логики.

При изучении модальных логик мы ограничимся только одной связкой 2, кото-

рую будем называть "необходимо"и при этом в список аксиом всегда будем включать

аксиомы A1-A10 и дополнительную аксиому K: 2(p → q) → (2p → 2q). Для нас это

будет наименьшая модальная логики, её мы также будем обозначать символом K.

Правила вывода: modus ponens, правило подстановки и правило Гёделя 2p/p. Все

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

наименьшая нормальная модальная логика - это логика, полученная добавлением к

классическому исчислению высказываний связки "необходимо", аксиомы K и прави-

ла Гёделя.

Вопросы и задания.

1. Запишите аксиомы классического исчисления высказываний.

2. Запишите аксиомы позитивного исчисления высказываний.

3. Запишите аксиомы логики Гейтинга.

4. Сформулируйте парадоксы импликации.

5. Используя математическую символику сформулируйте принцип исключённого тре-

тьего и принцип "противоречие влечёт всё что угодно".

6. Опишите основные направления развития математической логики.

7. Сформулируйте правила вывода немодальных логик.

8. Сформулируйте правила вывода нормальных модальных логик.

9. Какие логики называются суперинтуиционистскими?

10. Является ли классическое исчисление высказываний суперинтуиционистской ло-

гикой?

11. Какие логики называются нормальными модальными логиками?

12. Справедливы ли принципы "исключённого третьего"и "противоречие влечёт всё

что угодно"в нормальных модальных логиках?

2 Лекция 2. Определение пропозициональной логи-

ки.

Далее дадим строгие формальные определения основным понятиям и терминам ма-

тематической логики, используемым в данном курсе, а также введём необходимые

обозначения. При этом будем предполагать, что нам вполне ясен смысл таких по-

нятий, как символ, конечная последовательность символов и, кроме того, извест-

ны основные понятия теории множеств, такие как операции над множествами и их

свойства, отношение, счётное множество, множество мощности континуум, булеан,

декартово произведение и некоторые другие.

Все определения и обозначения будут выбираться исходя из того, что в данном

курсе рассматриваются только пропозициональные логики.

Произвольные конечные последовательности символов некоторого множества A

будем называть словами в алфавите A. Множество всех слов в алфавите A будем

обозначать A

∗

Будем говорить, что задан формальный язык, если задано некоторое подмно-

жество F or ⊆ A

∗

. Элементы множества F or будем называть формулами. Обычно

множество F or задаётся с помощью некоторой индуктивной (порождающей) про-

цедуры. То есть вначале указываются наиболее простые формулы, а затем даются

правила, с помощью которых из простых формул строятся все остальные формулы.

Для наших целей удобно разбить множество A на два подмножества: бесконеч-

ное подмножество пропозициональных переменных и конечное подмножество логи-

ческих связок. Рассматривая наш формальный язык как способ описания естествен-

ного языка, мы будем предполагать, что пропозициональные переменные служат

для обозначения простых предложений естественного языка, а символы логических

связок обозначают логические связки естественного языка, с помощью которых из

простых предложений строятся сложные предложения естественного языка. В ка-

честве пропозициональных переменных мы будем использовать символы p

, где ин-

декс i - некоторое неотрицательное целое число. В некоторых случаях будем ис-

пользовать и другие символы с индексами или без них, если это не вызовет недора-

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

{∧, ∨, →, ¬, 2, 3, >, ⊥}. Их эквивалентами в русском языке будут: ∧ - "и", ∨ - "или",

→ - "если ..., то", ¬ - "не", 2 - "необходимо", 3 - "возможно". Символы > и ⊥ обо-

значают константы, соответственно, "истина"и "абсурд". Языки пропозициональных

логик будут различаться только набором символов логических связок. В случае необ-

ходимости к приведённому списку логических связок будем присоединять и другие

связки. Но при этом ограничимся только двуместными, одноместными связками и

константами.

Дадим определение формулы.

1. Пропозициональные переменные и константы (если они есть в языке) являются

формулами.

2. Если α и β формулы, † - одноместная логическая связка, ∗ - двуместная логи-

ческая связка, то †α и (α ∗ β) - формулы.

3. Только последовательности символов, удовлетворяющие первым двум услови-

ям, являются формулами.

Правилами вывода будем называть частичные отображения 2

F or

→ F or опреде-

лённого типа. Приведём определения.

Мы будем говорить, что применяется правило подстановки, если каждой фор-

муле ϕ(p

, . . . , p

) ∈ F or ставится в соответствие формула ϕ(ψ

, . . . , ψ

). При этом

подстановка p

→ ψ

, для i 6 k, p

→ p

, для i > k рассматривается как параметр

данного отображения.

Структурным n-посылочным правилом вывода будем называть частичное отоб-

ражение r : 2

F or

→ F or, которое задаётся некоторым фиксированным набором

формул α

, . . . , p

), . . . , α

, . . . , p

), β(p

, . . . , p

) и действует следующим обра-

зом: каждому подмножеству формул вида {α

(ψ

, . . . , ψ

), . . . , α

(ψ

, . . . , ψ

)}, сопо-

ставляет формулу β(ψ

, . . . , ψ

). Формулы ψ

, . . . , ψ

принимают все возможные зна-

чения во множестве F or. Такое правило вывода будем записывать следующим обра-

зом:

, . . . , p

), . . . , α

, . . . , p

)

β(p

, . . . , p

)

Пусть Γ ⊆ F or некоторое множество формул и Π некоторое множество правил.

Выводом из множества Γ с помощью правил Π будем называть конечную последо-

вательность формул, каждая из которых удовлетворяет одному из условий:

1) принадлежит множеству Γ,

2) получена из предыдущих формул последовательности по одному из правил выво-

да.

Если существует вывод ϕ

, . . . , ϕ

из Γ ⊆ F or с помощью правил Π, такой что

= α , то будем говорить, что формула α выводима из Γ с помощью правил Π и обо-

значать этот факт символом (Γ, Π) `

F or

α. Замыканием множества формул Γ ⊆ F or

относительно правил вывода Π будем называть множество Γ

F or,Π

всех формул, выво-

димых из Γ с помощью правил Π. Если Γ = Γ

F or,Π

, то будем говорить, что множество

Γ замкнуто в F or относительно Π. Если из контекста ясно о каком множестве фор-

мул F or или правил Π идёт речь, то соответствующий символ в обозначениях будем

опускать.

Пусть задано множество формул For и совокупность правил вывода Π. Есте-

ственно будем предполагать, что оба множества F or и Π не пустые. Логикой будем

называть подмножество L множества F or, замкнутое относительно заданного мно-

жества правил вывода Π. Тривиальный пример логики - множество F or всех формул,

поскольку множество F or замкнуто относительно любой совокупности правил вы-

вода. Отметим следующие факты, вытекающие из нашего определения логики: а)

если L логика относительно Π и Π

⊆ Π, то L логика относительно Π

, б) если L ло-

гика относительно Π

и относительно Π

, то L логика относительно Π

∪ Π

. Таким

образом, для каждой логики L существует наибольшее множество Π правил выво-

да, относительно которого она замкнута. Правила из множества Π будем называть

допустимыми правилами логики L. Дадим эквивалентное определение допустимого

правила. Правило r будем называть допустимым в логике L, если его применение к

любому множеству формул из L даёт формулу принадлежащую L.

Если зафиксированы множество формул Γ, множество правил Π и L = Γ

, то Γ

будем называть множеством аксиом логики L, Π - множеством постулируемых пра-

вил вывода. Если задана тройка множеств (F or, Γ, Π), то будем говорить, что задано

формальное логическое исчисление (формальная аксиоматическая система, дедук-

тивная система). Отметим, что исчисления (F or

, Γ, Π) и (F or

, Γ, Π) при F or

6= F or

могут задавать разные множества доказуемых формул, т.е. разные логики. С дру-

гой стороны, зафиксировав множества F or и Π, мы можем рассматривать семейство

подмножеств множества F or, замкнутых относительно Π. То есть пара множества

F or и Π задаёт семейство логик. Нетрудно видеть, что это семейство всегда будет

непустым. А если множество Π содержит правило подстановки, то все логики будут

содержать бесконечное множество формул.

Пример. Пусть F or

множество формул, содержащих только связку →; F or

множество формул, построенных с использованием двух связок: → и ∨. Далее по-

ложим Γ = {p → q}, Π содержит только правило подстановки. Тогда L

⊂ L

. Все

формулы логик L

и L

имеют вид α → β, но в L

формулы α и β кроме импликации

могут содержать и дизъюнкцию. То есть включение L

⊂ L

строгое.

Как правило, мы будем рассматривать логики, алфавит которых содержит им-

пликацию, а в числе правил вывода содержатся правило подстановки и правило

modus ponens: правило, которое каждой паре формул вида α, α → β сопоставля-

ет формулу β. По крайне мере, все формализации логических свойств естественного

языка удовлетворяют этому требованию.

В этих более традиционных случаях под логикой мы будем понимать множество

формул соответствующего формального языка, замкнутое относительно правил под-

становки и modus ponens.

Доказательством в исчислении (F or, Ax, Π) будем называть конечную последо-

вательность формул, каждая из которых удовлетворяет одному из условий:

1) является аксиомой,

2) получена из предыдущих формул последовательности по одному из правил выво-

да.

Формулу α будем называть доказуемой, если существует доказательство, послед-

ней формулой которого является α. В соответствии с определением совокупность

Ax всех доказуемых в аксиоматической системе (F or, Ax, Π) формул является логи-

кой. Обратно, если L - логика в языке, задающем множество F or, и Π совокупность

правил вывода, определяющая данную логику, то L совпадает с совокупностью всех

формул, доказуемых в аксиоматической системе (F or, L, Π).

Пусть Γ - некоторое множество формул. Выводом из множества гипотез Γ в

аксиоматической системе (F or, Ax, Π) будем называть конечную последовательность

формул, каждая из которых удовлетворяет одному из условий:

1) является аксиомой,

2) принадлежит множеству Γ,

3) получена из предыдущих формул последовательности по одному из правил Π.

2.1 Позитивная логика

В качестве первого содержательного примера приведём аксиоматическую систему

позитивной логики. Для этого определим:

1) язык, 2) множество аксиом, 3) правила вывода.

Алфавит состоит из счётного множества символов {p

|i ∈ N}, которые мы будем

называть пропозициональными переменными, и символов {∧, ∨, →}, которые назы-

ваются, соответственно, конъюнкция, дизъюнкция, импликация.

Понятие формулы определим по индукции: 1) пропозициональная переменная

является формулой, 2) если α и β – формулы, то (α ∧β), (α∨β), (α → β) – формулы,

3) только выражения, построенные по правилам 1) и 2) являются формулами, других

формул нет. Определённое таким образом множество формул будем обозначать F or

В качестве аксиом возьмём следующее множество формул:

A1 p

→ (p

→ p

)

A2 (p

→ (p

→ p

)) → ((p

→ p

) → (p

→ p

))

A3 (p

∧ p

) → p

A4 (p

∧ p

) → p

A5 (p

→ p

) → ((p

→ p

) → (p

→ (p

∧ p

)))

A6 p

→ (p

∨ p

)

A7 p

→ (p

∨ p

)

A8 (p

→ p

) → ((p

→ p

) → ((p

∨ p

) → p

))

В качестве правил вывода возьмём два правила: правило подстановки и modus

ponens.

Логику, задаваемую данным исчислением будем обозначать Lp.

Пусть ϕ

, . . . , ϕ

доказательство в исчислении (Ax, Π), в котором последовательно

используется вначале правило modus ponens, а затем к полученной формуле приме-

няется некоторая подстановка: α(p

, . . . , p

), α(p

, . . . , p

) → β(p

, . . . , p

), β(p

, . . . , p

β(ψ

, . . . , ψ

). Построим новое доказательство, в котором порядок применения пра-

вил обратный: α(p

, . . . , p

), α(p

, . . . , p

) → β(p

, . . . , p

), α(ψ

, . . . , ψ

), α(ψ

, . . . , ψ

) →

β(ψ

, . . . , ψ

), β(ψ

, . . . , ψ

). Аналогичные рассуждения можно провести и в том слу-

чае, когда вместо modus ponens используется любое другое структурное правило.

Поскольку в доказательстве ϕ

, . . . , ϕ

применяется только конечное число правил

вывода, применив к нему указанные преобразования, через конечное число шагов

получим доказательство, в котором вначале идут аксиомы и формулы, полученные

из них с помощью подстановок, а затем все последующие формулы доказательства

получаются применением только структурных правил вывода.

Используя данное наблюдение, мы можем определить позитивное исчисление несколь-

ко иначе.

Если α(p

, . . . , p

) формула и X

, . . . , X

некоторые символы, обозначающие про-

извольные формулы, то выражение α(X

, . . . , X

) будем называть схемой формулы.

Теперь позитивное исчисление определим следующим образом.

Схемы формул

(X → (Y → X))

((X → (Y → Z)) → ((X → Y ) → (X → Z)))

((X ∧ Y ) → X)

((X ∧ Y ) → Y )

((X → Y ) → ((X → Z) → (X → (Y ∧ Z))))

(X → (X ∨ Y ))

(Y → (X ∨ Y ))

((X → Z) → ((Y → Z) → ((X ∨ Y ) → Z)))

задают совокупность аксиом. Отметим, что теперь множество аксиом бесконечно,

поскольку каждая схема при замене символов X, Y, Z на всевозможные формулы

даёт бесконечное множество аксиом.

Правило вывода только одно - modus ponens. Доказательство является последова-

тельностью формул, каждая из которых либо частный случай одной из схем аксиом,

либо получена из предыдущих по правилу вывода. Нетрудно видеть, что этим спо-

собом мы задаём ту же совокупность доказуемых формул, что и предыдущим. То

есть ту же логику. Далее при определении новых логик, совокупность аксиом будем

задавать схемами аксиом.

Поскольку наличие большого количества индексов и скобок часто затрудняет чте-

ние и не всегда необходимо, то договоримся о некоторых отклонениях от выше опре-

делённых строгих правил записи формул в тех случаях, когда это не приводит к

большим затруднениям.

Во первых, вместо p

будем использовать p, q, r и некоторые другие буквы для

обозначения пропозициональных переменных, когда это удобно. Во вторых, всегда

будем опускать внешние скобки. В третьих, определим старшинство логических свя-

зок. В списке ∧, ∨, → раньше находится более старшая связка. При восстановлении

скобок первыми будем восстанавливать скобки, содержащие более старшие связки:

запись p ∧ q ∨ r → s является сокращением формулы (((p ∧ q) ∨ r) → s).

Приведём пример доказательства в Lp.

1 p → ((p → p) → p) A1

2 (p → ((p → p) → p)) → ((p → (p → p)) → (p → p)) A2

3 (p → (p → p)) → (p → p) по m.p. из 1,2

4 p → (p → p) A1

5 p → p по m.p. из 3,4

При поиске и построении доказательств в аксиоматических теориях часто бывает

удобна теорема дедукции. Отметим, что, во-первых, не во всех логиках справедлива

теорема дедукции, во-вторых, в различных логиках теорема дедукции имеет, вообще

говоря, различные формы. Однако, как будет видно из доказательства, приводимая

ниже теорема дедукции справедливо во всех логиках, содержащих схемы аксиом A1

и A2 и имеющих только одно правило вывода - modus ponens.

Теорема 2.1. Если Γ, α ` β, то Γ ` α → β

Вначале докажем другую, более конструктивную теорему, из которой данная тео-

рема получится в качестве следствия.

Теорема 2.2. Если ψ

, . . . , ψ

вывод из множества гипотез Γ∪{α}, то существует

вывод Γ ` α → ψ

, где 1 6 i 6 n.

Доказательство проведём индукцией по параметру i.

I. Пусть i = 1. То есть нужно доказать утверждение Γ ` α → ψ

. В соответствии

с определением вывода формула ψ

либо аксиома, либо принадлежит множеству

Γ ∪ {α}. Если ψ

аксиома, либо принадлежит множеству Γ, то последовательность

, ψ

→ (α → ψ

), α → ψ

является выводом формулы α → ψ

из множества гипотез

Γ. Если же ψ

= α, то утверждение Γ ` α → ψ

верно, поскольку формула α → α

доказуема.

II. Предположим утверждение Γ ` α → ψ

доказано для всех i < k и докажем его

для i = k. В соответствии с определением вывода справедливо одно из утверждений:

а) формула ψ

аксиома,

б) формула ψ

принадлежит множеству Γ ∪ {α},

в) формула ψ

получена из предыдущих по правилу modus ponens.