Modellteori

Modellteori är en gren av matematisk logik som handlar om studiet av förhållandet mellan formella språk och deras tolkningar , eller modeller. Namnmodellteorin föreslogs först av Alfred Tarski 1954 . Den huvudsakliga utvecklingen av teorin om modeller var i verken av Tarski, Maltsev och Robinson .

Origins

Modellteori ägnas åt studiet av det grundläggande förhållandet mellan syntax och semantik . Samtidigt motsvarar det formella språket det första i det , och modellen motsvarar det andra - en matematisk struktur som tillåter en viss beskrivning av detta språk. Modellteori uppstod som en generalisering av befintliga metoder för att lösa metamatematiska problem relaterade till algebra och matematisk logik . Dessa tillvägagångssätt i sig har funnits länge, men under lång tid betraktades de inte i sin helhet, inom ramen för ett enda logiskt-filosofiskt paradigm . Ett naturligt exempel i detta sammanhang är problemet med Euklides femte postulat om parallella linjer. I århundraden misslyckades matematiker med att bevisa dess sanning, förrän Bolyai och Lobatsjovskij på 1800-talet byggde icke-euklidisk geometri , vilket visade att det parallella postulatet varken kan bevisas eller vederläggas. Ur modellteoretisk synvinkel innebär detta att systemet av axiom utan det femte postulatet tillåter flera olika modeller, det vill säga i det här fallet flera alternativ för att implementera geometrin.

Således växte den ursprungliga teorin om modeller ur sådana grenar av matematiken som logik , universell algebra , mängdteori som en generalisering och utvidgning av befintlig kunskap. Därför dök de första resultaten av modellteorin upp långt innan dess "officiella" utseende. Löwenheim-Skolem-satsen ( 1915 ) anses vara det första sådana resultatet [1] . Ett annat stort resultat var kompakthetssatsen , bevisad av Gödel ( 1930 ) och Maltsev ( 1936 ).

Klassisk första ordningens modellteori

Modellteori för klassisk första ordningens logik är historiskt sett det första och mest utvecklade exemplet på en modellteoretisk ansats. Modellernas roll här spelas av uppsättningar som representerar intervallet av möjliga värden för variabler . Funktionssymboler tolkas som operationer av motsvarande aritet på dem, och predikat som relationer (för mer information, se Första ordningens logik, tolkning ).

Kompakthetsteorem

Ett av de viktigaste verktygen inom modellteorin är kompaktitetsteoremet som bevisats av Maltsev , som säger att en uppsättning första ordningens formler har en modell om och bara om modellen har varje ändlig delmängd av den formleruppsättningen.

Namnet på satsen kommer från det faktum att det kan anges som ett påstående om kompaktheten hos ett stenrum .

Det följer av kompaktitetssatsen att vissa begrepp inte kan uttryckas i första ordningens logik. Till exempel kan begreppen ändlighet eller räknebarhet inte uttryckas med några första ordningens formler eller ens deras mängder: om en uppsättning formler har godtyckligt stora ändliga modeller, så har den också en oändlig modell. På liknande sätt har en teori som har en oändlig modell vars kardinalitet inte är mindre än signaturens kardinalitet modeller av någon större kardinalitet.

Kompakthetssatsen finner tillämpning för att konstruera icke-standardiserade modeller av klassiska teorier, såsom elementär aritmetik eller kalkyl .

Teorier och elementär ekvivalens

En teori är en uppsättning formler som är stängd med avseende på deducerbarhet (kort sagt sluten), det vill säga en sådan mängd att om formeln följer av , så tillhör den . $T$ $T$ $\varphi$ $T$ $\varphi$ $T$

En teori som har minst en modell kallas konsekvent, de andra teorierna kallas motsägelsefulla.

En teori kallas komplett om teorin för någon formel innehåller eller . Om är ett algebraiskt system, bildar uppsättningen sanna på slutna formler en komplett teori - systemets teori , betecknad med . $T$ $\varphi$ $\varphi$ $\linte \varphi$ $A$ $A$ $A$ $Th(A)$

Om på algebraiska system och samma slutna formler är sanna, så sägs och vara elementärt ekvivalenta . Alltså och är elementärt likvärdiga om och bara om de är modeller av samma fullständiga teori. $A$ $B$ $A$ $B$ $A$ $B$

Om en komplett teori har en finit modell är alla modeller av teorin isomorfa , i synnerhet innehåller de alla samma antal element. För finita algebraiska system sammanfaller därför begreppen elementär ekvivalens och isomorfism. $T$ $A$ $T$ $A$

Delsystem och Löwenheim-Skolem-satser

Ett algebraiskt system kallas ett delsystem av ett algebraiskt system om tolkningen av varje signatursymbol i är en begränsning av dess tolkning i mängden . Ett delsystem kallas elementärt om för vilken formel som helst och för vilken det har: om och endast om . Systemet kallas i dessa fall för en (elementär) förlängning av systemet . $B$ $A$ $|B|\subseteq |A|$ $B$ $A$ $|B|$ $\varphi (x_{1},\;\ldots ,\;x_{n})$ $b_{1},\;\ldots ,\;b_{n}\i |B|$ $A\models \varphi (b_{1},\;\ldots ,\;b_{n})$ $B\models \varphi (b_{1},\;\ldots ,\;b_{n})$ $A$ $B$

Ett elementärt delsystem är elementärt ekvivalent med . Teorier för vars modeller det omvända också är sant – varje elementärt ekvivalent delsystem är elementärt – kallas modell komplett. Modellens fullständighet för en teori motsvarar var och en av följande egenskaper: $B$ $A$ $T$

vilken formel som helst i är ekvivalent med en existentiell formel, $T$
vilken formel som helst i är likvärdig med en universell formel, $T$
att kombinera med ett diagram över valfri modell genererar en komplett teori. $T$

Om är en icke-tom uppsättning, så finns bland alla delsystem inklusive , det minsta, som kallas den genererade uppsättningen . För elementära delsystem, i det allmänna fallet, är ett sådant påstående inte sant. $X\subseteq |A|$ $A$ $X$ $X$

En teori sägs ha termiska Skolem-funktioner om det finns en term för varje formel och formeln följer av teorin . Med andra ord, om det finns ett element där formeln är sann, kan . tas som detta element . Om en teori har termiska Skolem-funktioner, är den modellen komplett. Varje teori har en förlängning , som har termiska Skolem-funktioner. I det här fallet kan varje modell av teorin berikas till teorins modell . $T$ $\varphi (x,\;{\bar y})$ $t_{\varphi }({\bar y})$ $T$ $(\forall {\bar y})((\exists x)\varphi (x,\;{\bar y})\to \varphi (t_{\varphi}({\bar y}),\;{\ stapel y}))$ $\varphi (x,\;{\bar y})$ $t({\bar y})$ $T$ $T^{s}$ $A$ $T$ $A^{s}$ $T^{s}$

Löwenheim-Skolems "upp" -sats säger att om det är ett algebraiskt kardinalitetssystem som inte är mindre än , så har det elementära förlängningar av vilken kardinalitet som helst som är större än eller lika med . $A$ $\alpha =|Th(A)|$ $A$ $\alfa$

Löwenheim-Skolems "nedåt"-sats: om är ett algebraiskt system av kardinalitet och , då har det elementära delsystem av vilken kardinalitet som helst mellan och . $A$ $\alfa$ $\beta =|Th(A)|$ $A$ $\beta$ $\alfa$

Axiomatiserbarhet och stabilitet

En uppsättning formler kallas en uppsättning axiom för en teori om det är en uppsättning konsekvenser . I synnerhet är sig själv en uppsättning axiom för sig själv. Om en teori har en ändlig uppsättning axiom, sägs den vara ändligt axiomatiserbar. $A$ $T$ $T$ $A$ $T$ $T$

Samlingar av algebraiska system kallas klasser. En klass av algebraiska system kallas axiomatiserbara om det är en uppsättning modeller av någon teori . I det här fallet kallas uppsättningen av axiom för också uppsättningen av axiom för . En klass är ändligt axiomatiserbar om och endast om både sig själv och dess komplement är axiomatiserbara. $K$ $T$ $T$ $K$ $K$ $K$

En teori kallas stabil med avseende på supersystem (respektive delsystem) om det för något algebraiskt system följer av och (respektive ) att . En teori är stabil med avseende på delsystem om och endast om den är axiomatiserbar med hjälp av universella formler. En teori är stabil med avseende på supersystem om och bara om den är axiomatiserbar med hjälp av existentiella formler. $T$ $A$ $A\modeller T$ $B\subseteq A$ $A\subseteq B$ $B\modeller T$ $T$ $T$

En teori sägs vara stabil med avseende på homomorfismer om, för något algebraiskt system , följer att , om är en homomorf bild av . En teori är stabil under homomorfismer om och bara om den är axiomatiserbar med hjälp av positiva formler (det vill säga formler som inte innehåller implikation och negation). $T$ $A$ $A\modeller T$ $B\modeller T$ $B$ $A$ $T$

Kedjor

En kedja är en uppsättning algebraiska system, linjärt ordnade av relationen "att vara ett delsystem". Om för elementen i kedjan egenskapen "att vara ett elementärt delsystem" är uppfyllt, kallas kedjan också elementär.

Föreningen av en kedja av algebraiska system ger ett nytt system med samma signatur, som kommer att vara ett supersystem för alla element i kedjan. När en elementär kedja är förenad kommer denna förening att vara ett elementärt supersystem och följaktligen kommer sanningen om alla formler att bevaras i den.

När man kombinerar vilka kedjor som helst (inklusive icke-elementära sådana) bevaras sanningen om -formler, och motsatsen är också sant - om en formel behåller sin sanning när man kombinerar vilka kedjor som helst, då är den likvärdig med någon -formel. $\förallt \finns$ $\förallt \finns$

Teorier som kan axiomatiseras med -formler kallas induktiva. Enligt Chen-Los-Sushko-satsen är en teori induktiv om och endast om den är stabil med avseende på föreningen av kedjor. Ett viktigt exempel på induktiv teori är teorin om fält med fasta egenskaper. $\förallt \finns$ $T$

Kedjemetoden är ett av de viktigaste verktygen för att konstruera algebraiska system med önskade egenskaper.

Ultraprodukter

Låt det vara språk. är en familj av algebraiska system, . En direkt produkt av algebraiska system , är ett algebraiskt system , där för varje predikatsymbol $L$ $\{{\mathcal {A}}_{i}\}_{{i\in I}}$ ${\mathcal {A}}_{i}=\langle M_{i},\;L\rangle$ ${\mathcal {A}}_{i}$ $i\i jag$ $\prod _{{i\in I}}{\mathcal {A}}_{i}=\left\langle \prod _{{i\in I}}A_{i},\;L\right\rangle$ $P\in L$

\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}})

för varje ;

i\i jag

för varje funktionssymbol $f\in L$

(f(a_{1},\;\ldots ,\;a_{{n_{f}}}))_{i}=f(a_{{1i}},\;\ldots ,\;a_{{ n_{f}i}})

och för varje konstant symbol $c\in L$

(c)_{i}=c.

Låt vara ett filter över . Låt oss definiera förhållandet . Låt oss presentera notationen: $D$ $jag$ $\prod _{{i\in I}}A_{i}$ $a\sim _{D}b\Leftrightarrow \{i\in I\mid a_{i}=b_{i}\}\in D$

a/D=\{b\mid b\sim _{D}a\}

\prod _{{i\in I}}A_{i}/D=\left\{a/D\mid a\in \prod _{{i\in I}}A_{i}\right\}.

Vi definierar ett algebraiskt system enligt följande. ${\mathcal {A}}=\left\langle \prod _{{i\in I}}A_{i}/D,\;L\right\rangle$

Låt oss ställa in för predikatsymbolen $P\in L$

{\mathcal {A}}\models P(a_{1},\;\ldots ,\;a_{{n_{P}}})\Leftrightarrow \{i\mid {\mathcal {A}}_{i }\modeller P(a_{{1_{i}}},\;\ldots ,\;a_{{n_{P}i}})\}\i D,

för varje funktionssymbol $f\in L$

f(a_{1}/D,\;\ldots ,\;a_{{n_{f}}}/D)=f(a_{1},\;\ldots ,\;a_{n})/D

och för konstanta symboler $c\in L$

c=c/D.

Det algebraiska systemet som definieras på detta sätt kallas den filtrerade produkten av system av filtret och betecknas med . Om är ett ultrafilter , då kallas det en ultraprodukt , om alla sammanfaller och är lika , då kallas det en ultrakraft och betecknas med . $\mathcal{A}$ ${\mathcal {A}}_{i}$ $D$ $\prod _{{i\in I}}{\mathcal {A}}_{i}/D$ $D$ $\prod _{{i\in I}}{\mathcal {A}}_{i}/D$ ${\mathcal {A}}_{i}$ $\mathcal{A}$ $\prod _{{i\in I}}{\mathcal {A}}_{i}/D$ $\mathcal{A}$ ${\mathcal {A}}^{I}/D$

Den huvudsakliga egenskapen hos ultraprodukter är att de bevarar alla meningar:

Älgens sats. Låt vara ett språk, vara en familj av språkets algebraiska system och vara ett ultrafilter över . Sedan för valfri språkformel och valfri sekvens av element från $L$ $\{{\mathcal {A}}_{i}\}_{{i\in I}}$ $L$ $D$ $jag$ $\varphi (\overline {x})$ $L$ ${\overline {a}}$ $\prod _{{i\in I}}A_{i}$

\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})\}\i D.

Kompakthetssatsen kan också formuleras enligt följande.

Kompakthetssatsen. Om en uppsättning formler är lokalt tillfredsställbar i någon klass , så är den tillfredsställbar i någon ultraprodukt av system från . ${\mathbf {K}}$ ${\mathbf {K}}$ [2]

Typer

Kategorisk

En teori med jämlikhet som har en ändlig eller räkningsbar signatur sägs vara kategorisk i räkningsbar kardinalitet om alla dess räknebara normala modeller är isomorfa . Kategoricitet i en given oräknelig makt definieras på liknande sätt. $T$

Teorin om högre ordningens modeller

Finite Model Theory

Anteckningar

↑ Keisler G., Chen C. Modellteori. — M.: Mir, 1977. — sid. fjorton.
↑ Ershov, 1987 , sid. 117.

Litteratur

Ershov Yu. L. , Palyutin E. A. Matematisk logik. — M .: Nauka, 1987. — 336 sid.
Uppslagsbok om matematisk logik. Del 1. Teori om modeller / red. J. Barwise. — M .: Nauka, 1982. — 392 sid.
Keisler, G.J.; Chen Chun, Chen. Teori om kontinuerliga modeller. - M . : Mir, 1971. - 184 sid.
Keisler, G.J.; Chen Chun, Chen. Teorin om modeller. — M .: Mir, 1977. — 616 sid.

Ordböcker och uppslagsverk

I bibliografiska kataloger
BNF : 119323610 GND : 4114617-7 J9U : 987007541020605171 LCCN : sh85086421 LNB : 000101674 NDL : 00567757 NKC : ph799924

Logik

Filosofi • Semantik • Syntax • Historia

Logiska grupper

klassisk logik	Aristotelisk logik propositionell logik Första beställningslogik Andra ordningens logik högre ordningslogik
matematisk logik	mängdteori Modellteori Beräkningsbarhetsteori Bevisteori och konstruktiv matematik Linjär logik formellt system naturlig slutsats Sekvenskalkyl Algebra av logik Relevant logik Deontisk logik intuitionistisk logik Lambek kalkyl
Icke-klassisk logik	intuitionism rolig logik Substrukturell logik logik Beskrivningslogik Flervärdig logik Logisk syntes Bindande logik Temporal logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritiskt tänkande informell logik deduktiva resonemang

Komponenter

Bortförande (logik)
Sannolikhet
påstående
Avdrag / Induktion / Traduktion
Verklighet
induktivt resonemang
slutledning
boolesk konstant
Sann
logiskt följa
Logisk form
Nödvändiga och tillräckliga förutsättningar
Beskrivning
Definition
Utbyte
Paket
Kontrovers ( Antinomy )
Syntetisk bedömning / Analytisk bedömning
Länk

Lista över booleska symboler