Правило образование форм исчисление высказываний

Исчисление высказываний ИВ – это аксиоматическая логическая система гильбертовского типа, адекватная алгебре высказываний. Опишем это исчисление. В качестве алфавита исчисления высказываний возьмем следующее множество символов: 1) счетное множество высказывательных переменных, обозначаемых прописными латинскими буквами с индексами и без них; 2) символы логических операций; 3) скобки ( , ). Вместе с символами алфавита будем использовать и метасимволы: латинские буквы жирного шрифта для обозначения формул и знак = для обозначения формул метасимволами. Множество формул обычно задается индуктивным определением. Допустимыми последовательностями символов или словами в языке исчисления высказываний являются формулы алгебры высказываний. Пункты 1 и 2 этого определения определяют элементарные формулы, а п. 3 – механизм образования новых формул.

Лекция 3 исчисление высказываний

Это множество формул называется схемой формулы U и обозначается выражением, полученным заменой в формуле U всех входящих в нее высказывательных переменных метасимволами . Например, из формулы возникает схема формул . (5) Этой схеме принадлежит формула . Новые схемы формул можно получить заменой ее метасимволов схемами формул.

Эти схемы выделяют некоторое подмножество формул из множества формул, принадлежащих исходной схеме. Например, из схемы (5) можно получить схему формул . (6) Формула принадлежит как схеме формул (5), так и (6). Для формул, являющимися аксиомами или теоремами, схемы формул называются соответственно схемами аксиом или схемами теорем.

Правила вывода исчисления высказываний

  • 1)
    Вниманиеattention
    B1 = A
  • 2) B2 = — аксиома 1
  • 3) B3 = B = — получено из B1 и B2 в силу правила заключения.

Заметим, что если посылки являются аксиомами или теоремами исчисления высказываний, то класс выводимых из них формул совпадает с классом всех истинных формул, выводимых из любой системы посылок. Выводимость формулы из системы посылок отличается от доказательства теоремы в исчислении высказываний тем, что здесь допускается использование только правила заключения. Но при выводе формулы разрешается использовать любую теорему исчисления высказываний, для получения которой может применяться правило подстановки.