Logikkens historie

Utvikling av modellteori

Resultater som de oppnådd av Gödel og Skolem var tydeligvis semantiske - eller, som de fleste logikere foretrekker å si, modellteoretikk. Likevel ble det ikke utviklet noen generell teori om logisk semantikk i noen tid. Den tyskfødte filosofen Rudolf Carnap prøvde å presentere en systematisk teori om semantikk i Logische Syntax der Sprache (1934; The Logical Syntax of Language), Introduction to Semantics (1942), og Meaning and Necessity (1947). Arbeidene hans fikk likevel skarp filosofisk kritikk, spesielt fra Quine, som frarådet andre logikere å følge Carnaps tilnærming.

De tidlige arkitektene av det som nå kalles modellteori var Tarski og den tyskfødte matematikeren Abraham Robinson. Deres første interesse var hovedsakelig i modellteorien for forskjellige algebraiske systemer, og deres endelige mål var kanskje en slags universell algebra, eller generell teori om algebraiske strukturer. Imidlertid var resultatet av et intensivt arbeid av Tarski og hans medarbeidere på slutten av 1950-tallet og begynnelsen av 60-tallet ikke så mye en generell teori, men et vell av modellteoretiske begreper og metoder. Noen av disse begrepene gjaldt klassifiseringen av forskjellige typer modeller — for eksempel som “fattigste” (atommodeller) eller “rikeste” (mettede modeller). Mer detaljerte studier av forskjellige typer modeller ble utført i det som er kjent som stabilitetsteori, hovedsakelig på grunn av den israelske logikeren Saharon Shelah.

En viktig utvikling innen modellteori var teorien om infinitærlogikk, som var pioner under Tarskis innflytelse av den amerikanske logikeren Carol Karp og andre. En logisk formel kan være uendelig på forskjellige måter. Opprinnelig ble uendelig bare behandlet i forbindelse med uendelig lange disjunksjoner og konjunksjoner. Senere ble det lagt inn uendelig lange sekvenser av kvantifiserere. Fortsatt senere ble logikk hvor det kan være uendelig lange synkende kjeder med underformler av noe slag, studert. For slike setninger kan ikke Tarski-definisjoner av sannhet brukes, siden de forutsetter eksistensen av minimale atomformler som den sannhet for lengre formler er definert. Infinitary logikker dermed bedt om utviklingen av noncompositional sannhets definisjoner, som opprinnelig ble formulert i forhold til tanken om et utvalg spill.

Bruken av spill for å definere sannhet førte til slutt til utviklingen av et helt felt av semantikk, kjent som spillteoretisk semantikk, som kom til konkurrerende semantiske teorier av Tarski-typen (se spillteori). Spillene som brukes til å definere sannhet i denne semantikken er ikke formelle teorem-spill som beviser, men spilles "utendørs" blant individene i det relevante diskursuniverset.

Grensesnitt mellom bevisteori og modellteori

Noen av de viktigste utviklingstrekkene i logikk i andre halvdel av 1900-tallet involverte ideer fra både bevisteori og modellteori. For eksempel oppdaget Evert W. Beth og andre i 1955 at bevis av gentzen-type kunne tolkes som frustrerte motmodellkonstruksjoner. (Den samme tolkningen ble uavhengig foreslått for en tilsvarende bevisteknikk kalt tremetoden av den finske filosofen Jaakko Hintikka.) For å vise at G er en logisk konsekvens av F prøver man på trinnvis å beskrive en modell der F er sant, men G usant. Et bokholder for slike konstruksjoner ble av Beth kalt et semantisk tablå eller bord. Hvis den forsøkte moteksempel på konstruksjon fører til en blindvei i form av en eksplisitt motsetning i alle mulige retninger, kan ikke G unnlate å være sant hvis F er; med andre ord, G er en logisk konsekvens av F. Det viser seg at reglene for tablåkonstruksjon er syntaktisk identiske med kuttfrie sekvensregler av gentzen-type lest i motsatt retning.

Enkelte ideer som har sin opprinnelse i sammenheng med Hilbertisk bevisteori, har ført til innsikt om modellteoretisk betydning av de ordinære språkkvantifisererne hver og en (og selvfølgelig deres symbolske motstykker). En metode som ble brukt av Hilbert og hans medarbeidere var å tenke på jobben med kvantifiserere som utført av passende valgbegrep, som Hilbert kalte epsilon-termer. Den ledende ideen blir grovt uttrykt som følger. Logikken i en eksistensiell proposisjon som "Noen brøt vinduet" kan forstås ved å studere den tilsvarende instanserte setningen "John Doe brøt vinduet," der "John Doe" ikke refererer til noen bestemt person, men i stedet står for en muligens ukjent person hvem gjorde det. (Slike postulerte eksempler på individer kalles noen ganger “vilkårlige individer.”) Hilbert ga regler for bruk av epsilon-termer og viste at alle kvantifiserere kan erstattes av dem.

Den resulterende epsilonberegningen illustrerer de dynamiske aspektene ved betydningen av kvantifiserere. Spesielt blir ikke meningen deres uttømt av ideen om at de "spenner over" en viss klasse av verdier. Den andre hovedfunksjonen til kvantifiserere er å indikere avhengigheter mellom variabler når det gjelder de formelle avhengighetene mellom kvantifiseringspunktene som variablene er bundet til. Selv om det ikke er noen variabler på vanlig språk, kan et verbalt eksempel brukes for å illustrere ideen om en slik avhengighet. For at setningen “Alle har minst en fiende” skal være sanne, må det eksistere, for en gitt person, minst ett ”vitneindivid” som er hans fiende. Siden fiendens identitet avhenger av det gitte individet, kan fiendens identitet betraktes som verdien av en viss funksjon som tar det gitte individet som et argument. Dette kommer til uttrykk teknisk ved å si ganske enkelt at i eksemplet setning, kvantifiserer noen avhenger av kvantifiserer alle.

Funksjonene som stiller ut avhengighetene til variabler på hverandre i en setning med førsteordens logikk ble først vurdert av Skolem og er kjent som Skolem-funksjoner. Deres betydning indikeres av det faktum at sannhet for førsteordens setninger kan defineres i form av dem: en førsteordens setning er sann hvis, og bare hvis det finnes en fullstendig rekke Skolem-funksjoner. På denne måten kan forestillingen om sannhet håndteres i situasjoner der Tarski-definisjoner av sannhet ikke er anvendelige. Faktisk har logikere spontant brukt definisjoner av Skolem-funksjon (eller deres ekvivalenter) når definisjoner av Tarski-type mislykkes, enten fordi det ikke er noen utgangspunkt for den typen rekursjon som Tarski bruker eller på grunn av en mislykkethet av komposisjonalitet.

Når man innser hvordan avhengighetsforhold mellom kvantifiseringsmidler kan brukes til å representere avhengighetsrelasjoner mellom variabler, blir det også klart at den mottatte behandlingen av kvantifiseringsmidler som går tilbake til Frege og Russell er mangelfull ved at mange perfekt mulige avhengighetsmønstre ikke kan representeres i den. Årsaken er at omfanget av kvantifiserere har en begrenset struktur som begrenser mønstrene de kan reprodusere. Når disse restriksjonene fjernes systematisk, oppnår man en rikere logikk, kjent som “uavhengighetsvennlig” førsteordenslogikk, som først ble redegjort for av Jaakko Hintikka på 1990-tallet. Noen av de grunnleggende logiske og matematiske begrepene som ikke kan uttrykkes i vanlig førsteordens logikk, ble uttrykkelige i uavhengighetsvennlig logikk på førsteordens nivå, inkludert likeverdighet, uendelighet og sannhet. (Dermed kan sannhet for et gitt førsteordens språk nå uttrykkes i det samme førsteordens språket.) En sannhetsdefinisjon er mulig fordi sannhet ikke er en komposisjonsattributt i uavhengighetsvennlig logikk. Oppdagelsen av uavhengighetsvennlig logikk førte til en ny undersøkelse av mange aspekter av samtidens logiske teori.