Теорія моделей

Тео́рія моде́лей — розділ математичної логіки, який займається вивченням зв'язку між формальними мовами та їх інтерпретаціями, або моделями. Назву теорія моделей вперше запропонував Альфред Тарський у 1954 році. Основний розвиток теорія моделей отримала в працях Тарського, Мальцева та Робінсона.

Історія

Теорія моделей присвячена вивченню фундаментального зв'язку між синтаксисом та семантикою. При цьому, першому в ній відповідає формальна мова, а другому — модель — математична структура, яка допускає деякий опис цією мовою. Теорія моделей виникла як узагальнення існуючих підходів рішень метаматематичних проблем, пов'язаних із алгеброю й математичною логікою. Самі ці підходи існували давно, але при цьому довгий час не розглядались у всій своїй загальності, в рамках однієї науково-філософської парадигми. Природним прикладом в цьому контексті, пов'язаним з п'ятим постулатом Евкліда про паралельну лінію. Сторіччями математикам не вдавалося довести його істинність, доки у XIX столітті Больяї й Лобачевський не збудували неевклідову геометрію, показавши тим самим, що постулат паралельності не може бути ні доведений, ні спростований. З точки зору теорії моделей, це означає, що система аксіом без п'ятого постулату допускає декілька різних моделей, тобто в цьому випадку — декілька варіантів реалізації геометрії.

Таким чином, початкова теорія моделей виросла з таких розділів математики як логіка, універсальна алгебра, теорія множин як узагальнення і закріплення існуючих знань. Тому перші результати теорії моделей з'явились задовго після її «Офіційного» виникнення. Першим таким результатом прийнято вважати теорему Льовенгейма — Сколема (1915). Другим великим результатом стала теорема компактності, доведена Геделем (1930) та Мальцевим (1936).

Класична історія моделей першого порядку

Теорія моделей для класичної логіки першого порядку є історично розвиненим і найбільш яскравим прикладом теоретично-модельного підходу. В ролі моделей тут є множини, що вказує область можливих значень змінних. Функціональні символи інтерпретуються як операції відповідної арності над ними, а предикати — як відношення (більш детально, див. Логіка першого порядку, інтерпретація).

Теорема компактності

Одним з найбільш важливих інструментів теорії моделей є теорема компактності, доведена Мальцевим, котра стверджує, що множина формул першого порядку має модель тільки тоді, коли модель має кожна його скінченна підмножина.

Назва теореми пов'язана з тим, що вона може бути сформульована як твердження про компактність стоунівського простору.

З теореми компактності слідує, що деякі поняття не є виражуваними в логіці першого порядку. Наприклад, поняття скінченності або зліченності неможе бути виражені ніякими формулами першого порядку й навіть їх множинами: якщо множина формул має стільки скільки потрібно великих скінченних моделей, то воно має безкінечну модель. Аналогічно, теорія, яка має безконечну модель, потужність якої не менше потужності сигнатури, має моделі і будь-якої потужності.

Теорема компактності знаходить використання і в конструюванні нестандартних моделей класичних теорій, наприклад, елементарної арифметики або математичного аналізу.

Теорії та елементарна еквівалентність

Теорія  — це множина замкнутих формул, замкнутих відносно виводу, тобто якщо є формула слідує з , то належить .

Теорія, яка має хоч би одну модель, називається несуперечливою, решта теорій — суперечливі.

Теорія називається повною, якщо для будь-якої формули теорія має або . Якщо  — Алгебраїчна система, то множина істинних замкнутих формул утворює повну теорію — теорія системи , позначувану за допомогою .

Якщо на алгебраїчних системах й істинні одні і ті ж самі формули, то і називаються елементарно еквівалентні. Таким чином, і елементарно еквівалентні тоді і тільки тоді, коли вони моделі однієї і тої самої теорії.

Якщо повна теорія має скінченну модель , то всі моделі теорії ізоморфні , в тому числі, всі вони містять таку ж кількість елементів. Слідує що, для скінченних алгебраїчних систем, поняття елементарної еквівалентності і ізоморфізму збігаються.

Підсистеми і теореми Левенгейма — Скулема

Алгебраїчна система називається підсистемою алгебраїчної системи , якщо і інтерпретація кожного сигнатурного символу в є обмеженням його ж інтерпретації в на множину . Підсистема називається елементарною, якщо для будь-якої формули і для будь-яких виконано: тоді і тільки тоді, коли . Система називається в цих випадках (елементарним) розширенням системи .

Елементарна підсистема елементарно еквівалентна . Теорії, для моделей котрих вірно і навпаки — кожна елементарна підсистема є підсистемою — називається модельно повною. Модельна повнота теорії еквівалентна кожному з наступних властивостей:

• будь-яка формула в еквівалентна екзистенційній формулі,
• будь-яка формула в еквівалентна універсальній формулі,
• об'єднання з діаграмою будь-якої моделі породжує повну теорію.

Якщо  — непорожня множина, то серед всіх підсистем , включаючих , існує найменша, як а називається найменшою множиною . Для елементарної підсистеми в загальному випадку таке твердження невірне.

Кажуть, що теорія має термальні скулемівські функції, якщо для кожної формули існує терм і з теорії слідує формула . Інакше кажучи, якщо існує елемент, на якому формула істинна, то як цей елемент можна взяти . Якщо теорія має нормальні скулемівські функції, то вона модельно повна. Кожна теорія має розширення , яке має термальні скулемівські функції. При цьому кожна модель теорії може бути збагачена до моделі теорії .

Теорема Левенгейма — Скулема «вгору» стверджує, що якщо  — алгебраїчна система потужності не менше , то то має елементарні розширення будь-якої потужності менш чи більш рівної .

Теорема Левенгейма — Скулема «вниз»: якщо  — алгебраїчна система потужності і , то має елементарні підсистеми будь-якої потужності між і .

Аксіоматизовність та стійкість

Множина формул називається множиною аксіом для теорії , якщо є ножино слідст^{[прояснити]} . Також, сама є множиною аксіом для себе. Якщо для теорії існує скінченна множина аксіом, то вона називається скінченно аксіоматизовною.

Суму алгебраїчних систем називають класами. Клас алгебраїчних систем називається аксіоматизуємий, якщо він є сукупністю моделей деякої теорії . В тому випадку множина аксіом для називається також множиною аксіом для . Клас звичайно аксіоматизуємий тоді і тільки тоді, коли аксіоматизуємий сам і його доповнення.

Теорія називається стійкою відносно надсистем (відповідно, підсистем), якщо для будь-якої алгебраїчної системи з і (відповідно, ) слідує, що . Теорія стійка відносно підсистем тоді і тільки тоді, коли вона автоматизуєма засобом унвіерсальних формул. Теорія стійка відносно надсистем тоді і тільки тоді, коли вона аксіоматизуєма засобом екзестинційних формул.

Теорія теорія зветься стійкою відносно гомоморфізмів, якщо для будь-якої алгебраїчної системи з слідує, що , якщо  — гомоморфний образ . Теорія стійка відносно гомоморфізмів тоді і тільки тоді, коли вона аксіоматизуєма засобом простих формул (тобто формул, які не мають імплікацію і заперечення).

Ланцюги

Ланцюгом називається множина алгебраїчних систем, лінійно впорядкована за відношенням «бути підсистемою». Якщо для елементів ланцюга виконується властивість «бути елементарною підсистемою», то ланцюг також називається елементарним.

Об'єднання алгебраїчних систем дає нову систему тієї ж сигнатури, яка буде підсистемою для всіх елементів ланцюга. При об'єднанні елементарного ланцюга це об'єднання буде елементарною підсистемою і відповідно, в ній зберігатиметься істинність всіх формул.

При об'єднанні ланцюгів (в тому рахунку неелеменатрних) зберігається істинність -формул, правдиво і протилежно — якщо формула зберігає свою істинність при об'єднанні будь-яких ланцюгів, то вона еквівалентна деякій -формулі.

Теорії, які можуть бути аксіоматизовані засобом -формул називаються індуктивними. За теоремою Ченя — Лося — Сушко теорія є індуктивністю тоді і тільки тоді, коли вона стійка відносно об'єднаних ланцюгів. Важливий приклад індуктивної теорії — теорія полів фіксованої характеристики.

Метод підсистем є найважливішим при побудові алгебраїчних систем з потрібними властивостями.

Ультравивід

Нехай  — мова.  — сім'я алгебраїчних систем, . прямий вивід алгебраїчних систем , , називається алгебраїчна система , де для кожного предикатного символу

для кодного функціонального символу

і для кожного константного символу

Нехай  — фільтр над . Визначеним над відношення . Введемо позначення:

Визначимо алгебраїчну систему наступним чином.

Покладемо для предикатного символу

для кожного функціонального символу

і для сталих символі

Визначена таким чином алгебраїчна система зветься фільтрованним виводом систем по фільтру і позначається . Якщо  — ультрафільтр, то називається ультравивід, якщо все збігаються і рівні , то називається ультрастепенем і позначається .

Основна властивість ультравиводу полягає в тому, що вони зберігають всі пропозиції:

Теорема Лося. Нехай  — мова,  — сім'я алгебраїчних систем мови ,  — ультрафільтр над . Тоді для будь-якої формули мови і будь-якої послідовності елементів з

Також теорему компактності можна сформулювати наступним чином.

Теорема компактності. Якщо множина формул локально виконувана в деякому класі , то вона виконувана в деякому ультравивіді систем з .

Типи

Категоричність

Теорія з рівністю, яка має скінченну або зліченну сигнатуру, зветься категориною в зліченній потужності, якщо всі її зліченні нормальні моделі Ізоморфні. Категоричність в даній незліченній потужності визначається аналогічно.

Теорія моделей вищих порядків

Теорія скінченних моделей

Примітки

1. Кейслер Г., Чен Ч. Теория моделей. — М.: Мир, 1977. — с. 14.