lec3

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Исчисление высказываний является непротиворечивой, полной, разрешимой теорией, причем все три утверждения доказуемы в рамках самой логики высказываний.

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

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

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Алфавит исчисления высказываний - пропозиционарные переменные, логические операции, скобки

Правила построения формул исчисления высказываний - совпадают с правилами формирований формул алгебры высказываний

Аксиомы - подмножество формул, являющихся тождественно истинными

Правила вывода - правила подстановки, правила заключения и правила введения и удаления логических связок.

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

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

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

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Поиск алгоритма, определяющего к какому классу принадлежит та или иная формула, формирует проблему разрешимости исчисления высказываний.

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

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

Для логических связок импликации и дизъюнкции только пять аксиом.

Для полного набора логических связок: импликация, отрицание, конъюнкция и дизъюнкция система содержит десять аксиом

В силу полноты систем, использующих логические связки а) импликации и отрицания, б) импликации и дизъюнкции, в) импликации, отрицания, конъюнкции и дизъюнкции можно использовать в процессе дедуктивного вывода любую из указанных систем.

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

A1. F1 ! (F2 ! F1)

A2. (F1 ! F3) ! ((F2 ! F3) ! (F1 ! F3))

A3. (F1 ^ F2) ! F1

A4. (F1 ^ F2) ! F2

A5. F1 ! (F2 ! (F1 ^ F2)

A6. F1 ! (F1 _ F2)

A7. F2 ! (F1 _ F2)

A8. (F1 ! F3) ! ((F2 ! F3) ! (F1 _ F2) ! F3)

A9. (F1 ! F2) ! ((F1 ! F3) ! F1)

A10. (F1 ! F2) ! ((F1 ^ F3) ! (F2 ^ F3))

A11. (F1 ! F2) ! ((F1 _ F3) ! (F2 _ F3))

A12. F1 ! F1

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Выводом формулы из множества формул F1; F2; :::Fn называется такая последовательность формул, что любая Fi есть либо аксиома, либо непосредственно выводима из подмножества предшествующих ей формул F1; F2; :::Fn.

В этом случае формулу B называют заключением, а последовательность формул F1; F2; :::Fn, сформированная отношением логического вывода, представляет схему дедуктивного вывода.

Схему дедуктивного вывода записывают так:

F1; F2; :::Fn ` B

F1; F2; :::Fn

B

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Правила подстановки

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

Правила заключения

Красоткина О.В.

Красоткина

О.В.

Формальные

системы

Формальные

системы (аксиоматические теории)

Разновидности

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Если выводимая формула F содержит некоторую переменную A (обозначим этот факт F (A)) и существует произвольная формула B, то формула F (B), получающаяся заменой всех вхождений A на формулу B, также выводима в исчислении высказываний.

Этот факт формально описывают так:

RAB (F (A)

F (B)

Красоткина О.В.