Полнота логических функций. Теорема дедукции. Свойства формальных теорий (логических систем). Равносильные формулы логики предикатов, страница 3

1)=, тогда по Теореме 5.

├Пустое множество ╞.

2)├, тогда по Теореме 4.

├

                                   ├      ╞

Дедукционный шаг :

1)  =, по Теореме 5.

├ {}╞

2)  =, тогда по a₁)  - доказуема по определению.

a₁)

                        ├

├ : ПСП.

{}╞, {}╞ 

                                               {}╞                                               Ч. и т.д.

3) ├А, то по Теореме 4.      ├

                                                               {}╞

4)           {}╞, {}╞

                                      {}╞

{}╞, {}╞ 

                                               {}╞  

a₂)

Сделаем подстановку :  a₂)

                                                                  ├ a₂

ПСП :  ├

{}╞ - по условию.

                        {}╞

МР :        {}╞ ()  

                        {}╞{}╞()

МР :        {}╞   

Обобщённая Теорема Дедукции.

Если из совокупности гипотез  {} выводима некоторая формула , то                                                                          ├.

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

По условию :

                                   {}╞

                        :{}╞

                                    {}╞

                        :{}╞

:

.

(n-2) раза         .

.

Пустое множество ╞

                                               ├      (по Замечанию.)     Ч. и т.д.

§ 4. Применение Теоремы Дедукции

Теорема 1.

├

├

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

1)  Сначала докажем, что

├

Закон – это истинное утверждение.

H={}

Попробуем доказать, что :

2) H╞

Доказательство 2).

H╞, H╞

                                   МР :                H╞

H╞, H╞

                                   МР :                H╞                   Ч. и т.д.

Доказательство 1).

                                             {}╞

По Теореме Дедукции ├

├, ├

МР :                             ├                                                                               Ч. и т.д.

Замечание  1.

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

H╞

HY╞

Замечание  2. ( обратное к Теореме Дедукции)

H╞

H{B}╞

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

H{B}╞,  H{B}╞

МР :                H{B}╞                                                Ч. и т.д.

Замечание  3.

├

                        ├, ├

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

├, ├

                    МР :            ├             Ч. и т.д.       , аналогично для .

Замечание  4.

H╞

                    H╞, H╞

Замечание  5.

├, ├

   ├

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

a₈)  - доказуема по определению.

Сделаем подстановку :

a₈)=

├(a₈)

                        ПП :    ├a₈)

├, ├

                    МР :            ├

a₁)  - доказуема по определению.

Сделаем подстановку :

a₁) =

├(a₁)

                                   ПСП :   ├a₁)

├, ├

                                   МР :                ├

├, ├

                                   МР :                ├      

├, ├

                                   МР :                ├                                      Ч. и т.д.

Замечание  6.                    Правило введения коньюнкциии.

                              H╞, H╞

H╞

Теорема 2.                Правило соединения посылок.

├

                                                  ├

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

1) Докажем закон соединения посылок :

├

H={├}

2) H╞

Доказательство 2)

По Замечанию 4. :

H╞

                                   H╞, H╞

Применяем МР. два раза :

                                   H╞, H╞,  H╞

H╞                             Ч. и т.д.

Доказательство 1)

{├}╞

                        ТД :    ├             Ч. и т.д.

├, ├        

                        МР :                           ├                                          Ч. и т.д.

Теорема 3.                Правило разъединения посылок.

├

├

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

1)  ├

H={├}

2)  H╞

Доказательство 2)

По Замечанию 6. :

                                   H╞, H╞

H╞

H╞,H╞

                                   МР :                H╞                                Ч. и т.д.