Modellteori

Den modellen teori er en gren av matematisk logikk . Innholdet i modellteorien er forholdet mellom de rent formelle uttrykkene for et språk ( syntaktisk nivå ) og deres betydning ( semantisk nivå ). Dette forholdet er etablert ved hjelp av såkalte tolkninger og et matematisk forhold som kalles oppfyllelsesforholdet .

Generelt handler modellteori om konstruksjon og klassifisering av alle (mulige) strukturer og klasser av strukturer, spesielt med strukturer som tilsvarer aksiomatiserbare språk eller teorier. Dette inkluderer blant annet. oppgaven med å konstruere modeller for et gitt aksiomsystem - det handler ofte om modeller med tilleggsegenskaper som ikke kan spesifiseres i aksiomsystemet, f.eks. B. kardinaliteten til modellen. Videre handler modellteori om ekvivalens av modeller , for eksempel spørsmålet om de samme utsagnene gjelder i dem og spørsmålet om hvor mange (ikke-isomorfe) modeller av et aksiomsystem det er.

Grunnleggende begreper i modellteori

En modell i betydningen modellteori er et sett med en viss struktur (kalt univers, område av individer, bæresett eller domene) som et sett med utsagn gjelder.

Det faktum at støttesettet har en struktur betyr at visse forhold er definert, dvs. delmengder av kartesiske produkter . Universets tufle og relasjonene kalles struktur. En struktur kalles en modell for en uttalelse hvis utsagnet kan tolkes som en uttalelse om strukturen og oppfylles der.

Eksempel. De enkleste strukturene inkluderer grafer . En graf er en tupel med . Universet ville være her, og (i dette tilfellet bare) forholdet ville være . For å tolke en uttalelse som "Julian og Chelsea er venner" i , kan man (i dette tilfellet, siden det ikke er noen annen relasjon) tolke det som et vennskapsforhold; Julian og Chelsea måtte identifiseres med individer fra universet . Hvis da , ville uttalelsen være tilfreds i strukturen og være en modell for uttalelsen. Men hvis det var tomt, ville det ikke være noen måte å stemme på en slik måte at de er venner, og proposisjonen ville ikke bli oppfylt i denne strukturen .

Mer generelt vurderes ikke bare ett utsagn, men et sett med utsagn på et språk. Modellteori behandler spørsmålet om hvilke modeller som oppfyller hver setning av settet, eller om settet i det hele tatt har en modell.

Den første vanskeligheten er å bestemme hvilke strukturer som kan brukes som modeller for uttalelsene til et språk. For dette formålet ble begrepet signatur introdusert, som søker å dele hver setning i språket i emne og predikat. Emner kan være egennavn (hvert språk snakker om bestemte objekter og bruker noen ganger egennavn for dem), variabler (pronomen, for å si det så er de ikke egennavn, men refererer til objektene språket snakker om) eller termer (andre mulige fag). Den grunnleggende ideen i modellteori er,

- variabler med nulsifrede forhold,
- Egennavn med ensifrede forhold som bare inneholder ett element,
- Begreper med funksjoner (disse er venstre totalt, høyre entydige relasjoner) og
- Prediker med de andre relasjonene

å assosiere. Hvor generelle definisjonene blir gjort, avhenger av sammenhengen: I kategoriteori prøver man å gå veldig generelt, innen datavitenskap mye mindre generelt, i matematikk begrenser man seg ofte til et enkelt språk (første nivå predikatlogikk). Derfor er det ingen ensartede definisjoner. For detaljer, se hovedoppføringene.

signatur

En signatur er en tuple som består av tre sett og en funksjon.

  • er settet med symboler for relasjoner,
  • er settet med symboler for funksjoner,
  • er settet med symboler for konstanter,
  • er en funksjon som tildeler arity til hvert symbol .

Settene og må være sammenhengende parvis, men de skal også være tomme. I prinsippet kan de også være uendelige, men som regel er de endelige. Elementene fra kalles ikke-logiske symboler .

struktur

Vær en signatur. A - struktur er en tuple som består av:

  • en ikke-tom mengde , universet ,
  • et k-sted-forhold for hvert symbol for k-sted-forhold ,
  • en k-sifferfunksjon for hvert k-siffer-funksjonssymbol ,
  • ett element for hvert konstante symbol fra K.

tolkning

Vær et språk med variabler, egennavn, termer og predikater. En tolkning av i en struktur er en assosiasjon

  • det individuelle navnet til konstantene til ,
  • vilkårene for funksjonene til ,
  • av predikatene om de andre relasjonene til .

En oppgave er en oppgave

  • av variablene på universet av .

En tolkning er derfor mulig hvis språket samsvarer med signaturen. Tolkningen og oppgaven gir en uttalelse om strukturen . Oppdraget er som oftest definert som en del av tolkningen.

Modell og tilfredshetsforhold

Vær hvilket som helst språk og en delmengde av språket. En struktur kalles en modell for om det er en tolkning (med en oppgave) slik at hvert element tilsvarer en påstand som oppfylles i strukturen. Symbolsk :, talt: oppfylt , eller er også sant i .

Modellteoretisk konklusjon

Når det gjelder modellteori, sies det at en uttalelse følger av en uttalelse hvis hver modell av også er en modell for . Symbolsk .

Slutningsforholdet utvides deretter til ethvert sett med utsagn: Når det gjelder modellteori , følger et sett med utsagn fra et sett med utsagn hvis hver modell av er en modell for . Symbolsk .

Den teorien om en modell er forstått å være mengden av alle uttalelser som gjelder for det. Hver teori om en modell er komplett , det vil si at det er en eller for hver uttalelse .

På viktigheten av modeller

  • Et sett med aksiomer kan ofte gis lettere som en teori om en modell enn i en oppsatt form.
  • Eksistensen av en modell beviser at aksiomene ikke motsier hverandre, så de er konsistente. En logikk har egenskapen til fullstendighet hvis omvendt hvert konsistent sett med utsagn har en modell (dette gjelder førsteordens predikatlogikk , se nedenfor ).
  • Hvis det er modeller med en bestemt egenskap, så vel som modeller som ikke har denne egenskapen, så er den logiske uavhengigheten av eiendommen fra aksiomene bevist. Det vil si at denne egenskapen ikke følger av aksiomene, og den kan heller ikke tilbakevises på grunnlag av aksiomene.
  • Hver setning i et formelt språk induserer et sett med endelige modeller som tilfredsstiller det. Hvert språk kan således sees på som foreningen av alle modeller som oppfylles av setningene i språket. Et språk kalles da definierbart i en logikk hvis det er et forslag om logikk som oppfylles av det samme settet med modeller. I den deskriptive kompleksitetsteorien ble forholdet mellom trykk- kompleksitetsklassen til et språk og dets definerbarhet studert i visse logikker.

Eksempler på modeller

Tette ordrer

Det ordnede settet med rasjonelle tall er en modell for aksiomene til de tette åpne strenge totalordrene :

  1. (Trikotomi)
  2. (Antisymmetri)
  3. (Transitivitet)
  4. (Åpenhet)
  5. (Tetthet)

Det ordnede settet med reelle tall og alle delmengder av reelle tall som inneholder rasjonelle tall er modeller. Teorien om tette åpne strenge totalordrer er et standardeksempel i modellteori. Den har blant annet følgende egenskaper:

  • Den er endelig aksiomatiserbar, men har ingen endelige modeller.
  • Den er komplett og modell komplett .
  • Alle tellbare modeller er isomorfe (for bevis ), i utallige hovedtall er det ikke-isomorfe modeller. På modellteoriens språk betyr dette: Det er - kategorisk , men ikke kategorisk i utallige hovedtall: Hvis et utellelig hovednummer, så har denne teorien ikke-isomorfe modeller for kraft .
  • Det er den (utvetydig bestemte) modellkameraten til teorien om den lineære ordenen.
  • Med de rasjonelle tallene har den en hovedmodell . (Dette er en modell som fundamentalt kan være innebygd i en hvilken som helst annen modell.)
  • Hver modell er atomisk .
  • Den har kvantifiseringseliminering .
  • Det er ikke stabilt .

Ett element universer

Ettelementsuniverset, som bare inneholder konstanten c, er en modell for aksiomet over signaturen .

Et eksempel på to-element modeller

Hvordan kan en modell for følgende sett med utsagn om se ut? ( være en konstant, være et tosifret forhold)

Den første utsagnet bestemmer at universet inneholder maksimalt to elementer, den andre og tredje utsagnet gjelder bare hvis det inneholder to elementer. Med unntak av isomorfisme er det bare to modeller ( basert på universet ):

og

Modellen

er isomorf til . (Det er en isomorfisme som på kart og videre .)

Utilfredsstillende aksiomer

Uttalelsessettet

kan ikke oppfylles, det vil si at den ikke har noen modell.

Viktige setninger i modellteori

Kriterier for sett med uttalelser fra førsteordens predikatlogikk kan bli funnet som garanterer eksistensen av modeller.

  • For eksempel sier Gödels teorem om fullstendighet at enhver syntaktisk konsistent teori (dvs. hvert sett med lukkede formler som ingen logisk motsetning kan utledes fra) har en modell.
  • Den kompakte teorem sier at en (uendelig) aksiom systemet har en modell hvis og bare hvis alle endelig delsystem har en modell.
  • Den Löwenheim-Skolem teorem også sier at hver teori (i en tellbar språket predikatlogikk) som har en uendelig modell i det hele tatt har også en modell av hver uendelig kardinalitet .

Endelig modellteori

Den endelige modellteorien er en del av modellteorien, logikken om egenskapene til språk (for eksempel predikatlogikk ), samt begrensede strukturer som endelige grupper, grafer, og de fleste maskinmodeller er fokusert. Et fokus er spesielt på forholdet mellom logiske språk og teorien om beregbarhet . Det er også nære lenker til diskret matematikk , kompleksitetsteori og teori om databaser .

Typiske spørsmål i endelig modellteori er kardinalitetene som modeller kan lages for et gitt system av aksiomer . Så dette spørsmålet er helt svarte for kroppen aksiomer : Primtall og primtall krefter er de eneste kardinalitetene av begrensede modeller. Dette settet med naturlige tall kalles da spekteret av kroppsaksiomer .

Det er ennå ikke avklart om komplementet til et spektrum alltid er et spektrum: Vi ser etter et sett med aksiomer slik at alle endelige modeller har en kardinalitet i komplementet til spektret. Dette spørsmålet er også relatert til P-NP-problemet fra kompleksitetsteori .

Om modellteoriens historie

Opprinnelsen til modellteori finnes i 1800-tallets algebra, som presentert i Ernst Schöders omfattende arbeid : Forelesninger om logikkalgebra (1890–1905). Det sentrale området var individets område (på den tiden også kalt tankeområdet ) som et algebraisk uttrykk ble brukt på. Schröder introduserte også strukturbegrepet. Men vilkårene forble udefinerte. Denne tradisjonen fortsatte selv med matematikere med en logisk og aksiomatisk disposisjon som Ernst Zermelo , som da han aksiomatiserte mengdeteori, også la begrepet individuelt domene uten definisjon, selv om hans aksiomatisering var basert på begrepet. Selv Albert Thoralf Skolem , som prøvde å avklare noen av begrepene Zermelos, brukte begrepet uten nærmere forklaring.

Det første forsøket på formalisering kan bli funnet med Rudolf Carnap. Men moderne modellteori avviker fra hans oppfatning på viktige punkter. Han relaterte modeller (som det var vanlig den gangen) til aksiomsystemer og ikke sett med proposisjoner, slik at et aksiomsystem allerede hadde en modell hvis aksiomene til systemet er oppfylt. Av viktige grunner er dette ikke lenger nødvendig i den moderne unnfangelsen. Carnap forsto en modell for de grunnleggende aksiomatiske tegnene til et gitt aksiomatisk system med hensyn til et gitt domene for individer som følger: en evaluering for disse tegnene på en slik måte at både domenet og evalueringen er gitt uten bruk av beskrivende konstanter. En modell for grunntegnene kalles en modell for et aksiomsystem hvis det tilfredsstiller alle aksiomer, dvs. H. blir sant.

Gjennombruddet til moderne forståelse kom med Alfred Tarski, som skilt semantikken til et aksiomsystem fra syntaksen og prioriterte semantikken fremfor syntaksen: En syntaktisk konklusjon er riktig hvis den blir semantisk oppfylt. Andre viktige milepæler er Herbrand-strukturen av Jacques Herbrand (1930) og definisjonen av sannhet av Tarski og Robert Vaught i aritmetiske utvidelser av relasjonssystemer (1956), som fjernet noe av utilgjengeligheten av Tarskis opprinnelige definisjon av sannhet fra 1930-tallet. Arbeidet til Anatoli Malzew var spesielt viktig for applikasjonene i algebra. Allerede i 1936 inkluderte han språk med et utallig antall logiske symboler.

Se også

litteratur

weblenker

Individuelle bevis

  1. Carnap, Rudolf: Introduksjon til symbolsk logikk. Springer, Wien, New York, 3. utg. 1968, s. 174