Словарь по логике

Формальная теория

Множество формул некоторого формального языка, замкнутое относительно некоторого множества дедуктивных функций (правил вывода). То есть, некоторое множество ППФ языка L является формальной теорией не само по себе, а относительно некоторого дедуктивного замыкания. В принципе, правила вывода могут быть любыми, например, если единственное правило вывода A |– A, то любое подмножество языка L относительно такого замыкания будет формальной теорией. Обычно в качестве минимального требования выдвигают замкнутость относительно тех или иних правил подстановки. И, как правило, требуют также замкнутости относительно modus ponens.
– множество формул X является формальной теорией относительно множества функций O (операций над формулами языка L) X замкнуто относительно функций из O (функции из O являются операциями на X).
– множество формул X является формальной теорией относительно отношения выводимости |– для всякой формул (X |– A AєX).
– множество формул X является формальной теорией относительно отношения логического следования |= для всякой формулы A (X |= A AєX). Для первопорядковых теорий определения замыканий через |– и |= эквивалентны, для второпорядковых теорий замыкания относительно |– и |= – разные понятия.
– множество формул X является формальной теорией относительно оператора дедуктивного замыкания Cn Cn(X) = X.

© Автор статьи.