Главная   Онлайн инструменты по математической логике   Мат. логика теория   Как считает компьютер?   Схемы для ЭВМ    

Определение формальной теории

Определение булевой функции
Элементарные булевы функции
Задание булевых функций посредством элементарных
Существенные и несущественные переменные
Эквивалентные функции
Основные эквивалентности
Функциональная полнота
Нормальные формы
Совершенные нормальные формы
Минимизация ДНФ методом Квайна
Карты Карно
Полином Жегалкина
Высказывания
Предикаты
Кванторы
Определение формальной теории
Исчисление высказываний
Теорема о дедукции. Полнота ИВ
Автоматическое доказательство теорем
Метод резолюций в ИВ
Определение алгоритма
Машина Тьюринга
Рекурсивные функции
Алгоритмически неразрешимые задачи
Алгоритмы и их сложности



     Формальная теория (или исчисление) ψ - это:
         1. множество A символов, образующих алфавит;
         2. множество F слов в алфавите A, F⊂A, которые называются формулами;
         3. подмножество B формул, B⊂F, которые называются аксиомами;
         4. множество отношений R на множестве формул, которые называются правилами вывода.
     Множество символов A может быть конечным или бесконечным. Обычно для образования символов используют конечное множество букв, к которым, если нужно, приписываются в качестве индексов натуральные числа.
     Множество формул F обычно задается индуктивным определением, например, с помощью формальной грамматики. Как правило, это множество бесконечно. Множества A и F в совокупности определяют язык, или сигнатуру, формальной теории.
     Множество аксиом B может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задается с помощью конечного множества схем аксиом и правил порождения конкретных аксиом из схемы аксиом.
     Множество правил вывода R, как правило, конечно.
     Итак, исчисление ψ есть четверка (A, F, B, R).
     Выводом в исчислении ψ называется последовательность формул F1,F2,…,Fn такая, что для любого k (1≤k≤n) формула Fk есть либо аксиома исчисления ψ, либо непосредственное следствие каких-либо предыдущих формул, полученное по правилу вывода.
     Формула G называется теоремой исчисления ψ (выводимой в ψ или доказуемой в ψ), если существует вывод F1,F2,…,Fn,G который называется выводом формулы G или доказательством теоремы G. Записывается это следующим образом:
         F1,F2,…,Fn├ G.
     Исчисление ψ называется непротиворечивым, если не все его формулы доказуемы. Можно дать другое определение непротиворечивости: Исчисление ψ называется непротиворечивым, если в нем не являются выводимыми одновременно формулы F и ¬F (отрицание F).
     Исчисление ψ называется полным (или адекватным), если каждому истинному высказыванию М соответствует теорема теории ψ.
     Формальная теория ψ называется разрешимой, если существует алгоритм, который для любой формулы теории определяет, является ли эта формула теоремой теории ψ или нет.

@ 2010 - 2016 tablica-istinnosti.ru Рейтинг@Mail.ru