Логічна теорія - це концептуальний клас елементарних висловлювань. описують властивості і зв'язку певній галузі логічних обчислень (див. Логіка). Логічну теорію також ототожнюють зі способом вибору підкласу справжніх висловлювань (теорем) з числа висловлювань, сформульованих на мові даної теорії. У найзагальнішому вигляді логічна теорія розглядається як безліч тверджень, замкнутих щодо виводимості, яка задає спосіб вибору теорем. Зазначене поняття логічної теорії було введено польським і американським математиком і логіком Альфредом Тарським в 30-і роки XX століття.
Замість відносини виводимості для отримання підкласу теорем часто використовується оператор приєднання наслідків, який визначається для деякого рахункового безлічі висловлювань A як функція C. σ (A) → σ (A) (тобто як відображення безлічі підмножин A в себе), яка для кожного підмножини X ⊆ A задовольняє таким умовам:
- (C 1) X ⊆ C (X) (вихідні твердження є складовою частиною теорії).
- (C 2) C (C (X) = C (X) (операція приєднання наслідків дозволяє отримати всі слідства прийнятих припущень без винятку).
- (C З) якщо X ⊆ Y. то C (X) ⊆ C (Y) (чим більше прийнятих припущень, тим більше наслідків ми отримуємо - властивість монотонності операції приєднання наслідків).
Оператор приєднання наслідків трансформується в відношення приєднання наслідків (виводимість) ⎕Cσ (A) ⊆ A між підмножинами A і елементами A. якщо постулювати, що для кожної підмножини X ⊆ A і для кожного твердження a з A виконується така умова:
x ⎕Ca тоді і тільки тоді, коли a ∈ C (X) (a виводиться з X тоді і тільки тоді, коли a належить множині наслідків з X).
Умови (C 1) - (C З) трансформуються при цьому в умови:
Теореми визначаються щодо виводимості як затвердження φ. такі, що ∅⎕cφ. а теорія буде являти собою безліч тверджень Σ, замкнутих щодо ставлення приєднання наслідків ⎕c. тобто таких, що якщо Σ⎕cφ. то φ ∈ Σ.
Теорія Σ аксіоматізіруема тоді і тільки тоді, коли існує рекурсивне безліч пропозицій Δ. таке, що Σ = C (Δ), тобто кожне речення, яке належить безлічі Σ, що виводиться з Δ. Якщо Δ звичайно, то теорію Σ називають звичайно-аксіоматізіруемой. Подібні теорії можуть бути задані списком своїх аксіом і з цієї причини в літературі поняття теорії часто ототожнюють з поняттям «аксіоматизована теорія».
Теорія Σ несуперечлива, якщо і тільки якщо не знайдеться така пропозиція, щоб воно само і його заперечення належали Σ; теорія сповнена, якщо і тільки якщо для кожної пропозиції (сформульованого на мові теорії) або воно саме, або його заперечення належить теорії.
Елементарної теорією, або теорією Першого порядку, в логіці називається така теорія така, мовою якої є мова першого порядку, аксіомами формальної системи є логічні аксіоми і деякі інші аксіоми, звані нелогічні аксіомами, покликані описати специфічні властивості об'єктів предметної області. Клас всіх елементарних теорій, сформульованих в одному і тому ж мовою, утворює своєрідну алгебру щодо операцій, сформульованих на основі теоретико-множинних операцій. Як показав А. Тарський в 1936 році, клас елементарних теорій, сформульованих на одному і тому ж мовою на основі класичної логіки, утворює щодо цих операцій брауерову алгебру. Я. Челяковскій в 1983 році поширив цей результат на випадок звичайно-аксіоматізіруемих теорій на базі широкого класу так званих фінітарно протоалгебраіческіх логік. Клас звичайно-аксіоматізіруемих теорій на базі класичної логіки утворює булеву алгебру.
При заміні виводимості на семантичне поняття логічного слідування отримують інше поняття теорії. Для первопорядкових теорій на базі класичної логіки ці два поняття збігаються, так як в цьому випадку логічне слідування і виводимість збігаються за обсягом. Але вже для второпорядкових теорій при такій заміні ми отримуємо два різних поняття теорії, причому теорія в семантичному сенсі буде теорія в синтаксичному сенсі, але не навпаки. Те ж саме відноситься до деяких первопорядковой теоріям, заснованим на некласичної логіки.