Перегляд вихідного коду сторінки Теорія моделей

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

== Історія ==
''Теорія моделей'' присвячена вивченню фундаментального зв'язку між [[синтаксис]]ом та [[семантика|семантикою]]. При цьому, першому в ній відповідає [[формальна мова]], а другому&nbsp;— модель&nbsp;— математична структура, яка допускає деякий опис цією мовою. ''Теорія моделей'' виникла як узагальнення існуючих підходів рішень [[метаматематика|метаматематичних]] проблем, пов'язаних із [[алгебра|алгеброю]] й [[математична логіка|математичною логікою]]. Самі ці підходи існували давно, але при цьому довгий час не розглядались у всій своїй загальності, в рамках однієї науково-філософської [[Парадигма (філософія)|парадигми]]. Природним прикладом в цьому контексті, пов'язаним з [[Аксіома паралельності Евкліда|п'ятим постулатом Евкліда]] про паралельну лінію. Сторіччями математикам не вдавалося довести його істинність, доки у [[XIX століття|XIX столітті]] [[Больяй Янош|Больяї]] й [[Лобачевський]] не збудували [[неевклідова геометрія|неевклідову геометрію]], показавши тим самим, що постулат паралельності не може бути ні доведений, ні спростований. З точки зору ''теорії моделей'', це означає, що система аксіом без п'ятого постулату допускає декілька різних моделей, тобто в цьому випадку&nbsp;— декілька варіантів реалізації геометрії.

Таким чином, початкова ''теорія моделей'' виросла з таких розділів математики як [[математична логіка|логіка]], [[універсальна алгебра]], [[теорія множин]] як узагальнення і закріплення існуючих знань. Тому перші результати теорії моделей з'явились задовго після її «Офіційного» виникнення. Першим таким результатом прийнято вважати<ref>''Кейслер Г., Чен Ч.'' Теория моделей.&nbsp;— М.: Мир, 1977.&nbsp;— с. 14.</ref> [[Теорема Льовенгейма—Сколема|теорему Льовенгейма&nbsp;— Сколема]] ([[1915]]). Другим великим результатом стала [[теорема компактності]], доведена [[Курт Гедель|Геделем]] ([[1930]]) та [[Мальцев Анатолій Іванович|Мальцевим]] ([[1936]]).

== Класична історія моделей першого порядку ==
Теорія моделей для [[логіка першого порядку|класичної логіки першого порядку]] є історично розвиненим і найбільш яскравим прикладом теоретично-модельного підходу. В ролі моделей тут є [[множина|множини]], що вказує область можливих значень [[Змінна|змінних]]. Функціональні символи інтерпретуються як операції відповідної [[арність|арності]] над ними, а [[предикат]]и&nbsp;— як [[Відношення (логіка)|відношення]] (більш детально, див. [[Логіка першого порядку#Інтерпретація|Логіка першого порядку, інтерпретація]]).

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

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

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

Теорема компактності знаходить використання і в конструюванні [[нестандартні моделі|нестандартних моделей]] класичних теорій, наприклад, [[елементарна арифметика|елементарної арифметики]] або [[нестандартний аналіз|математичного аналізу]].
{{Розширити розділ|дата=грудень 2013}}

=== Теорії та елементарна еквівалентність ===
Теорія <math>T</math>&nbsp;— це множина замкнутих формул, замкнутих відносно виводу, тобто якщо є формула <math>\varphi</math> слідує з <math>T</math>, то <math>\varphi</math> належить <math>T</math>.

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

Теорія <math>T</math> називається повною, якщо для будь-якої формули <math>\varphi</math> теорія має <math>\varphi</math> або <math>\lnot\varphi</math>. Якщо <math>A</math>&nbsp;— Алгебраїчна система, то множина істинних <math>A</math> замкнутих формул утворює повну теорію&nbsp;— теорія системи <math>A</math>, позначувану за допомогою <math>Th(A)</math>.

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

Якщо повна теорія <math>T</math> має скінченну модель <math>A</math>, то всі моделі теорії <math>T</math> ізоморфні <math>A</math>,
в тому числі, всі вони містять таку ж кількість елементів. Слідує що, для скінченних [[Алгебрична структура|алгебраїчних систем]], поняття елементарної еквівалентності і ізоморфізму збігаються.
{{Розширити розділ|дата=грудень 2013}}

=== Підсистеми і теореми Левенгейма&nbsp;— Скулема ===
Алгебраїчна система <math>B</math> називається підсистемою алгебраїчної системи <math>A</math>, якщо <math>|B|\subseteq|A|</math> і інтерпретація кожного сигнатурного символу в <math>B</math> є обмеженням його ж інтерпретації в <math>A</math> на множину <math>|B|</math>. Підсистема називається елементарною, якщо для будь-якої формули <math>\varphi(x_1,\;\ldots,\;x_n)</math> і для будь-яких <math>b_1,\;\ldots,\;b_n\in |B|</math> виконано: <math>A\models\varphi(b_1,\;\ldots,\;b_n)</math> тоді і тільки тоді, коли <math>B\models\varphi(b_1,\;\ldots,\;b_n)</math>. Система <math>A</math> називається в цих випадках (елементарним) розширенням системи <math>B</math>.

Елементарна підсистема <math>B</math> елементарно еквівалентна <math>A</math>. Теорії, для моделей котрих вірно і навпаки&nbsp;— кожна елементарна підсистема є підсистемою&nbsp;— називається модельно повною. Модельна повнота теорії <math>T</math> еквівалентна кожному з наступних властивостей:
* будь-яка формула в <math>T</math> еквівалентна екзистенційній формулі,
* будь-яка формула в <math>T</math> еквівалентна універсальній формулі,
* об'єднання <math>T</math> з діаграмою будь-якої моделі породжує повну теорію.

Якщо <math>X\subseteq|A|</math>&nbsp;— непорожня множина, то серед всіх підсистем <math>A</math>, включаючих <math>X</math>, існує найменша, як а називається найменшою множиною <math>X</math>. Для елементарної підсистеми в загальному випадку таке твердження невірне.

Кажуть, що теорія <math>T</math> має термальні скулемівські функції, якщо для кожної формули <math>\varphi(x,\;\bar y)</math> існує терм <math>t_\varphi(\bar y)</math> і з теорії <math>T</math> слідує формула <math>(\forall\bar y)((\exists x)\varphi(x,\;\bar y)\to \varphi(t_\varphi(\bar y),\;\bar y))</math>. Інакше кажучи, якщо існує елемент, на якому формула <math>\varphi(x,\;\bar y)</math> істинна, то як цей елемент можна взяти <math>t(\bar y)</math>. Якщо теорія має нормальні скулемівські функції, то вона модельно повна. Кожна теорія <math>T</math> має розширення <math>T^s</math>, яке має термальні скулемівські функції. При цьому кожна модель <math>A</math> теорії <math>T</math> може бути збагачена до моделі <math>A^s</math> теорії <math>T^s</math>.

'''Теорема Левенгейма&nbsp;— Скулема «вгору»''' стверджує, що якщо <math>A</math>&nbsp;— алгебраїчна система потужності не менше <math>\alpha=|Th(A)|</math>, то <math>A</math> то має елементарні розширення будь-якої потужності менш чи більш рівної <math>\alpha</math>.

'''Теорема Левенгейма&nbsp;— Скулема «вниз»:''' якщо <math>A</math>&nbsp;— алгебраїчна система потужності <math>\alpha</math> і <math>\beta=|Th(A)|</math>,
то <math>A</math> має елементарні підсистеми будь-якої потужності між <math>\beta</math> і <math>\alpha</math>.
{{Розширити розділ|дата=грудень 2013}}

=== Аксіоматизовність та стійкість ===
[[Множина]] формул <math>A</math> називається множиною аксіом для теорії <math>T</math>, якщо <math>T</math> є {{прояснити|ножино слідст}} <math>A</math>. Також, сама <math>T</math> є множиною аксіом для себе. Якщо для теорії <math>T</math> існує скінченна множина аксіом, то вона називається скінченно аксіоматизовною.

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

Теорія <math>T</math> називається стійкою відносно надсистем (відповідно, підсистем), якщо для будь-якої алгебраїчної системи <math>A</math> з <math>A\models T</math> і <math>B\subseteq A</math> (відповідно, <math>A\subseteq B</math>) слідує, що <math>B\models T</math>.
Теорія <math>T</math> стійка відносно підсистем тоді і тільки тоді, коли вона автоматизуєма засобом унвіерсальних формул.
Теорія <math>T</math> стійка відносно надсистем тоді і тільки тоді, коли вона аксіоматизуєма засобом екзестинційних формул.

Теорія <math>T</math> теорія зветься стійкою відносно гомоморфізмів, якщо для будь-якої алгебраїчної системи <math>A</math> з <math>A\models T</math> слідує, що <math>B\models T</math>, якщо <math>B</math>&nbsp;— гомоморфний образ <math>A</math>. Теорія <math>T</math> стійка відносно гомоморфізмів тоді і тільки тоді, коли вона аксіоматизуєма засобом простих формул (тобто формул, які не мають імплікацію і заперечення).
{{Розширити розділ|дата=грудень 2013}}

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

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

При об'єднанні ланцюгів (в тому рахунку неелеменатрних) зберігається істинність <math>\forall\exists</math>-формул, правдиво і протилежно&nbsp;— якщо формула зберігає свою істинність при об'єднанні будь-яких ланцюгів, то вона еквівалентна деякій <math>\forall\exists</math>-формулі.

Теорії, які можуть бути аксіоматизовані засобом <math>\forall\exists</math>-формул називаються індуктивними. За теоремою Ченя&nbsp;— Лося&nbsp;— Сушко теорія <math>T</math> є індуктивністю тоді і тільки тоді, коли вона стійка відносно об'єднаних ланцюгів. Важливий приклад індуктивної теорії&nbsp;— теорія полів фіксованої характеристики.

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

=== Ультравивід ===
Нехай <math>L</math>&nbsp;— мова. <math>\{\mathcal{A}_i\}_{i\in I}</math>&nbsp;— сім'я алгебраїчних систем, <math>\mathcal{A}_i=\langle M_i,\;L\rangle</math>. ''прямий вивід'' алгебраїчних систем <math>\mathcal{A}_i</math>, <math>i\in I</math>, називається алгебраїчна система <math>
\prod_{i\in I}\mathcal{A}_i=\left\langle\prod_{i\in I}A_i,\;L\right\rangle</math>, де для кожного предикатного символу <math>P\in L</math>
: <math>\prod_{i\in I}\mathcal{A}_i\models P(a_1,\;\ldots,\;a_{n_P})\Leftrightarrow\mathcal{A}_i\models P(a_{1i},\;\ldots,\;a_{n_Pi})</math> для кожного <math>i \in I</math>;
для кодного функціонального символу <math>f\in L</math>
: <math>(f(a_1,\;\ldots,\;a_{n_f}))_i=f(a_{1i},\;\ldots,\;a_{n_fi})</math>
і для кожного константного символу <math>c\in L</math>
: <math>(c)_i=c.</math>
Нехай <math>D</math>&nbsp;— фільтр над <math>I</math>. Визначеним над <math>\prod_{i\in I}A_i</math> відношення <math>a\sim_D b\Leftrightarrow\{i\in I\mid a_i=b_i\}\in D</math>. Введемо позначення:
: <math>a/D=\{b\mid b\sim_D a\}</math>, <math>\prod_{i\in I}A_i/D=\left\{a/D\mid a\in\prod_{i\in I}A_i\right\}.</math>
Визначимо алгебраїчну систему <math>\mathcal{A}=\left\langle\prod_{i\in I}A_i/D,\;L\right\rangle</math> наступним чином.

Покладемо для предикатного символу <math>P\in L</math>
: <math>\mathcal{A}\models P(a_1,\;\ldots,\;a_{n_P})\Leftrightarrow\{i\mid\mathcal{A}_i\models P(a_1i,\;\ldots,\;a_{n_Pi})\}\in D,</math>
для кожного функціонального символу <math>f\in L</math>
: <math>f(a_1/D,\;\ldots,\;a_{n_f}/D)=f(a_1,\;\ldots,\;a_n)/D</math>
і для сталих символі <math>c\in L</math>
: <math>c=c/D.</math>
Визначена таким чином алгебраїчна система <math>\mathcal{A}</math> зветься ''фільтрованним виводом'' систем <math>\mathcal{A}_i</math> по фільтру <math>D</math> і позначається <math>\prod_{i\in I}\mathcal{A}_i/D</math>. Якщо <math>D</math>&nbsp;— ультрафільтр, то <math>\prod_{i\in I}\mathcal{A}_i/D</math> називається ''ультравивід'', якщо все <math>\mathcal{A}_i</math> збігаються і рівні <math>\mathcal{A}</math>, то <math>\prod_{i\in I}\mathcal{A}_i/D</math> називається ультрастепенем <math>\mathcal{A}</math> і позначається <math>\mathcal{A}^I/D</math>.

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

'''Теорема Лося.''' ''Нехай <math>L</math>&nbsp;— мова, <math>\{\mathcal{A}_i\}_{i\in I}</math>&nbsp;— сім'я алгебраїчних систем мови <math>L</math>, <math>D</math>&nbsp;— ультрафільтр над <math>I</math>. Тоді для будь-якої формули <math>\varphi(\overline{x})</math> мови <math>L</math> і будь-якої послідовності <math>\overline{a}</math> елементів з <math>\prod_{i\in I} A_i</math>
: <math>\prod_{i\in I}\mathcal{A}_i/D\models\varphi(\overline{a}/D)\Leftrightarrow\{i\in I\mid\mathcal{A}_i\models\varphi(\overline{a}_i)\}\in D.</math>''

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

'''Теорема компактності.''' ''Якщо множина формул локально виконувана в деякому класі <math>\mathbf{K}</math>, то вона виконувана в деякому ультравивіді систем з <math>\mathbf{K}</math>.''

=== Типи ===
{{В планах|присвячений=типам, атомним і насиченним системам}}

=== Категоричність ===
{{Розширити розділ|дата=грудень 2013}}
Теорія <math>T</math> з рівністю, яка має скінченну або зліченну сигнатуру, зветься категориною в зліченній [[Потужність в множині|потужності]], якщо всі її зліченні нормальні моделі [[Ізоморфічні|Ізоморфні]]. Категоричність в даній незліченній потужності визначається аналогічно.

== Теорія моделей вищих порядків ==
{{В планах|присвячений=теоретико-множинній інтерпретації логік вищих порядків}}

== Теорія скінченних моделей ==
{{В планах|присвячений=вивченню властивостей кінцевих алгебраїчних систем}}

== Примітки ==
{{Примітки}}

{{Математична логіка}}


{{Math-stub}}
{{Logic-stub}}

[[Категорія:Математична логіка]]
[[Категорія:Теорія моделей|*]]
[[Категорія:Металогіка]]