Загрузка...

Математическая логика. Раздел 2. Аксиоматические теории.


Раздел 2. Аксиоматические теории

1.2. Формальные аксиоматические теории

Формальная аксиоматическая теория Т считается заданной, если :
1) задано некоторое счётное конечное множество символов теории Т (алфавит). Конечные последовательности из символов Т называются выражениями теории Т.

2) существует подмножество выражений Т, которые будем называть формулами теории Т. (Не любое выражение является формулой, но любая формула является выражением).
3) Выделено некоторое множество формул, называемых аксиомами.
4) Имеется конечное множество отношений между формулами, называемых правилами вывода.
Если некоторая формула А находится с некоторыми формулами А1уА2,..^ находящихся в отношении Я;, то А называется непосредственным следствием из формул А1, А2,… полученным по правилу Я;.
Выводом в теории Т называется любая последовательность формул А1,А2 …,А„ , такая что любая формула А; является либо аксиомой Т, либо непосредственным следствием из каких-либо предыдущих формул.
Формула А называется теоремой теории Т, если существует вывод, в котором последней формулой является А. Этот вывод называется выводом формулы А. Таким образом, теоремы аксиоматической теории — это формулы, которые могут быть выведены по определённым правилам.
Пусть дано некоторое множество формул Г.
Формула А называется следствием множества формул Г тогда и только тогда, когда, существует такая последовательность формул А1,А2,_ Ап , что:
1) Ап есть А, (А= Ап)
2) А — это формула из Г (А э Г)
3) А есть непосредственное следствие из предыдущих формул.
Тогда последовательность А1,А2,_Ап называется выводом А из множества Г. Элементы Г называются посылками вывода или гипотезами. Применяют следующую запись Г|- А, (А есть следствие из Г). Если Г={ ВьВ2,…Вп} и Г|- А то ВьВ2,..Вп [ А
Если Г=0 то Г \- А тогда и только тогда, когда А является аксиомой или теоремой и обозначается \- А. (Она будет выводиться не из 0, а из аксиом).
2.2. Свойства понятия выводимости из системы гипотез.

Пусть Г- некоторое множество формул, а А, В, С- произвольные формулы.
1) Г, А|- А
2) Г, А, В|- С, то Г, В, А|- С (т.е. можно менять порядок формул в выводе)
3) Г|-А и В — произвольная формула, то Г, В|- А (т.е. можно добавлять любое количество формул)
4) Г|- А, Г|- В и А, В|- С, то Г|- С
5) Г, А|- В и Г|- А, то Г|- В (правило удаления выводимой гипотезы). Пример формальной теории (АТ)
1. Зададим некоторое конечное множество символов теории Т — алфавит {,а,Ь}.
(Любая последовательность из этих символов называется выражением).
2. Зададим подмножество формул. Пусть формулами являются одиночные символы или любая последовательность символов алфавита.
3. Аксиома аа .
4. Правило вывода с1 с2 — Ьс1 Ьс2, где с1 и с2 — некоторые последовательности из символов а и Ь.
Вывод любой формулы начинается с аксиом. аа Применим правило вывода, получим Ьа Ьа
еще раз ЬЬа ЬЬа

п раз Ьпа Ьпа — формулы только такого вида будут
являться теоремами.
Теорема ли ЬЬа ЬЬаЬ ? — Это формула, но не теорема, т.к. мы не можем построить ее
вывод.

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

При создании формальных систем возникает вопрос — можно ли рассматривая некоторую формулу формальной системы определить является ли она доказуемой, т.е. теоремой или нет и как это доказать. При задании формальных систем полагается, что существует хорошо определенный способ, который за конечное число шагов позволяет ответить на данный вопрос. Если такой способ существует, то его называют процедурой разрешения, а саму формальную систему называют разрешимой. Разрешимых систем мало.
Приведенная выше формальная система является разрешимой системой, т.к. всегда можно определить доказуема ли формула или нет.
Интерпретация представляет собой распространение положений формальной системы на реальный мир. При интерпретации каждому символу придается некоторый смысл и устанавливается взаимно-однозначное соответствие между символами формальной системы и реальными объектами.
Теоремы формальной системы после интерпретации становятся обычными утверждениями и мы можем судить истинны они или ложны.
Формальная система тем более интересна, чем больше ее интерпретаций существует и необходимо, чтоб существовала хотя бы одна интерпретация в которой каждая теорема была бы истинной.
Предложим интерпретацию для вышеизложенного примера:
— будем интерпретировать как «=» аксиома будет интерпретироваться 0=0
Ьпа — это натуральное число следующее за числом Ьп-1а
тогда, применяя правило вывода будем получать выражения вида 1 =1
2=2 и. т. д
ЬЬа ЬЬЬа — не теорема т.к. 2ф3.
При интерпретации теорема обращается в истинное высказывание, а не теорема (простая формула) в ложное высказывание.
Другая интерпретация этой же формальной системы:
— совпадение двух выражений по смыслу
аксиому аа будем интерпретировать а: «на улице лето», в: «неверно, что» а=а по смыслу совпадают Ьа=Ьа по смыслу совпадают
а ЬЬа — формула, но не теорема, (хотя истинная в данном случае, т.к. «на улице лето» = «неверно, что» «неверно, что» «на улице лето» )
Получили, что если в качестве примера рассмотреть недоказуемую формулу, то ее интерпретация представляет собой истинное утверждение.
Имеется 4 варианта взаимоотношений между доказательством и значением истинности:
При рассмотрении формальных систем важным является также вопрос о непротиворечивости формальной системы, что означает, что в данной формальной теории не может быть одновременно построен вывод формулы А и —А.
Следующий момент, который рассматривается при создании формальных систем заключается в том, чтобы определить выводима ли некая формула в данной формальной системе и есть ли некоторое множество формул, которое совпадает со множеством теорем (выводимых формул) для данной формальной системы.
В частности, любой язык программирования является формальной системой.
1 ) есть алфавит
2) аксиомы — команды
3) выражения
4) правила построения новых конструкций из имеющихся.
Т.о, при создании формальной системы необходимо выяснить непротиворечивость и полноту и далее обговорить интерпретацию.
Исчисление высказываний — это 1-й тип. Пример формальной системы:
1) Алфавит {М, I, и}.
2) Формулы — любая последовательность алфавита.
3) Аксиома М1
4) Правила вывода: а) т1—т1И (где т — некоторая последовательность символов)
б) Мт—Мтт
в) Шь-»И правило переписывания
г) ИИ!
Требуется построить в данной формальной системе вывод формулы МИ. М1—МП—МШ—МИ
(2) (2) (3)

2.4. Исчисление высказываний. Определение и свойства.
Теорема дедукции.

Определение: Исчисление высказываний (ИВ) определяется следующим образом: 1 ) Алфавит исчисления высказываний содержит символы пропозициональных переменных с индексами или без, символы логических связок (—1, =) и символы скобок (,); 2) Форммулами ИВ является:
а) любая переменная с индексом или без, является формулой;
б) если А и В — формулы, то формулами будут:
(— А), (А=>В);
в) других формул нет.
3) Аксиомами исчисления высказываний является следующие схемы аксиом.
А1) A == (B == A)
А2) (A == (B == C)) == ((A == B )= (A == C)) А3) ((—B) = (—A)) == ((—B == A)= B)
4) Правилом вывода называют процедуру
(modus pones) A A == B A, A = B \- В
B
перехода от двух формул вида А и А=В к одной формуле вида В, для любых А и В. Это правило называют modus pones (MP). Это правило позволяет избавиться от импликации поэтому его называют также правилом удаления импликации (УИ).
Т.к. в аксиомах не участвуют связки v, &, <=> то нам придется их определить
A v B = —A == B
A & B = —(A == B)
A <=> B = (—A == B )=—(A = —B)
Замечание: В исчислении высказываний действуют те же правила опускания скобок, что и в логике.
Замечание: Наряду со свойствами 1-5 аксиоматической теории в ИВ имеет место шестое свойство:
6) если Г|- А=В и Г|-А, то Г|-В. Утверждение 1: В ИВ для любой формулы А выводима Доказательство: Построим вывод формулы А=А
1) В схему аксиом А2 вместо В подставим А=А и вместо. С — А. Получаем: (A == [(A == A)= A])= ((A ==(A == A))=> (A == A))
2) В схему А1 вместо В — А=А, вместо А — А получим A == ((A == A) = A)
3) Из пунктов 1) и 2) по правилу MP получаем: ((A == (A == A)) == (A == A))
4) В схему А1 вместо В подставим А получаем: A == (A == A)
5) Применяем правило MP к 3) и 4) получаем А =А — теорема. ЧТД. Утверждение 2: если Г|-А и В — любая формула, то из Г| В= A.
Доказательство: Пусть А1,А2,_,АП=А — вывод формулы А из Г, тогда, учитывая аксиому А1 и
правило МР получим, что A = (B = A) | В= A

В математических рассуждениях часто некоторое утверждение В доказывают, предпологая истинность некоторого другого предположения А. После чего заключают, что верно утверждение «если А то и В». В ИВ этот приём обосновывается следующей теоремой:
Теорема о дедукции: Пусть Г некоторое множество формул и А и В — некоторые
формулы, причем из Г, А| В, тогда из Г| А= В. (перенос посылки вправо)
Доказательство: пусть В1гВ2,.. ,Вп=В (*)
вывод формулы В из Г и А. Докажем теорему методом индукции по п, где п длина вывода (*).
При п=1формула (*) примет вид В=В1. По определению вывода возможно 1 . В1 — аксиома ИВ
2. В1 — формула из Г
3. В1=А
В случаях 1 и 2 имеем, что Г| В1 , тогда по утверждению 2 получаем, что из Г выводимо
А= В1(или Г| А= В)
Рассмотрим третий случай. В этом случае А=В имеет вид А=А. А по утверждению 1 А=А — теорема, следовательно из Г| А= А.
Допустим теперь, что если длина вывода формулы В из Г и А меньше п, то утверждение теоремы верно.
Докажем теорему, когда длина вывода равна п. Возможны четыре случая: 1 . Вп — аксиома ИВ
2. Вп — теорема из Г
3. Вп =А
4. Вп была получена из правилу МР из В; и Вj , где ;<п, _)<п. В случаях 1 -3 доказательство проводиться как при п=1 . Рассмотрим 4-й случай. Либо формула В; имеет вид В;=Вп либо Вj (имеет вид)= Вj=Вn ограничимся случаем, когда Вj=Вi=Вn. Из вывода (*) отбросим последние (п-;) формулы и получим вывод формулы В; из Г и А. А если отбросить последние п- формулы из (*), то получим вывод формулы Вj из Г и А. Длины обоих этих выводов меньше чем п, а по индуктивному предположению имеем 1. Из Г |- А=Вj 2. Из Г [■ А= (В; =Вп); 3. По схеме аксиома А2 имеем, если вместо В подставим В;, а вместо С подставим Вп, то получим: (А = (Б1 = Бп ))= ((А = Б, )= (А = Бп)) Применяя свойство 6 к пунктам 2 и 3 получаем, что из Г выводима А =Вп. ЧТД. Следствие 1: (правило силлогизма): Если А=В, В=С|- А=С. Доказательство: Имеем 3 гипотезы, 1) А=В 2) В= С 3) А - гипотеза Нужно доказать, что А=С - гипотеза. 4) Применим к 1 ) и 3) правило МР получаем, что | В 5) Применяя правило МР к 4) и 2), получаем, что |- С 6) Получили, что из А= В, В= С, А| С, тогда по теореме дедукции А= В, В= С|А= С. Следствие 2: из (А= (В=С)), В|- А=С. Доказательство: 1) Предположим, что А - гипотеза, тогда А, (А= (В=С)), В|- С 2) Из 1 ) по МР выводится В= С 3) Из 1 ) и 2) по МР выводится С 4) Применяя теорему о дедукции, получаем А= В, В= С|А= С ЧТД. Для любых А и В имеют место следующие утверждения в ИВ. Утверждение 3: |——А=А Утверждение 4: [■ А=——А Утверждение 5: |—А=(А=В) Утверждение 6: |-(—В=—А) = (А=В) Утверждение 7: \- (А=В) = (— В ==—А) Утверждение 8: |- А= (—В=— (А=В)) Утверждение 9: ^(А=В) =( (—А=В) =В) Следствие 3 к утверждению 9. Если из Г, А |- В, и из Г, — А|- В, то Г|- В Доказательство: 1 ) по тереме о дедукции Г|А= В 2) по тереме о дедукции Г|—А=В 3) по утверждению 9 (А=В) =( (—А=В) =В) 4) из 1 и 3 по МР [ (—А=В) =В 5) из 2 и 4 по МР [ В ЧТД. Полнота и непротиворечивость ИВ Покажем, что множество теорем ИВ совпадает со множеством тождественно истинных формул логики высказываний. Теорема 1: Всякая выводимая формула ИВ является тождественно истинной. Для аксиом ИВ это можно доказать непосредственной проверкой с помощью таблиц истинности. А в силу определения и свойств импликации формула, получающая из тождеств истинных формул по правилу МР также тождественно истинна, следовательно любая выводимая формула в ИВ - тождественно истинна. Имеет место и обратная теорема: любая тождественно истинная формула, выводима в ИВ, то есть является теоремой. Свойство аксиоматических теорий заключается в том, что если некоторая формула А выражает логический закон (как например тождественно истинные формулы) то она выводима в этой теории, называется полнотой аксиоматической теории или полнотой в широком смысле. Из Теоремы 2 следует, что ИВ - полная аксиоматическая теория. Определение: Формальную аксиоматическую теорию называют непротиворечивой, если в ней не существует формулы А такой, что одновременно выводимы А и —А. Теорема 3: ИВ непротиворечиво. Формальная аксиоматическая теория называется полной в узком смысле, если добавление любой невыводимой формулы в качестве схемы аксиом приводит к противоречию теории. Теорема 4: Исчисление высказываний полно в узком смысле. В любой формальной теории возникает вопрос о независимости системы аксиом, то есть можно ли вывести какую-либо аксиому из остальных, применяя правило вывода данной аксиоматической системы. Теорема 5: Система аксиом А1- А3 ИВ - независима. Вопрос о независимости аксиом оказывается равносилен вопросу о возможности замены без противоречия в рассматриваемой системе данной аксиомы ее отрицанием. Кроме того ИВ может быть описано схемами аксиом отличными от А1-А3 и вместо символов (в алфавите) — и = могут быть использованы другие наборы символов, но с их помощью должно быть возможно выразить все остальные логические операции. Пример: Рассмотрим ИВ в алфавит которого входят символы V, —, = со следующей схемой аксиом: А1 А V А = А А2 А = А V Б А3 А V Б = Б V А А4 (Б = С )=(А V С )=(А V С) Правило вывода одно - МР. В данном ИВ = рассматривается как сокращенная формула для х = у = — х V у. Теорема 2: Формула А ИВ выводима тогда и только тогда, когда она тождественно истинна. Практические задания к разделу 2 Доказать утверждения 3-9. Построить вывод формул в ИВ: а) Л^Б, Б^С [ Л^С ж) б) Л^(Б^С) |- Б^(Л^С) з) в) Л^(Б^С) |- Б^(Л^С) и) г) \- Л^(Б^(Л&Б)) к) д) [ Л^(ЛУБ) л) е) [ (Л^(Б^С))^(Б^(Л^С)) м) Скачать:

Загрузка...