Modelteori

Modelteori er en gren af matematisk logik , der beskæftiger sig med studiet af forholdet mellem formelle sprog og deres fortolkninger eller modeller. Navnemodelteorien blev først foreslået af Alfred Tarski i 1954 . Den vigtigste udvikling af teorien om modeller var i værkerne af Tarski, Maltsev og Robinson .

Oprindelse

Modelteori er helliget studiet af det grundlæggende forhold mellem syntaks og semantik . Samtidig svarer det formelle sprog til det første i det , og modellen svarer til det andet - en matematisk struktur , der tillader en vis beskrivelse af dette sprog. Modelteori opstod som en generalisering af eksisterende tilgange til løsning af metamatematiske problemer relateret til algebra og matematisk logik . Disse tilgange har i sig selv eksisteret i lang tid, men i lang tid blev de ikke betragtet i deres helhed inden for rammerne af et enkelt logisk-filosofisk paradigme . Et naturligt eksempel i denne sammenhæng er problemet forbundet med Euklids femte postulat om parallelle linjer. I århundreder lykkedes det ikke matematikere at bevise dens sandhed, indtil Bolyai og Lobachevsky i det 19. århundrede byggede ikke-euklidisk geometri , og derved viste, at det parallelle postulat hverken kan bevises eller tilbagevises. Fra modelteoriens synspunkt betyder det, at systemet af aksiomer uden det femte postulat tillader flere forskellige modeller, det vil sige i dette tilfælde flere muligheder for at implementere geometrien.

Således voksede den oprindelige teori om modeller ud af sådanne grene af matematik som logik , universel algebra , mængdeteori som en generalisering og udvidelse af eksisterende viden. Derfor dukkede de første resultater af modelteori op længe før dens "officielle" udseende. Löwenheim-Skolem-sætningen ( 1915 ) anses for at være det første resultat af denne art [1] . Et andet stort resultat var kompakthedssætningen , bevist af Gödel ( 1930 ) og Maltsev ( 1936 ).

Klassisk førsteordens modelteori

Modelteori for klassisk førsteordenslogik er historisk set det første og mest udviklede eksempel på en modelteoretisk tilgang. Modellernes rolle her spilles af sæt, der repræsenterer rækken af mulige værdier af variabler . Funktionssymboler fortolkes som operationer af den tilsvarende aritet på dem og prædikater som relationer (for flere detaljer, se Førsteordens logik, fortolkning ).

Kompakthedssætning

Et af de vigtigste værktøjer inden for modelteori er kompaktitetssætningen bevist af Maltsev , som siger, at et sæt af førsteordens formler har en model, hvis og kun hvis modellen har hver endelig delmængde af dette sæt af formler.

Navnet på sætningen kommer af, at det kan angives som et udsagn om kompaktheden af et stenrum .

Det følger af kompakthedssætningen, at nogle begreber ikke kan udtrykkes i førsteordens logik. For eksempel kan begreberne endelighed eller tællelighed ikke udtrykkes med nogen formler af første orden eller endda deres mængder: hvis et sæt formler har vilkårligt store endelige modeller, så har det også en uendelig model. På samme måde har en teori, der har en uendelig model, hvis kardinalitet ikke er mindre end signaturens kardinalitet, modeller af enhver større kardinalitet.

Kompaktitetsteoremet finder anvendelse til at konstruere ikke-standardiserede modeller af klassiske teorier, såsom elementær aritmetik eller calculus .

Teorier og elementær ækvivalens

En teori er et sæt formler, der er lukket med hensyn til deducerbarhed (kort sagt lukket), altså sådan et sæt , at hvis formlen følger af , så hører den til . $T$ $T$ $\varphi$ $T$ $\varphi$ $T$

En teori, der har mindst én model, kaldes konsistent, de andre teorier kaldes modstridende.

En teori kaldes komplet, hvis teorien for en formel indeholder eller . Hvis er et algebraisk system, danner sættet af sande på lukkede formler en komplet teori - teorien om systemet , betegnet med . $T$ $\varphi$ $\varphi$ $\likke \varphi$ $EN$ $EN$ $EN$ $Th(A)$

Hvis på algebraiske systemer og de samme lukkede formler er sande, så siges og at være elementært ækvivalente . Altså og er elementært ækvivalente, hvis og kun hvis de er modeller af den samme komplette teori. $EN$ $B$ $EN$ $B$ $EN$ $B$

Hvis en komplet teori har en endelig model , så er alle modeller af teorien isomorfe , især indeholder de alle det samme antal elementer. For endelige algebraiske systemer falder begreberne elementær ækvivalens og isomorfi derfor sammen. $T$ $EN$ $T$ $EN$

Delsystemer og Löwenheim-Skolem-sætninger

Et algebraisk system kaldes et undersystem af et algebraisk system, hvis fortolkningen af hvert signatursymbol i er en begrænsning af dets fortolkning i mængden . Et undersystem kaldes elementært hvis for enhver formel og for enhver det har: hvis og kun hvis . Systemet kaldes i disse tilfælde en (elementær) udvidelse af systemet . $B$ $EN$ $|B|\subseteq |A|$ $B$ $EN$ $|B|$ $\varphi (x_{1},\;\ldots ,\;x_{n})$ $b_{1},\;\ldots ,\;b_{n}\i |B|$ $A\modeller \varphi (b_{1},\;\ldots ,\;b_{n})$ $B\modeller \varphi (b_{1},\;\ldots ,\;b_{n})$ $EN$ $B$

Et elementært delsystem svarer elementært til . Teorier, for hvis modeller det modsatte også er sandt - hvert elementært ækvivalent undersystem er elementært - kaldes model komplet. Modellens fuldstændighed af en teori svarer til hver af følgende egenskaber: $B$ $EN$ $T$

enhver formel i svarer til en eksistentiel formel, $T$
enhver formel i svarer til en universel formel, $T$
at kombinere med et diagram af enhver model genererer en komplet teori. $T$

Hvis er et ikke-tomt sæt, så er der blandt alle undersystemer inklusive , det mindste, som kaldes det genererede sæt . For elementære undersystemer, i det generelle tilfælde, er en sådan erklæring ikke sand. $X\subseteq |A|$ $EN$ $x$ $x$

En teori siges at have termiske Skolem-funktioner, hvis der findes et udtryk for hver formel, og formlen følger af teorien . Med andre ord, hvis der er et element, hvor formlen er sand, kan . tages som dette element . Hvis en teori har termiske Skolem-funktioner, så er den modelfuldendt. Hver teori har en udvidelse , som har termiske Skolem-funktioner. I dette tilfælde kan hver model af teorien beriges til teorimodellen . $T$ $\varphi (x,\;{\bar y})$ $t_{\varphi }({\bar y})$ $T$ $(\forall {\bar y})((\eksisterer x)\varphi (x,\;{\bar y})\til \varphi (t_{\varphi}({\bar y}),\;{\ bar y}))$ $\varphi (x,\;{\bar y})$ $t({\bar y})$ $T$ $T^{s}$ $EN$ $T$ $A^{s}$ $T^{s}$

Löwenheim-Skolems "op" -sætning siger, at hvis er et algebraisk kardinalitetssystem ikke mindre end , så har det elementære forlængelser af enhver kardinalitet større end eller lig med . $EN$ $\alpha =|Th(A)|$ $EN$ $\alfa$

Löwenheim-Skolems "ned"-sætning: hvis er et algebraisk system af kardinalitet og , så har det elementære undersystemer af enhver kardinalitet mellem og . $EN$ $\alfa$ $\beta =|Th(A)|$ $EN$ $\beta$ $\alfa$

Aksiomatiserbarhed og stabilitet

Et sæt formler kaldes et sæt af aksiomer for en teori, hvis det er et sæt konsekvenser . Især sig selv er et sæt aksiomer for sig selv. Hvis en teori har et endeligt sæt af aksiomer, så siges det at være endeligt aksiomatiserbart. $EN$ $T$ $T$ $EN$ $T$ $T$

Samlinger af algebraiske systemer kaldes klasser. En klasse af algebraiske systemer kaldes aksiomatiserbare, hvis det er et sæt modeller af en eller anden teori . I dette tilfælde kaldes sættet af aksiomer for også sættet af aksiomer for . En klasse er endeligt aksiomatiserbar, hvis og kun hvis både sig selv og dens komplement er aksiomatiserbare. $K$ $T$ $T$ $K$ $K$ $K$

En teori kaldes stabil med hensyn til supersystemer (henholdsvis undersystemer), hvis det for et hvilket som helst algebraisk system følger af og (henholdsvis ) at . En teori er stabil med hensyn til delsystemer, hvis og kun hvis den er aksiomatiserbar ved hjælp af universelle formler. En teori er stabil med hensyn til supersystemer, hvis og kun hvis den kan aksiomatiseres ved hjælp af eksistentielle formler. $T$ $EN$ $A\modeller T$ $B\subseteq A$ $A\subseteq B$ $B\modeller T$ $T$ $T$

En teori siges at være stabil med hensyn til homomorfismer, hvis det for ethvert algebraisk system følger , at hvis er et homomorfisk billede af . En teori er stabil under homomorfismer, hvis og kun hvis den er aksiomatiserbar ved hjælp af positive formler (det vil sige formler, der ikke indeholder implikation og negation). $T$ $EN$ $A\modeller T$ $B\modeller T$ $B$ $EN$ $T$

Kæder

En kæde er et sæt algebraiske systemer, lineært ordnet efter relationen "at være et undersystem". Hvis for kædens elementer egenskaben "at være et elementært delsystem" er opfyldt, så kaldes kæden også elementær.

Foreningen af en kæde af algebraiske systemer giver et nyt system med samme signatur, som vil være et supersystem for alle elementer i kæden. Når en elementær kæde er forenet, vil denne forening være et elementært supersystem, og som følge heraf vil sandheden af alle formler blive bevaret i den.

Når man kombinerer nogen kæder (inklusive ikke-elementære), bevares sandheden af -formler, og det modsatte er også sandt - hvis en formel bevarer sin sandhed, når den kombinerer nogen kæder, så svarer den til en -formel. $\foralt \eksisterer$ $\foralt \eksisterer$

Teorier, der kan aksiomatiseres af -formler, kaldes induktive. Ifølge Chen-Los-Sushko-sætningen er en teori induktiv, hvis og kun hvis den er stabil med hensyn til forening af kæder. Et vigtigt eksempel på induktiv teori er teorien om felter med fast karakteristik. $\foralt \eksisterer$ $T$

Kædemetoden er et af de vigtigste værktøjer til at konstruere algebraiske systemer med ønskede egenskaber.

Ultraprodukter

Lad det være sprog. er en familie af algebraiske systemer, . Et direkte produkt af algebraiske systemer , er et algebraisk system , hvor for hvert prædikat symbol $L$ $\{{\mathcal {A}}_{i}\}_{{i\in I}}$ ${\mathcal {A}}_{i}=\langle M_{i},\;L\rangle$ ${\mathcal {A}}_{i}$ $i\i I$ $\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}})

for hver ;

i\i I

for hvert funktionssymbol $f\in L$

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

og for hvert konstant symbol $c\in L$

(c)_{i}=c.

Lad være et filter over . Lad os definere forholdet . Lad os introducere notationen: $D$ $jeg$ $\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 definerer et algebraisk system som følger. ${\mathcal {A}}=\left\langle \prod _{{i\in I}}A_{i}/D,\;L\right\rangle$

Lad os indstille for prædikatsymbolet $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,

for hvert funktionssymbol $f\in L$

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

og for konstante symboler $c\in L$

c=c/D.

Det algebraiske system defineret på denne måde kaldes det filtrerede produkt af systemer af filteret og betegnes med . Hvis er et ultrafilter , så kaldes det et ultraprodukt , hvis alle sammenfalder og er ens , så kaldes det en ultrapower og betegnes 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 vigtigste egenskab ved ultraprodukter er, at de bevarer alle sætninger:

Elks sætning. Lad være et sprog, være en familie af algebraiske systemer af sproget , og være et ultrafilter over . Derefter for enhver sprogformel og enhver sekvens af elementer fra $L$ $\{{\mathcal {A}}_{i}\}_{{i\in I}}$ $L$ $D$ $jeg$ $\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.

Kompakthedssætningen kan også formuleres som følger.

Kompakthedssætningen. Hvis et sæt formler er lokalt tilfredsstillende i en eller anden klasse , så er det tilfredsstillende i et eller andet ultraprodukt af systemer fra . ${\mathbf {K}}$ ${\mathbf {K}}$ [2]

Typer

Kategorisk

En teori med lighed, der har en endelig eller tællig signatur, siges at være kategorisk i tællelig kardinalitet , hvis alle dens tællelige normale modeller er isomorfe . Kategoricitet i en given utallig magt defineres på samme måde. $T$

Teorien om højere-ordens modeller

Finite Model Theory

Noter

↑ Keisler G., Chen C. Modelteori . — M.: Mir, 1977. — s. fjorten.
↑ Ershov, 1987 , s. 117.

Litteratur

Ershov Yu. L. , Palyutin E. A. Matematisk logik. — M .: Nauka, 1987. — 336 s.
Opslagsbog om matematisk logik. Del 1. Teori om modeller / udg. J. Barwise. — M .: Nauka, 1982. — 392 s.
Keisler, G.J.; Chen Chun, Chen. Teori om kontinuerlige modeller. - M . : Mir, 1971. - 184 s.
Keisler, G.J.; Chen Chun, Chen. Teorien om modeller. — M .: Mir, 1977. — 616 s.

Ordbøger og encyklopædier

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

Logikker

Filosofi • Semantik • Syntaks • Historie

Logiske grupper

klassisk logik	Aristotelisk logik propositionel logik Første ordens logik Anden ordens logik højere ordens logik
matematisk logik	mængdeteori Modelteori Beregnelighedsteori Bevisteori og konstruktiv matematik Lineær logik formelt system naturlig konklusion Sekvensberegning Algebra af logik Relevant logik Deontisk logik intuitionistisk logik Lambek regning
Ikke-klassisk logik	intuitionisme sløret logik Substrukturel logik logik Beskrivelseslogik Flerværdilogik Logisk syntese Bindende logik Tidsmæssig logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritisk tænkning uformel logik deduktiv ræsonnement

Komponenter

Bortførelse (logik)
Sandsynlighed
udmelding
Fradrag / Induktion / Traduktion
Virkelighed
Induktiv begrundelse
slutning
boolsk konstant
Rigtigt
logisk følge
Logisk form
Nødvendige og tilstrækkelige betingelser
Beskrivelse
Definition
Substitution
Pakke
Kontrovers ( Antinomy )
Syntetisk dømmekraft / Analytisk dømmekraft
Link

Liste over booleske symboler