lec3

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

к.ф.-м.н., доцент Красоткина О.В.

Тульский государственный университет

Математическая логика и теория алгоритмов Лекция 3 Тула, 2014

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

1Формальные системы

Формальные системы (аксиоматические теории)

Разновидности формальных теорий

Свойства формальных теорий

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

Определение

Аксиомы

Правила вывода

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Определение

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

Уточнение

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

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Формальная теория (аксиоматическая теория ) считается определенной, если заданы

Алфавит формальной теории - конечное или счетное множество произвольных символов. Конечные последовательности символов называются выражениями теории

Правила построения формул формальной теории

- способы конструирования выражений формальной теории

Аксиомы - подмножество выражений, считающихся верными в рамках теории

Правила вывода - правила получения верных в рамках даной теории выражений на основе аксиом

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Заданы и аксиомы и правила вывода

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

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Заданы только аксиомы

Задаются только аксиомы, правила вывода считаются общеизвестными. Пример - Евклидова геоматрия

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

Заданы только правила вывода

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

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

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

Красоткина

О.В.

Формальные

системы

Формальные

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

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

формальных

теорий

Свойства

формальных

теорий

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

Определение

Аксиомы

Правила

вывода

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

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