Тео́рія моде́лей — розділ математичної логіки, який займається вивченням зв'язку між формальними мовами та їх інтерпретаціями, або моделями. Назву теорія моделей вперше запропонував Альфред Тарський у 1954 році. Основний розвиток теорія моделей отримала в працях Тарського, Мальцева та .
Історія
Теорія моделей присвячена вивченню фундаментального зв'язку між синтаксисом та семантикою. При цьому, першому в ній відповідає формальна мова, а другому — модель — математична структура, яка допускає деякий опис цією мовою. Теорія моделей виникла як узагальнення існуючих підходів рішень метаматематичних проблем, пов'язаних із алгеброю й математичною логікою. Самі ці підходи існували давно, але при цьому довгий час не розглядались у всій своїй загальності, в рамках однієї науково-філософської парадигми. Природним прикладом в цьому контексті, пов'язаним з п'ятим постулатом Евкліда про паралельну лінію. Сторіччями математикам не вдавалося довести його істинність, доки у XIX столітті Больяї й Лобачевський не збудували неевклідову геометрію, показавши тим самим, що постулат паралельності не може бути ні доведений, ні спростований. З точки зору теорії моделей, це означає, що система аксіом без п'ятого постулату допускає декілька різних моделей, тобто в цьому випадку — декілька варіантів реалізації геометрії.
Таким чином, початкова теорія моделей виросла з таких розділів математики як логіка, універсальна алгебра, теорія множин як узагальнення і закріплення існуючих знань. Тому перші результати теорії моделей з'явились задовго після її «Офіційного» виникнення. Першим таким результатом прийнято вважати теорему Льовенгейма — Сколема (1915). Другим великим результатом стала , доведена Геделем (1930) та Мальцевим (1936).
Класична історія моделей першого порядку
Теорія моделей для класичної логіки першого порядку є історично розвиненим і найбільш яскравим прикладом теоретично-модельного підходу. В ролі моделей тут є множини, що вказує область можливих значень змінних. Функціональні символи інтерпретуються як операції відповідної арності над ними, а предикати — як відношення (більш детально, див. (Логіка першого порядку, інтерпретація)).
Теорема компактності
Одним з найбільш важливих інструментів теорії моделей є теорема компактності, доведена Мальцевим, котра стверджує, що множина формул першого порядку має модель тільки тоді, коли модель має кожна його скінченна підмножина.
Назва теореми пов'язана з тим, що вона може бути сформульована як твердження про компактність .
З теореми компактності слідує, що деякі поняття не є виражуваними в логіці першого порядку. Наприклад, поняття скінченності або зліченності неможе бути виражені ніякими формулами першого порядку й навіть їх множинами: якщо множина формул має стільки скільки потрібно великих скінченних моделей, то воно має безкінечну модель. Аналогічно, теорія, яка має безконечну модель, потужність якої не менше потужності сигнатури, має моделі і будь-якої потужності.
Теорема компактності знаходить використання і в конструюванні класичних теорій, наприклад, елементарної арифметики або математичного аналізу.
Цей розділ потребує доповнення. (грудень 2013) |
Теорії та елементарна еквівалентність
Теорія — це множина замкнутих формул, замкнутих відносно виводу, тобто якщо є формула слідує з , то належить .
Теорія, яка має хоч би одну модель, називається несуперечливою, решта теорій — суперечливі.
Теорія називається повною, якщо для будь-якої формули теорія має або . Якщо — Алгебраїчна система, то множина істинних замкнутих формул утворює повну теорію — теорія системи , позначувану за допомогою .
Якщо на алгебраїчних системах й істинні одні і ті ж самі формули, то і називаються елементарно еквівалентні. Таким чином, і елементарно еквівалентні тоді і тільки тоді, коли вони моделі однієї і тої самої теорії.
Якщо повна теорія має скінченну модель , то всі моделі теорії ізоморфні , в тому числі, всі вони містять таку ж кількість елементів. Слідує що, для скінченних алгебраїчних систем, поняття елементарної еквівалентності і ізоморфізму збігаються.
Цей розділ потребує доповнення. (грудень 2013) |
Підсистеми і теореми Левенгейма — Скулема
Алгебраїчна система називається підсистемою алгебраїчної системи , якщо і інтерпретація кожного сигнатурного символу в є обмеженням його ж інтерпретації в на множину . Підсистема називається елементарною, якщо для будь-якої формули і для будь-яких виконано: тоді і тільки тоді, коли . Система називається в цих випадках (елементарним) розширенням системи .
Елементарна підсистема елементарно еквівалентна . Теорії, для моделей котрих вірно і навпаки — кожна елементарна підсистема є підсистемою — називається модельно повною. Модельна повнота теорії еквівалентна кожному з наступних властивостей:
- будь-яка формула в еквівалентна екзистенційній формулі,
- будь-яка формула в еквівалентна універсальній формулі,
- об'єднання з діаграмою будь-якої моделі породжує повну теорію.
Якщо — непорожня множина, то серед всіх підсистем , включаючих , існує найменша, як а називається найменшою множиною . Для елементарної підсистеми в загальному випадку таке твердження невірне.
Кажуть, що теорія має термальні скулемівські функції, якщо для кожної формули існує терм і з теорії слідує формула . Інакше кажучи, якщо існує елемент, на якому формула істинна, то як цей елемент можна взяти . Якщо теорія має нормальні скулемівські функції, то вона модельно повна. Кожна теорія має розширення , яке має термальні скулемівські функції. При цьому кожна модель теорії може бути збагачена до моделі теорії .
Теорема Левенгейма — Скулема «вгору» стверджує, що якщо — алгебраїчна система потужності не менше , то то має елементарні розширення будь-якої потужності менш чи більш рівної .
Теорема Левенгейма — Скулема «вниз»: якщо — алгебраїчна система потужності і , то має елементарні підсистеми будь-якої потужності між і .
Цей розділ потребує доповнення. (грудень 2013) |
Аксіоматизовність та стійкість
Множина формул називається множиною аксіом для теорії , якщо є ножино слідст[] . Також, сама є множиною аксіом для себе. Якщо для теорії існує скінченна множина аксіом, то вона називається скінченно аксіоматизовною.
Суму алгебраїчних систем називають класами. Клас алгебраїчних систем називається аксіоматизуємий, якщо він є сукупністю моделей деякої теорії . В тому випадку множина аксіом для називається також множиною аксіом для . Клас звичайно аксіоматизуємий тоді і тільки тоді, коли аксіоматизуємий сам і його доповнення.
Теорія називається стійкою відносно надсистем (відповідно, підсистем), якщо для будь-якої алгебраїчної системи з і (відповідно, ) слідує, що . Теорія стійка відносно підсистем тоді і тільки тоді, коли вона автоматизуєма засобом унвіерсальних формул. Теорія стійка відносно надсистем тоді і тільки тоді, коли вона аксіоматизуєма засобом екзестинційних формул.
Теорія теорія зветься стійкою відносно гомоморфізмів, якщо для будь-якої алгебраїчної системи з слідує, що , якщо — гомоморфний образ . Теорія стійка відносно гомоморфізмів тоді і тільки тоді, коли вона аксіоматизуєма засобом простих формул (тобто формул, які не мають імплікацію і заперечення).
Цей розділ потребує доповнення. (грудень 2013) |
Ланцюги
Ланцюгом називається множина алгебраїчних систем, лінійно впорядкована за відношенням «бути підсистемою». Якщо для елементів ланцюга виконується властивість «бути елементарною підсистемою», то ланцюг також називається елементарним.
Об'єднання алгебраїчних систем дає нову систему тієї ж сигнатури, яка буде підсистемою для всіх елементів ланцюга. При об'єднанні елементарного ланцюга це об'єднання буде елементарною підсистемою і відповідно, в ній зберігатиметься істинність всіх формул.
При об'єднанні ланцюгів (в тому рахунку неелеменатрних) зберігається істинність -формул, правдиво і протилежно — якщо формула зберігає свою істинність при об'єднанні будь-яких ланцюгів, то вона еквівалентна деякій -формулі.
Теорії, які можуть бути аксіоматизовані засобом -формул називаються індуктивними. За теоремою Ченя — Лося — Сушко теорія є індуктивністю тоді і тільки тоді, коли вона стійка відносно об'єднаних ланцюгів. Важливий приклад індуктивної теорії — теорія полів фіксованої характеристики.
Метод підсистем є найважливішим при побудові алгебраїчних систем з потрібними властивостями.
Цей розділ потребує доповнення. (грудень 2013) |
Ультравивід
Нехай — мова. — сім'я алгебраїчних систем, . прямий вивід алгебраїчних систем , , називається алгебраїчна система , де для кожного предикатного символу
- для кожного ;
для кодного функціонального символу
і для кожного константного символу
Нехай — фільтр над . Визначеним над відношення . Введемо позначення:
- ,
Визначимо алгебраїчну систему наступним чином.
Покладемо для предикатного символу
для кожного функціонального символу
і для сталих символі
Визначена таким чином алгебраїчна система зветься фільтрованним виводом систем по фільтру і позначається . Якщо — ультрафільтр, то називається ультравивід, якщо все збігаються і рівні , то називається ультрастепенем і позначається .
Основна властивість ультравиводу полягає в тому, що вони зберігають всі пропозиції:
Теорема Лося. Нехай — мова, — сім'я алгебраїчних систем мови , — ультрафільтр над . Тоді для будь-якої формули мови і будь-якої послідовності елементів з
Також теорему компактності можна сформулювати наступним чином.
Теорема компактності. Якщо множина формул локально виконувана в деякому класі , то вона виконувана в деякому ультравивіді систем з .
Типи
Цей розділ статті, присвячений типам, атомним і насиченним системам, ще . |
Категоричність
Цей розділ потребує доповнення. (грудень 2013) |
Теорія з рівністю, яка має скінченну або зліченну сигнатуру, зветься категориною в зліченній , якщо всі її зліченні нормальні моделі . Категоричність в даній незліченній потужності визначається аналогічно.
Теорія моделей вищих порядків
Цей розділ статті, присвячений теоретико-множинній інтерпретації логік вищих порядків, ще . |
Теорія скінченних моделей
Цей розділ статті, присвячений вивченню властивостей кінцевих алгебраїчних систем, ще . |
Примітки
- Кейслер Г., Чен Ч. Теория моделей. — М.: Мир, 1977. — с. 14.
Це незавершена стаття з математики. Ви можете проєкту, виправивши або дописавши її. |
Це незавершена стаття з логіки. Ви можете проєкту, виправивши або дописавши її. |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Teo riya mode lej rozdil matematichnoyi logiki yakij zajmayetsya vivchennyam zv yazku mizh formalnimi movami ta yih interpretaciyami abo modelyami Nazvu teoriya modelej vpershe zaproponuvav Alfred Tarskij u 1954 roci Osnovnij rozvitok teoriya modelej otrimala v pracyah Tarskogo Malceva ta IstoriyaTeoriya modelej prisvyachena vivchennyu fundamentalnogo zv yazku mizh sintaksisom ta semantikoyu Pri comu pershomu v nij vidpovidaye formalna mova a drugomu model matematichna struktura yaka dopuskaye deyakij opis ciyeyu movoyu Teoriya modelej vinikla yak uzagalnennya isnuyuchih pidhodiv rishen metamatematichnih problem pov yazanih iz algebroyu j matematichnoyu logikoyu Sami ci pidhodi isnuvali davno ale pri comu dovgij chas ne rozglyadalis u vsij svoyij zagalnosti v ramkah odniyeyi naukovo filosofskoyi paradigmi Prirodnim prikladom v comu konteksti pov yazanim z p yatim postulatom Evklida pro paralelnu liniyu Storichchyami matematikam ne vdavalosya dovesti jogo istinnist doki u XIX stolitti Bolyayi j Lobachevskij ne zbuduvali neevklidovu geometriyu pokazavshi tim samim sho postulat paralelnosti ne mozhe buti ni dovedenij ni sprostovanij Z tochki zoru teoriyi modelej ce oznachaye sho sistema aksiom bez p yatogo postulatu dopuskaye dekilka riznih modelej tobto v comu vipadku dekilka variantiv realizaciyi geometriyi Takim chinom pochatkova teoriya modelej virosla z takih rozdiliv matematiki yak logika universalna algebra teoriya mnozhin yak uzagalnennya i zakriplennya isnuyuchih znan Tomu pershi rezultati teoriyi modelej z yavilis zadovgo pislya yiyi Oficijnogo viniknennya Pershim takim rezultatom prijnyato vvazhati teoremu Lovengejma Skolema 1915 Drugim velikim rezultatom stala dovedena Gedelem 1930 ta Malcevim 1936 Klasichna istoriya modelej pershogo poryadkuTeoriya modelej dlya klasichnoyi logiki pershogo poryadku ye istorichno rozvinenim i najbilsh yaskravim prikladom teoretichno modelnogo pidhodu V roli modelej tut ye mnozhini sho vkazuye oblast mozhlivih znachen zminnih Funkcionalni simvoli interpretuyutsya yak operaciyi vidpovidnoyi arnosti nad nimi a predikati yak vidnoshennya bilsh detalno div Logika pershogo poryadku interpretaciya Teorema kompaktnosti Odnim z najbilsh vazhlivih instrumentiv teoriyi modelej ye teorema kompaktnosti dovedena Malcevim kotra stverdzhuye sho mnozhina formul pershogo poryadku maye model tilki todi koli model maye kozhna jogo skinchenna pidmnozhina Nazva teoremi pov yazana z tim sho vona mozhe buti sformulovana yak tverdzhennya pro kompaktnist Z teoremi kompaktnosti sliduye sho deyaki ponyattya ne ye virazhuvanimi v logici pershogo poryadku Napriklad ponyattya skinchennosti abo zlichennosti nemozhe buti virazheni niyakimi formulami pershogo poryadku j navit yih mnozhinami yaksho mnozhina formul maye stilki skilki potribno velikih skinchennih modelej to vono maye bezkinechnu model Analogichno teoriya yaka maye bezkonechnu model potuzhnist yakoyi ne menshe potuzhnosti signaturi maye modeli i bud yakoyi potuzhnosti Teorema kompaktnosti znahodit vikoristannya i v konstruyuvanni klasichnih teorij napriklad elementarnoyi arifmetiki abo matematichnogo analizu Cej rozdil potrebuye dopovnennya gruden 2013 Teoriyi ta elementarna ekvivalentnist Teoriya T displaystyle T ce mnozhina zamknutih formul zamknutih vidnosno vivodu tobto yaksho ye formula f displaystyle varphi sliduye z T displaystyle T to f displaystyle varphi nalezhit T displaystyle T Teoriya yaka maye hoch bi odnu model nazivayetsya nesuperechlivoyu reshta teorij superechlivi Teoriya T displaystyle T nazivayetsya povnoyu yaksho dlya bud yakoyi formuli f displaystyle varphi teoriya maye f displaystyle varphi abo f displaystyle lnot varphi Yaksho A displaystyle A Algebrayichna sistema to mnozhina istinnih A displaystyle A zamknutih formul utvoryuye povnu teoriyu teoriya sistemi A displaystyle A poznachuvanu za dopomogoyu T h A displaystyle Th A Yaksho na algebrayichnih sistemah A displaystyle A j B displaystyle B istinni odni i ti zh sami formuli to A displaystyle A i B displaystyle B nazivayutsya elementarno ekvivalentni Takim chinom A displaystyle A i B displaystyle B elementarno ekvivalentni todi i tilki todi koli voni modeli odniyeyi i toyi samoyi teoriyi Yaksho povna teoriya T displaystyle T maye skinchennu model A displaystyle A to vsi modeli teoriyi T displaystyle T izomorfni A displaystyle A v tomu chisli vsi voni mistyat taku zh kilkist elementiv Sliduye sho dlya skinchennih algebrayichnih sistem ponyattya elementarnoyi ekvivalentnosti i izomorfizmu zbigayutsya Cej rozdil potrebuye dopovnennya gruden 2013 Pidsistemi i teoremi Levengejma Skulema Algebrayichna sistema B displaystyle B nazivayetsya pidsistemoyu algebrayichnoyi sistemi A displaystyle A yaksho B A displaystyle B subseteq A i interpretaciya kozhnogo signaturnogo simvolu v B displaystyle B ye obmezhennyam jogo zh interpretaciyi v A displaystyle A na mnozhinu B displaystyle B Pidsistema nazivayetsya elementarnoyu yaksho dlya bud yakoyi formuli f x 1 x n displaystyle varphi x 1 ldots x n i dlya bud yakih b 1 b n B displaystyle b 1 ldots b n in B vikonano A f b 1 b n displaystyle A models varphi b 1 ldots b n todi i tilki todi koli B f b 1 b n displaystyle B models varphi b 1 ldots b n Sistema A displaystyle A nazivayetsya v cih vipadkah elementarnim rozshirennyam sistemi B displaystyle B Elementarna pidsistema B displaystyle B elementarno ekvivalentna A displaystyle A Teoriyi dlya modelej kotrih virno i navpaki kozhna elementarna pidsistema ye pidsistemoyu nazivayetsya modelno povnoyu Modelna povnota teoriyi T displaystyle T ekvivalentna kozhnomu z nastupnih vlastivostej bud yaka formula v T displaystyle T ekvivalentna ekzistencijnij formuli bud yaka formula v T displaystyle T ekvivalentna universalnij formuli ob yednannya T displaystyle T z diagramoyu bud yakoyi modeli porodzhuye povnu teoriyu Yaksho X A displaystyle X subseteq A neporozhnya mnozhina to sered vsih pidsistem A displaystyle A vklyuchayuchih X displaystyle X isnuye najmensha yak a nazivayetsya najmenshoyu mnozhinoyu X displaystyle X Dlya elementarnoyi pidsistemi v zagalnomu vipadku take tverdzhennya nevirne Kazhut sho teoriya T displaystyle T maye termalni skulemivski funkciyi yaksho dlya kozhnoyi formuli f x y displaystyle varphi x bar y isnuye term t f y displaystyle t varphi bar y i z teoriyi T displaystyle T sliduye formula y x f x y f t f y y displaystyle forall bar y exists x varphi x bar y to varphi t varphi bar y bar y Inakshe kazhuchi yaksho isnuye element na yakomu formula f x y displaystyle varphi x bar y istinna to yak cej element mozhna vzyati t y displaystyle t bar y Yaksho teoriya maye normalni skulemivski funkciyi to vona modelno povna Kozhna teoriya T displaystyle T maye rozshirennya T s displaystyle T s yake maye termalni skulemivski funkciyi Pri comu kozhna model A displaystyle A teoriyi T displaystyle T mozhe buti zbagachena do modeli A s displaystyle A s teoriyi T s displaystyle T s Teorema Levengejma Skulema vgoru stverdzhuye sho yaksho A displaystyle A algebrayichna sistema potuzhnosti ne menshe a T h A displaystyle alpha Th A to A displaystyle A to maye elementarni rozshirennya bud yakoyi potuzhnosti mensh chi bilsh rivnoyi a displaystyle alpha Teorema Levengejma Skulema vniz yaksho A displaystyle A algebrayichna sistema potuzhnosti a displaystyle alpha i b T h A displaystyle beta Th A to A displaystyle A maye elementarni pidsistemi bud yakoyi potuzhnosti mizh b displaystyle beta i a displaystyle alpha Cej rozdil potrebuye dopovnennya gruden 2013 Aksiomatizovnist ta stijkist Mnozhina formul A displaystyle A nazivayetsya mnozhinoyu aksiom dlya teoriyi T displaystyle T yaksho T displaystyle T ye nozhino slidst proyasniti A displaystyle A Takozh sama T displaystyle T ye mnozhinoyu aksiom dlya sebe Yaksho dlya teoriyi T displaystyle T isnuye skinchenna mnozhina aksiom to vona nazivayetsya skinchenno aksiomatizovnoyu Sumu algebrayichnih sistem nazivayut klasami Klas algebrayichnih sistem K displaystyle K nazivayetsya aksiomatizuyemij yaksho vin ye sukupnistyu modelej deyakoyi teoriyi T displaystyle T V tomu vipadku mnozhina aksiom dlya T displaystyle T nazivayetsya takozh mnozhinoyu aksiom dlya K displaystyle K Klas K displaystyle K zvichajno aksiomatizuyemij todi i tilki todi koli aksiomatizuyemij sam K displaystyle K i jogo dopovnennya Teoriya T displaystyle T nazivayetsya stijkoyu vidnosno nadsistem vidpovidno pidsistem yaksho dlya bud yakoyi algebrayichnoyi sistemi A displaystyle A z A T displaystyle A models T i B A displaystyle B subseteq A vidpovidno A B displaystyle A subseteq B sliduye sho B T displaystyle B models T Teoriya T displaystyle T stijka vidnosno pidsistem todi i tilki todi koli vona avtomatizuyema zasobom unviersalnih formul Teoriya T displaystyle T stijka vidnosno nadsistem todi i tilki todi koli vona aksiomatizuyema zasobom ekzestincijnih formul Teoriya T displaystyle T teoriya zvetsya stijkoyu vidnosno gomomorfizmiv yaksho dlya bud yakoyi algebrayichnoyi sistemi A displaystyle A z A T displaystyle A models T sliduye sho B T displaystyle B models T yaksho B displaystyle B gomomorfnij obraz A displaystyle A Teoriya T displaystyle T stijka vidnosno gomomorfizmiv todi i tilki todi koli vona aksiomatizuyema zasobom prostih formul tobto formul yaki ne mayut implikaciyu i zaperechennya Cej rozdil potrebuye dopovnennya gruden 2013 Lancyugi Lancyugom nazivayetsya mnozhina algebrayichnih sistem linijno vporyadkovana za vidnoshennyam buti pidsistemoyu Yaksho dlya elementiv lancyuga vikonuyetsya vlastivist buti elementarnoyu pidsistemoyu to lancyug takozh nazivayetsya elementarnim Ob yednannya algebrayichnih sistem daye novu sistemu tiyeyi zh signaturi yaka bude pidsistemoyu dlya vsih elementiv lancyuga Pri ob yednanni elementarnogo lancyuga ce ob yednannya bude elementarnoyu pidsistemoyu i vidpovidno v nij zberigatimetsya istinnist vsih formul Pri ob yednanni lancyugiv v tomu rahunku neelemenatrnih zberigayetsya istinnist displaystyle forall exists formul pravdivo i protilezhno yaksho formula zberigaye svoyu istinnist pri ob yednanni bud yakih lancyugiv to vona ekvivalentna deyakij displaystyle forall exists formuli Teoriyi yaki mozhut buti aksiomatizovani zasobom displaystyle forall exists formul nazivayutsya induktivnimi Za teoremoyu Chenya Losya Sushko teoriya T displaystyle T ye induktivnistyu todi i tilki todi koli vona stijka vidnosno ob yednanih lancyugiv Vazhlivij priklad induktivnoyi teoriyi teoriya poliv fiksovanoyi harakteristiki Metod pidsistem ye najvazhlivishim pri pobudovi algebrayichnih sistem z potribnimi vlastivostyami Cej rozdil potrebuye dopovnennya gruden 2013 Ultravivid Nehaj L displaystyle L mova A i i I displaystyle mathcal A i i in I sim ya algebrayichnih sistem A i M i L displaystyle mathcal A i langle M i L rangle pryamij vivid algebrayichnih sistem A i displaystyle mathcal A i i I displaystyle i in I nazivayetsya algebrayichna sistema i I A i i I A i L displaystyle prod i in I mathcal A i left langle prod i in I A i L right rangle de dlya kozhnogo predikatnogo simvolu P L displaystyle P in L i I A i P a 1 a n P A i P a 1 i a n P i displaystyle 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 P i dlya kozhnogo i I displaystyle i in I dlya kodnogo funkcionalnogo simvolu f L displaystyle f in L f a 1 a n f i f a 1 i a n f i displaystyle f a 1 ldots a n f i f a 1i ldots a n f i i dlya kozhnogo konstantnogo simvolu c L displaystyle c in L c i c displaystyle c i c Nehaj D displaystyle D filtr nad I displaystyle I Viznachenim nad i I A i displaystyle prod i in I A i vidnoshennya a D b i I a i b i D displaystyle a sim D b Leftrightarrow i in I mid a i b i in D Vvedemo poznachennya a D b b D a displaystyle a D b mid b sim D a i I A i D a D a i I A i displaystyle prod i in I A i D left a D mid a in prod i in I A i right Viznachimo algebrayichnu sistemu A i I A i D L displaystyle mathcal A left langle prod i in I A i D L right rangle nastupnim chinom Poklademo dlya predikatnogo simvolu P L displaystyle P in L A P a 1 a n P i A i P a 1 i a n P i D displaystyle mathcal A models P a 1 ldots a n P Leftrightarrow i mid mathcal A i models P a 1 i ldots a n P i in D dlya kozhnogo funkcionalnogo simvolu f L displaystyle f in L f a 1 D a n f D f a 1 a n D displaystyle f a 1 D ldots a n f D f a 1 ldots a n D i dlya stalih simvoli c L displaystyle c in L c c D displaystyle c c D Viznachena takim chinom algebrayichna sistema A displaystyle mathcal A zvetsya filtrovannim vivodom sistem A i displaystyle mathcal A i po filtru D displaystyle D i poznachayetsya i I A i D displaystyle prod i in I mathcal A i D Yaksho D displaystyle D ultrafiltr to i I A i D displaystyle prod i in I mathcal A i D nazivayetsya ultravivid yaksho vse A i displaystyle mathcal A i zbigayutsya i rivni A displaystyle mathcal A to i I A i D displaystyle prod i in I mathcal A i D nazivayetsya ultrastepenem A displaystyle mathcal A i poznachayetsya A I D displaystyle mathcal A I D Osnovna vlastivist ultravivodu polyagaye v tomu sho voni zberigayut vsi propoziciyi Teorema Losya Nehaj L displaystyle L mova A i i I displaystyle mathcal A i i in I sim ya algebrayichnih sistem movi L displaystyle L D displaystyle D ultrafiltr nad I displaystyle I Todi dlya bud yakoyi formuli f x displaystyle varphi overline x movi L displaystyle L i bud yakoyi poslidovnosti a displaystyle overline a elementiv z i I A i displaystyle prod i in I A i i I A i D f a D i I A i f a i D displaystyle 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 Takozh teoremu kompaktnosti mozhna sformulyuvati nastupnim chinom Teorema kompaktnosti Yaksho mnozhina formul lokalno vikonuvana v deyakomu klasi K displaystyle mathbf K to vona vikonuvana v deyakomu ultravividi sistem z K displaystyle mathbf K Tipi Cej rozdil statti prisvyachenij tipam atomnim i nasichennim sistemam she ne napisano Vi mozhete dopomogti proyektu napisavshi jogo Kategorichnist Cej rozdil potrebuye dopovnennya gruden 2013 Teoriya T displaystyle T z rivnistyu yaka maye skinchennu abo zlichennu signaturu zvetsya kategorinoyu v zlichennij yaksho vsi yiyi zlichenni normalni modeli Kategorichnist v danij nezlichennij potuzhnosti viznachayetsya analogichno Teoriya modelej vishih poryadkivCej rozdil statti prisvyachenij teoretiko mnozhinnij interpretaciyi logik vishih poryadkiv she ne napisano Vi mozhete dopomogti proyektu napisavshi jogo Teoriya skinchennih modelejCej rozdil statti prisvyachenij vivchennyu vlastivostej kincevih algebrayichnih sistem she ne napisano Vi mozhete dopomogti proyektu napisavshi jogo PrimitkiKejsler G Chen Ch Teoriya modelej M Mir 1977 s 14 Ce nezavershena stattya z matematiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Ce nezavershena stattya z logiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi