Определение формального исчисления

Введем общее понятие формального исчисления. Будем говорить, что формальное исчисление I определено, если выполняются четыре условия.

1. Имеется некоторое множество А символов – алфавит исчисления I. Конечные последовательности символов называются словами или выражениями исчисления I. Обозначим через S множество всех слов алфавита исчисления I.

2. Задано подмножество FS, называемое множеством формул исчисления I. Элементы множества F называются формулами.

3. Выделено множество АхF формул, называемых аксиомами исчисления I.

4. Имеется конечное множество K отношений R₁,R₂,…,R_n между формулами, называемых правилами вывода, причем если (φ₁,…,φ_m,φ)R_i, то φ называется непосредственным следствием формул φ₁,…,φ_m по правилу R_i.

Итак, исчисление I есть четверка (А,F,Ах,K).

Выводом в исчислении I называется последовательность формул φ₁,φ₂,…,φ_n такая, что для любого i (1≤i≤n) формула φ_i есть либо аксиома исчисления I, либо непосредственное следствие каких-либо предыдущих формул.

Формула φ называется теоремой исчисления I, выводимой в I, или доказуемой в I, если существует вывод φ₁,…,φ_n,φ, который называется выводом формулы φ или доказательством теоремы φ.

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

2. Содержание

   • Введение
   • Программа курса математическая логика и терия алгоритмов
   • Логическое следствие в алгебре высказываний
   • 2.1.3. Эквивалентные формулы алгебры высказываний
   • 2.1.4. Дизъюнктивные и конъюнктивные нормальные формы в алгебре высказываний
   • 2.1.5. Совершенные дизъюнктивные и конъюнктивные нормальные формы
   • Исчисление высказываний
   • Определение формального исчисления
   • Система аксиом и правил вывода
   • Теорема о дедукции в исчислении высказываний
   • Теорема о замене в исчисления высказываний
   • Свойства выводимых и эквивалентных формул исчисления высказываний
   • Основные эквивалентности исчисления высказываний
   • Полнота и непротиворечивость исчисления высказываний
   • Логика предикатов
   • Алгебраические системы
   • Пример 3. Построить подсистему алгебраической системы , порожденную множествомХ:
   • Формулы логики предикатов
   • Истинность формулы логики предикатов в алгебраической системе
   • 2.3.4. Логическое следствие в логике предикатов
   • 2.3.5. Эквивалентные формулы логики предикатов
   • 2.3.6. Пренексная нормальная форма в логике предикатов
   • X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
   • X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
   • Xφ≡X(φ)xφ≡X(φ)
   • 2.4. Исчисление предикатов
   • 2.4.1. Система аксиом и правил вывода
   • 2.4.2. Эквивалентные формулы исчисления предикатов
   • 2.4.3. Теорема Геделя о полноте. Непротиворечивость исчисления предикатов
   • Элементы теории алгоритмов
   • 2.5.1. Машины Тьюринга
   • 2.5.2. Примитивно рекурсивные функции
   • 2.5.3. Частично рекурсивные функции
   • Задания для домашних и контрольных работ
   • 3.1. Совершенные дизъюнктивные нормальные формы, совершенные конъюнктивные нормальные формы
   • 3.2. Логическое следствие в алгебре высказываний
   • Логическое следствие в логике предикатов
   • Частично рекурсивные функции
   • Список литературы
   • Основная литература
   • 4.2. Дополнительная литература
   • Содержание