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

Любая тождественно-истинная формула доказуема в исчислении высказываний.

 

Лемма: Пусть формула А – произвольная формула языка логики высказывании. Пусть она содержит переменные: р1, р2, …рn. Рассмотрим произвольный набор значений этих переменных α 1, α 2, …α n.

Пусть pi' = pi, если α i = и

┐ рi, если α i = л

А' = А, если α = и

┐ А, если α = л

Доказать, что из р1', р2', … рn' |-- A '.

Доказательство: методом возвратной индукции. Параметр – число пропозициональных связок в формуле А (m). Для всех формул, где число связок меньше чем m, т е меньше чем у формулы А, то для них верно утверждение леммы.

Разбор случаев.

1. А = рi

и рi' = pi' A' = A = pi pi |-- pi 1.pi (доп.)

л рi' = ┐ pi' A' = ┐ A =┐ pi ┐ pi |-- ┐ pi 1. ┐ pi (доп.)

 

2. А = ┐ В В (индукт. допущ.) р1', р2', … рn' |-- В ' А' = А = ┐ В

и л р1', р2', … рn' |-- ┐ В

 

л и В' = В А' = ┐ А = ┐ ┐ В р1', р2', … рn' |-- В ' = В

р1', р2', … рn' |-- А ' = ┐ ┐ В

В |-- ┐ ┐ В 1.B

+2. ┐ В

3. ┐ ┐ В

 

3. А = В & C В С В' = В С' = С А ' = А = В & C

и и и и по индукт. допущ.: р1', р2', … рn' |-- В ' = В

р1', р2', … рn' |-- С ' = С

р1', р2', … рn' |-- А ' = В & C

 

л В В' = ┐ В А' = ┐ А А' = ┐ А = ┐ (В & C) по индукт. допущ.: р1', р2', … рn' |-- ┐ В

л р1', р2', … рn' |-- ┐ (В& C)

┐ В |-- ┐ (В& C)

1. ┐ В

+ 2. В& C

3. В

4. ┐ (В& C)

 

С С' = ┐ С А' = ┐ А А' = ┐ А = ┐ (В & C) по индукт. допущ.: р1', р2', … рn' |-- ┐ С

л р1', р2', … рn' |-- ┐ (В& C)

┐ С |-- ┐ (В& C)

 

4. А = В v C

и В В' = В А' = А = В v C по индукт. допущ.: р1', р2', … рn' |-- B

и р1', р2', … рn' |-- B v C

 

 

С C' = C A' = A = B v C по индукт. допущ.: р1', р2', … рn' |-- C

и р1', р2', … рn' |-- B v C

 

л В С В' = ┐ В С' = ┐ С А' = ┐ А = ┐ (В & C) по индукт. допущ.: р1', р2', … рn' |-- ┐ В

л и л р1', р2', … рn' |-- ┐ С

р1', р2', … рn' |-- ┐ (В v C)

┐ В, ┐ С |-- ┐ (В v C)

5. A = B > C

и В В' = ┐ В А' = А = В > C по индукт. допущ.: р1', р2', … рn' |-- ┐ В

л р1', р2', … рn' |-- В > C

┐ В |-- В > C

 

 

С C' = C А' = А = В > C по индукт. допущ.: р1', р2', … рn' |-- ┐ С

и р1', р2', … рn' |-- В > C

┐ С |-- В > C

 

л В С В' = В С' = С┐ А' = ┐ А = ┐ (В > C) по индукт. допущ.: р1', р2', … рn' |-- В

и и л р1', р2', … рn' |-- ┐ С

р1', р2', … рn' |-- ┐ (В > C)

В, ┐ С |-- ┐ (В > C)

Теорема. V˚ A ( |= A > ˚ |--A)

Допускаем, что |= A, показать что эта формула доказуема.

Во всех строках таблицы эта формула – истинна. А' = А. А' всегда совпадает с А

В соответствии с леммой из любой комбинации переменных и отрицаний переменных, входящих в А, будет выводиться сама формула А

р1, р2, … рn |-- А

р1, р2, … ┐ рn |-- А

 

Теорема дедукции позволяет последнюю формулу выносить за знак выводимости и подписывать ее с импликацией:

р1, р2, … р_n-1 |-- pn > А

р1, р2, … р_n-1 |-- ┐ pn > А

 

pn > A, ┐ pn > A |-- A

 

C > A, ┐ C > A |--A

 

1. C > A

2. ┐ C > A

+3. ┐ A

+4. C

5. A (исключение > : 1, 4)

6. ┐ C (введение ┐: 3, 5)

7. А (исключение > : 2, 6)

8. ┐ ┐ А (введение ┐: 3, 7)

9. А (исключение ┐: 8)

Исключаются пункты 4 и 5; и с 3 по 8.

 

pn > A, ┐ pn > A |-- A

р1, р2, … р_n-1 |-- А

 

р1, р2, …┐ р_n-1 |-- А

 

р1, р2, … р_n-2 |-- р_n-1 > А

р1, р2, … ┐ р_n-2 |-- р_n-1 > А

 

Уменьшая количество формул слева приходим к тому, что |-- А

 

 

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

Классическое исчисление высказываний с конечным числом аксиом и правилом подстановки обладает свойством синтаксической полноты.

 

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

Дано: Формула А – произвольная формула языка логики высказываний. Пусть она содержит переменные: γ 1, γ 2, …γ n. И произвольный набор значений этих переменных α 1, α 2, …α n. Осуществим подстановку в формулу А:

вместо γ i (итой переменной) будем подставлять или: γ i v ┐ γ i, если α i = и

или: γ i & ┐ γ i, если α i=л

В результате подстановки получаем формулу А*

Лемма: Если на данном наборе значений А принимает значение истина, то А* - тождественно-истинна (т.и.). Если А – ложь, то А* - тождественно-ложна (т.л.).

* - операция над формулой, процедура подстановки.

Доказательство:

5 типов формул.

А*: γ i* = или γ i v ┐ γ i, если α i = и

или: γ i & ┐ γ i, если α i=л

(┐ В)* = ┐ В* (преобразовать В, а перед результатом поставить ┐ )

(В& С)* = В* & C*

(BvC)* = B* v C*

(B> C)* = B* > C*

Лемма доказывается при помощи метода возвратной математический индукции:

1. Выбирается параметр индукции (такая функциональная характеристика объектов составляющих область, относительно которой ведется доказательство). Здесь – число пропозициональных связок в формуле А.

2. Принимается индуктивное допущение. Выбираем формулу с определенным числом связок и допускаем, что для всех формул, у которых число связок меньше чем у А, утверждение леммы верно.

 

Разбор случаев.

1. А – пропозициональная переменная. γ i содержит переменную γ i.

γ i = и γ i* = γ i v ┐ γ i т. и.

γ i = л γ i * = γ i & ┐ γ i т. л.

 

2. А = ┐ В

┐ В В (индукт. допущ.) В* ┐ В* = (┐ В)* = А*

и л т.л. т.и. т.и.

л и т.и. т.л. т.л.

 

3. А = В & С В С (индукт. допущ.) В* С* В*& С* = (В& С)* = А*

и и и т.и. т.и. т.и. т.и.

л л или л т.л. или т.л. т.л. т.л.

 

4. А = В v С В С (индукт. допущ.) В* С* В* v C* = (В* v С*) = А*

и и или и т.и или т.и. т.и. т.и.

л л и л т.л. и т.л. т.л. т.л

 

5. А = В > C В С (индукт. допущ.) В* С* В* > С* = (В > С)* = А*

и л или и т.л. или т.и. т.и. т.и.

л и и л т.и. и т.л. т.л. т.л.

 

Доказательство теоремы см. вопрос 5. Лемма в 6 пункте доказательства.

 

 

⇐ Предыдущая123

Поделиться: