yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->3.6. Свойства формальной теория L 

Математическая логика

3.6. Свойства формальной теория L 

Рассмотрим следующие свойства формальной теории L.

  • Непротиворечивость. »     Полнота.
  • Независимость системы аксиом.
  • Полнота теории понимается в узком и широком" смысле.

 Полнота в широком смысле означает, что каждую формулу можно доказать либо опровергнуть. |—Av|—¬A

Определение 3.3. Теория является полной (в узком смысле), если добавление любой недоказуемой в этой теории формулы делает ее противоречивой.

Чтобы доказать полноту теории, нужно построить ее модель, в которой каждому предложению в формальной теории должно соответствовать предложение модели.

Поставим в соответствие каждой букве исчисления L пропозициональную букву, каждой формуле - формулу, каждой теореме - тавтологию алгебры высказываний. Тогда получим взаимно однозначное соответствие, которое доказывает, что алгебра высказываний является моделью теории L. В этом утверждении нуждается в доказательстве только последнее положение о том, что существует взаимно однозначное соответствие между теоремами теории и тавтологиями. Докажем его.

Метатеорема. Каждая теорема теории L является тавтологией алгебры высказываний.

Доказательство. Схемам аксиом А1, А2, A3 соответствуют тавтологии алгебры высказываний. Для проверки этою положения- достаточно построить их таблицы истинности. Правило МР сохраняет свойство тавтологичности согласно теореме 1 о тавтологиях. Поскольку любая теорема выводима из аксиом с помощью правила МР, ей также будет соответствовать тавтология алгебры высказываний.

Определение 3.4. Говорят, что модель, или интерпретация, адекватна формальной теории, если каждая формула модели", являющаяся истинной, является теоремой теории.

Метатеорема адекватности Каждая тавтология алгебры высказываний является теоремой формальной теории L.

Доказательство основывается' на следующей металемме.

Металемма.   Пусть   формула   А   алгебры   высказываний   зависит   от

пропозициональных   букв   В1, В2,…Вк.   Тогда   каждой   строке   таблицы

истинности этой формулы соответствует вывод формальной' Теории L вида

B1,...,Bk|—A', где В'=В, если |В|=Т и В, если |B|=F, A=A или А, если А=Т или F.

 

Смысл леммы заключается в следующем. Если дана формула, например, А1=АВ) А), то, построив ее таблицу истинности (Табл. 3.1), можно определить, из каких посылок она выводима.

Таблица 3. 1.

A

B

(AB) A

A((AB) A)

F

F

F

T

F

T

T

T

T

F

F

F

T

T

T

T

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

 ¬А, ¬В|—А1; ¬А,В|—А1;   А, ¬В|—А1,      А,В|—А1               

Доказательство металеммы.

Доказательство проводится индукцией по числу связок в формуле А.

1. Базис индукции.

Пусть n=0, А=В, где n - число связок. Тогда формула А может принимать одно из двух значений, Т или Р, каждому из которых соответствует вывод: В |В и ¬В|В.

2. Шаг индукции Допустим, число связок в формуле А равно m, и при этом выполняется металемма. Докажем, что металемма выполняется, если

1. случай. Формула А образована с помощью связки отрицания: где    В   содержит    т    связок.    Возможны    следующие    истинностные распределения:

а). |В|=Т, |¬B|=F, |А|=F. Необходимо доказать, что существует вывод В'1,В'2,…,В'n |—A. то есть В'1,.В'2,....,В'n. |—В.

Согласно предположению индукции, существует вывод: В'1,В'2,...,В'n |— В. Согласно  теореме   4,   В| — ¬¬В,  следовательно,   по  правилу   силлогизма,

В'1,.В'2,....,В'n. |—В. Доказать, что существует вывод '1

Так   как  |В|=F,   то   ¬В=B.   Вывод   В'1,.В'2,....,В'n. |—В - существует   по предположению индукции, значит, существует и В'1,.В'2,....,В'n. |—В.

2. случай.   Формула   А   образована   с   помощью   логической   связки импликации:   А=В С,   где   В и   С содержат   не   более   m   связок.   По предположению индукции существуют выводы:

В'1,.В'2,....,В'n. |—В.

В'1,.В'2,....,В'n. |—C.

Рассмотрим истинностные распределения:

а). |C |=Т, |A |=Т. Доказать, что существует вывод В'1,.В'2,....,В'n. |А, то есть В'1,.В'2,....,В'n. |—В C.

По индуктивному предположению, существует вывод

·         В'1,.В'2,....,В'n. |С

·         |-С  (В С)                                                      А1

·         В'1,.В'2,....,В'n. |—В С

b). |C |=F, |B |=T, |A |=T

Выводы В'1,.В'2,....,В'n. |—С и В'1,.В'2,....,В'n. |—В существуют по индуктивному предположению.

·         |- В С).                                                     Т6

·         В'1,.В'2,....,В'n. |—В С                                       МР

с). |C |=F, |B |=T, |A |=T. Доказать, что существует вывод В'1,.В'2,....,В'n. |—А, то есть В'1,.В'2,....,В'n. |—(ВС).

·         В'1,.В'2,....,В'n. |—С            (по индуктивному предположению)

·         В'1,.В'2,....,В'n. |—В.           (по индуктивному предположению)

·         ВС)).                                               Т8

·         В'1,.В'2,....,В'n |СС)                               МР

·         В'1,.В'2,....,В'n. |С)                                     МР

Металемма доказана.

Доказательство   метатеоремы.   Пусть   А   -   тавтология,   зависящая   от пропозициональных букв В'1,.В'2,....,В'n. Согласно металемме, существует вывод:           В'1,.В'2,....,В'n. |—А                                                      где |Вn|=T и

  В'1,.В'2,....,В'n. |A                                                      где |Вn|=F

  В'1,.В'2,....,В'n. |BnA                                             МТД

  В'1,.В'2,....,В'n. |BnA                                             МТД

  |nA) ((BnA) A)                                   T9

Применяя дважды правило МР, получим, выводВ'1,.В'2,....,В'n-1|A. Последовательно исключая все переменные, получим \—А. Формула -А выводима из пустого множества гипотез, то есть она является теоремой теории L.

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

Теорема. Теория L неполна в широком смысле.

Доказательство. Действительно, не любая формула или ее отрицание являются теоремами теории L. Если взять нейтральную формулу алгебры высказываний, то ее отрицание также является нейтральной формулой, т.е. ни сама формула, ни ее отрицание не являются тавтологиями алгебры высказываний. Поэтому эти формулы не являются теоремами исчисления L,

Теорема. Теория L непротиворечива.

Это означает, что не существуют такой формулы А, чтобы А и ¬А одновременно являлись теоремами.

Доказательство. Каждая теорема теории L является тавтологией алгебры высказываний. Отрицание формулы, являющимися тавтологией, тавтологией не является. Следовательно, отрицание теоремы теоремой не является.

Теорема. Теория L полна в узком смысле.

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

Доказательство. Теория L имеет три схемы аксиом Al, A2, A3, правило вывода МР. Построим новую теорию L':A1, A2, A3, А, правило вывода МР, добавив к системе аксиом L формулу А, которая не является тавтологией алгебры высказываний. Значит, если А представлена конъюнктивной нормальной формой, то эта фирма должна содержать хотя бы одну элементарную дизъюнкцию, не содержащую ни одну переменную вместе с ее отрицанием: =В'1,vВ'2v....vВ'n. В элементарной дизъюнкции  заменим каждое вхождение пропозициональной буквы В'1 на В, если BL=F, и на В, если В|=Т. Получим:  =BvBv...vB =B, Произведем другую замену; В'1 на В, если B1=F, и на В, если В1=Т. Получим: =BvBv...vB = B. В новой теории L' формула А аксиома, то есть |A. По правилу удаления & любая дизъюнкция конъюктивной нормальной формы также доказуема, т. е. |- ' а это означает, что |— ¬B и |-B, т. е. теория L' - противоречива.

Определение 3.5. формальная теория называется разрешимой, если существует эффективная процедура, позволяющая за конечное число шагов определить, является ли формула теоремой или нет.

Теорема L - разрешима, так как каждой теореме теории соответствует тавтология, а для любой тавтологии можно построить таблицу истинности.

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

Теорема Схемы аксиом Al, A2, A3 в теории L независимы.

Доказательство 1. Докажем независимость А1. Для этого необходимо построить такую непротиворечивую модель, в которой выполняются все аксиомы, кроме первой. Построим модель в трехзначной логике.

 

 

 

 

 

 

 

 

 

 

Таблица 3. 2.                                                                     Таблица  3. 3.

A

A

A

B

AB

0

1

0

0

0

1

1

1

0

2

2

0

2

0

0

 

0

1

2

1

1

2

2

1

0

0

2

2

1

2

0

2

2

0

Формулу   А   будем   считать   выделенной, если она всегда принимает значение 0. Правило МР сохраняет свойство выделенности. Можно доказать, что схемы аксиом А2, A3 являются выделенными в данной модели. Следовательно, выделенной является и всякая формула, выводимая из А2, A3 с помощью правила МР. Однако формула А1 не выделенная, - для доказательства этого достаточно найти один набор, значение А1 на котором отлично от 0:1 (21)=10=2

Аналогично можно доказать независимость А2, построив другую трехзначную модель, где выделенными будут аксиомы А1 и A32. Чтобы показать • независимость A3, достаточно переопределить отрицание так, чтобы х=х (тождественная операция). Тогда А1 и А2 no-прежнему будут тавтологиями, а A3 уже не будет тавтологией.

2 Подробное доказательство можно найти в [Мендельсон Э. 1976].

 

22