Интерпретация формальных теорий

Интерпретацией формальной теории Интерпретация формальных теорий в область интерпретации М называется функция Интерпретация формальных теорий , которая каждой формуле формальной теории ставит в соответствие некоторое содержательное высказывание относительно объектов множества М. Если соответствующее высказывание истинно, то говорят, что формула выполняется в интерпретации I.

Интерпретация называется моделью множества формул Г, если все формулы выполняются в данной интерпретации.

Если формула истинна в любой интерпретации, то это тавтология, если формула ложна в любой интерпретации, то это противоречие.

Формальная теория Интерпретация формальных теорий называется семантически непротиворечивой, если ни одна ее теорема не является противоречием.

Модель для формальной теории Интерпретация формальных теорий существует тогда и только тогда, когда она семантически непротиворечива.

Формальная теория Интерпретация формальных теорий формально непротиворечива, если в ней нельзя одновременно вывести формулу F и ее отрицание.

Формальная теория Интерпретация формальных теорий называется полной, если каждому истинному высказыванию модели М соответствует теорема теории Интерпретация формальных теорий .

Если для множества М существует формально полная непротиворечивая теория Интерпретация формальных теорий , то множество М называется аксиоматизируемым или формализуемым.

Формальная теория Интерпретация формальных теорий называется разрешимой, если существует алгоритм, который определяет, является ли формула теоремой теории.

Исчисление высказываний.

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

Исчисление высказываний – это формальная теория ?, которой:

1. Алфавит:

  • — буквы (A,B,…Z);
  • — специальные символы ?( ).

2. Формулы:

  • любая буква A, B,…Z – формула;
  • если А, В – формулы, то (А), (?А), (А В) – формулы.

3. Аксиомы:

1. А1: Интерпретация формальных теорий

2. А2: Интерпретация формальных теорий

3. А3: Интерпретация формальных теорий

Выражения А1-А3 называются схемами аксиом, т. к. каждая из них порождает бесконечное множество формул. Вместо А, В и С можно подставлять любые формулы.

4. Правило вывода: правило modus ponens (m.p.):

Интерпретация формальных теорий

A и B- любые формулы. Т. о. множество аксиом теории ? — бесконечно. Множество правил вывода также бесконечно.

Производные правила вывода

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

Теорема 1.

Интерпретация формальных теорий — закон тождества.

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

1. А1: Интерпретация формальных теорий . Выполним замену { Интерпретация формальных теорий }. Получим:

Интерпретация формальных теорий .

2. А1: Интерпретация формальных теорий . Выполним замену { Интерпретация формальных теорий }. Получим:

Интерпретация формальных теорий .

3. Из 1 и 2 по правилу m.p. получим:

Интерпретация формальных теорий .

4. A1: Интерпретация формальных теорий {A/B}. Получим: Интерпретация формальных теорий .

5. Из 3 и 4 по правилу m.p. получим Интерпретация формальных теорий .

Теорема 2

А Интерпретация формальных теорий — добавление антцедента.

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

1. А — гипотеза

2. А1: Интерпретация формальных теорий

3. Из 1 и 3 по правилу m.p. получаем

Интерпретация формальных теорий

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

Если имеется множество общезначимых формул, то из него можно вывести только общезначимые формулы.

Дедукция

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

Теорема (дедукции). Если Г – множество формул, А и B I Г и A|-?B, то Г|-АВ.

В частности A|-B, то АВ.

Доказательство. Пусть E1,E2,….En вывод B из Г, A. En = B. Покажем, что Г|-?А Ei, Интерпретация формальных теорий .

Пусть i=1.

Возможны 3 случая.

1) Пусть Е1 – аксиома. Тогда рассмотрим вывод:

1. Е1

2. А1: Интерпретация формальных теорий . Выполним замену {А/Е1, В/А}. Получим:

Интерпретация формальных теорий

3. Из 1 и 2 по правилу m.p. получаем |-?А E1.

2) Пусть Е1 Интерпретация формальных теорий Г. Доказательство аналогично 1).

3) Пусть Е1 Интерпретация формальных теорий А. Тогда по закону тождества (теорема1) Интерпретация формальных теорий , следовательно, Интерпретация формальных теорий

Таким образом Г Интерпретация формальных теорий .

Пусть i

1) Ek – аксиома.

2) Е1 Интерпретация формальных теорий Г.

3) Е1 Интерпретация формальных теорий А.

4) Ek получена из формул Ei и Ej по правилу m.p., причем i,j

Для 1), 2), 3) доказательство аналогично доказательству при i=1.

Для 4) случая:

1. Интерпретация формальных теорий (i)

2. Интерпретация формальных теорий (j)

Интерпретация формальных теорий

3. А2: Интерпретация формальных теорий . Выполним подстановку {Ei/B, Ek/C}, получим Интерпретация формальных теорий (n)

4. По правилу m.p. из (j) и (n) получаем Интерпретация формальных теорий (n+1)

5. По правилу m.p. из (j) и (n+1) получаем Интерпретация формальных теорий (n+2) ч.т.д.

Таким образом, Интерпретация формальных теорий для любого k, в том числе при k=n. Но En=B ? Интерпретация формальных теорий .

Схема аксиом A3 теории ? в доказательстве не использовалась, поэтому теорема дедукции имеет место для более широкого класса теорий, чем ?.

Следствие 1. Если Интерпретация формальных теорий , то Интерпретация формальных теорий и обратно.

Доказательство. По теореме дедукции, если Интерпретация формальных теорий , то Интерпретация формальных теорий . Пусть Г={0}. Тогда имеем Следствие 1.

Следствие 2. Интерпретация формальных теорий (правило транзитивности).

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

1. Гипотеза Интерпретация формальных теорий .

2. Гипотеза с.

3. Гипотеза А.

4. По правилу m.p. из 1 и 3 получаем B.

5. По правилу m.p. из 2 и 4 получаем C

6. Из 1-5 получаем: если Интерпретация формальных теорий , Интерпретация формальных теорий — гипотезы Г, то Интерпретация формальных теорий .

7. По теореме дедукции Интерпретация формальных теорий .

Следствие 3. Интерпретация формальных теорий (правило сечения).

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

1. Гипотеза Интерпретация формальных теорий .

2. Гипотеза A.

3. По правилу m.p. из 1 и 2 получим Интерпретация формальных теорий .

4. В – гипотеза.

5. По правилу m.p. из 3 и 4 получим С.

6. Из 1-5 получаем: Интерпретация формальных теорий

7. по теореме дедукции Интерпретация формальных теорий .

2.9. Некоторые теоремы теории ?

Множество теорем теории ? бесконечно. Рассмотрим некоторые из них.

1. Интерпретация формальных теорий (закон двойного отрицания).

2. Интерпретация формальных теорий (закон двойного отрицания).

3. Интерпретация формальных теорий (из ложного что угодно).

4. Интерпретация формальных теорий (закон де Моргана)

5. Интерпретация формальных теорий (закон де Моргана)

и т. д.

(Вывод законов см. Ф.А. Новиков “Дискретная математика для программистов”, стр.114).

Теорема. Теоремами теории ? являются только общезначимые формулы.

Интерпретация формальных теорий

Следствие. Теория ? формально непротиворечива.

Выводы.

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

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

Случайные записи:

Лекция 8: Формальные грамматики


Похожие статьи:

  • Модели теории первого порядка

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

  • Логические основы теории аргументации

    Аргументация – это совокупность логических операций, которые служат поиску и предъявлению оснований некоторой точки зрения с целью её понимания или(и)…

  • Гипотеза и теория

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

Добавьте постоянную ссылку в закладки. Вы можете следить за комментариями через RSS-ленту этой статьи.
Комментарии и трекбеки сейчас закрыты.