Логическая теория

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

Вместо отношения выводимости для получения подкласса теорем часто используется оператор присоединения следствий, определяемый для некоторого счётного множества высказываний A как функция C: σ(A) → σ(A) (то есть как отображения множества подмножеств A в себя), которая для каждого подмножества X ⊆ A удовлетворяет следующим условиям:

• (C1) X ⊆ C(X) (исходные утверждения являются составной частью теории).
• (C2) C(C(X) = C(X) (операция присоединения следствий позволяет получить все следствия принимаемых допущений без исключения).
• (CЗ) если X ⊆ Y, то C(X) ⊆ C(Y) (чем больше принимаемых допущений, тем больше следствий мы получаем — свойство монотонности операции присоединения следствий).

Оператор присоединения следствий трансформируется в отношение присоединения следствий (выводимость) ⎕_C σ(A) ⊆ A между подмножествами A и элементами A, если постулировать, что для каждого подмножества X ⊆ A и для каждого утверждения a из A выполняется следующее условие:

x⎕_C a тогда и только тогда, когда a ∈ C(X) (a выводимо из X тогда и только тогда, когда a принадлежит множеству следствий из X).

Условия (C1) — (CЗ) трансформируются при этом в условия:

• (C1’) если a ∈ X, то X⎕_C a (допущения обладают теми же правами, что и выводимые утверждения).
• (C2’) если Y⎕_c a для всех a ∈ X, и X⎕_C b, то Y⎕_c b (выводимость транзитивна).
• (CЗ’) если X⎕_C a и X ⊆ Y, то Y⎕_c a (увеличение количества допущений не влияет на выводимость — монотонность выводимости).

Теоремы определяются относительно выводимости как утверждения φ, такие, что ∅⎕_c φ, а теория будет представлять собой множество утверждений ∑, замкнутых относительно отношения присоединения следствий ⎕_c, то есть таких, что если ∑⎕_c φ, то φ ∈ ∑.

Теория ∑ аксиоматизируема тогда и только тогда, когда существует рекурсивное множество предложений Δ, такое, что ∑ = C(Δ), то есть каждое предложение, принадлежащее множеству ∑, выводимо из Δ. Если Δ конечно, то теорию ∑ называют конечно-аксиоматизируемой. Подобные теории могут быть заданы списком своих аксиом и по этой причине в литературе понятие теории часто отождествляют с понятием «аксиоматизированная теория».

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

Элементарной теорией, или теорией Первого порядка, в логике называется такая теория такая, языком которой является язык первого порядка, аксиомами формальной системы являются логические аксиомы и некоторые другие аксиомы, называемые нелогическими аксиомами, призванные описать специфические свойства объектов предметной области. Класс всех элементарных теорий, сформулированных в одном и том же языке, образует своеобразную алгебру относительно операций, сформулированных на основе теоретико-множественных операций. Как показал А. Тарский в 1936 году, класс элементарных теорий, сформулированных на одном и том же языке на основе классической логики, образует относительно этих операций брауэрову алгебру. Я. Челяковский в 1983 году распространил этот результат на случай конечно-аксиоматизируемых теорий на базе широкого класса так называемых финитарно протоалгебраических логик. Класс конечно-аксиоматизируемых теорий на базе классической логики образует булеву алгебру.

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

Понятие теории в «семантическом смысле» выходит на передний план в том случае, когда учитывается, что главной задачей теории является установление закономерностей функционирования объектов предметной области, свойства которых детерминируют семантику используемого языка (см. Семантика). В настоящее время в логике существуют два основных направления, в рамках которых систематически используется это понятие теории: подход на базе семантики (X. Андрека, И. Немети) и теоретико-категорный подход (основанный на теории институций Гогена — Берсталла). Первый поход с самого начала рассматривает теорию как детерминированную определённым классом моделей и интерпретацией на этих моделях. Второй подход рассматривает теорию как определяемую:

• категорией различных словарей — наборов атомарных формул;
• функтором, сопоставляющим этой категории категорию предложений, сформулированных на основе этих словарей;
• функтором, сопоставляющим категории словарей категорию моделей, то есть семантических эквивалентов предложений;
• функцией выполнимости, сопоставляющей каждому словарю бинарное отношение L логической выполнимости между объектами категории моделей и объектами категории предложений.

Более «синтаксическая» версия категорного подхода (теория институций Фадейро — Сернадаса) заменяет функцию выполнимости на категорный аналог операции присоединения следствий, ассоциирующей с каждым словарём бинарное отношение логического замыкания между подмножествами предложений и предложениями, сформулированными на основе этих словарей.