Metalogisk

Metalogik är studiet av logikens metateori . Medan logik studerar hur logiska system kan användas för att konstruera giltiga och sunda argument , studerar metalogik egenskaperna hos logiska system. Logik avser de sanningar som kan härledas med hjälp av ett logiskt system; metalogic handlar om de sanningar som kan härledas om de språk och system som används för att uttrycka sanningar.

De grundläggande föremålen för metallisk studie är formella språk, formella system och deras tolkningar . Studiet av tolkning av formella system är den gren av matematisk logik som är känd som modellteori , och studiet av deduktiva system är den gren som är känd som bevisteori .

Översikt

Formellt språk

Ett formellt språk är en organiserad uppsättning symboler , vars symboler exakt definierar det genom form och plats. Ett sådant språk kan därför definieras utan hänvisning till betydelsen av dess uttryck; den kan existera innan någon tolkning tilldelas den – det vill säga innan den har någon mening. Första ordningens logik uttrycks i något formellt språk. En formell grammatik avgör vilka symboler och uppsättningar av symboler som är formler i ett formellt språk.

Ett formellt språk kan formellt definieras som en uppsättning A av strängar (ändliga sekvenser) på ett fast alfabet α. Vissa författare, inklusive Rudolf Carnap , definierar språket som det ordnade paret <α, A >. Carnap kräver också att varje element i α måste förekomma i minst en sträng i A .

Formationsregler

Formationsregler (även kallade formell grammatik ) är en exakt beskrivning av ett formellt språks välformade formler . De är synonyma med uppsättningen strängar över alfabetet i det formella språket som utgör välformade formler . Den beskriver dock inte deras semantik (dvs vad de betyder).

Formella system

Ett formellt system (även kallat en logisk kalkyl , eller ett logiskt system ) består av ett formellt språk tillsammans med en deduktiv apparat (även kallad ett deduktivt system ). Den deduktiva apparaten kan bestå av en uppsättning transformationsregler (även kallade inferensregler ) eller en uppsättning axiom , eller ha båda. Ett formellt system används för att härleda ett uttryck från ett eller flera andra uttryck.

Ett formellt system kan formellt definieras som en ordnad trippel <α, ${\mathcal {I}}$ , ${\mathcal {D}}$ d>, där ${\mathcal {D}}$ d är förhållandet mellan direkt härledning. Denna relation förstås i en omfattande mening så att de primitiva meningarna i det formella systemet tas som direkt härledbara från den tomma uppsättningen meningar. Direkt härledning är en relation mellan en mening och en ändlig, möjligen tom uppsättning meningar. Axiom är så valda att varje första platsmedlem av ${\mathcal {D}}$ d är en medlem av ${\mathcal {I}}$ och varje andraplatsmedlem är en finit delmängd av ${\mathcal {I}}$ .

Ett formellt system kan också definieras med endast relationen ${\mathcal {D}}$ d. Därmed kan ${\displaystyle {\mathcal {I}}} och α$ utelämnas i definitionerna av tolkat formellt språk och tolkat formellt system . Denna metod kan dock vara svårare att förstå och använda.

Formella bevis

Ett formellt bevis är en sekvens av välformade formler för ett formellt språk, varav den sista är ett teorem för ett formellt system. Satsen är en syntaktisk konsekvens av alla välformade formler som föregår den i bevissystemet. För att en välformad formel ska kvalificera sig som en del av ett bevis, måste den härröra från att tillämpa en regel från den deduktiva apparaten i något formellt system på de tidigare välformade formlerna i bevissekvensen.

Tolkningar

En tolkning av ett formellt system är tilldelningen av betydelser till symbolerna och sanningsvärdena till meningarna i det formella systemet. Studiet av tolkningar kallas formell semantik . Att ge en tolkning är synonymt med att konstruera en modell .

Viktiga distinktioner

Metaspråk–objektspråk

I metalogik kallas formella språk ibland för objektspråk . Språket som används för att göra uttalanden om ett objektspråk kallas ett metaspråk . Denna distinktion är en nyckelskillnad mellan logik och metalogik. Medan logik handlar om bevis i ett formellt system , uttryckt i något formellt språk, handlar metalogik om bevis om ett formellt system som uttrycks i ett metaspråk om något objektspråk.

Syntax–semantik

Inom metalogiken har 'syntax' att göra med formella språk eller formella system utan hänsyn till någon tolkning av dem, medan 'semantik' har att göra med tolkningar av formella språk. Termen "syntaktisk" har en något bredare räckvidd än "bevisteoretisk", eftersom den kan tillämpas på egenskaper hos formella språk utan några deduktiva system, såväl som på formella system. 'Semantisk' är synonymt med 'modellteoretisk'.

Användning–nämn

Inom metalologin antar orden "använda" och "nämna", i både deras substantiv- och verbformer, en teknisk betydelse för att identifiera en viktig distinktion. Distinktionen användning –omnämnande (ibland kallad distinktionen ord-som-ord ) är skillnaden mellan att använda ett ord (eller en fras) och att nämna det. Vanligtvis anges att ett uttryck nämns snarare än att det används genom att omsluta det inom citattecken, skriva ut det i kursiv stil eller sätta uttrycket för sig självt på en rad. Att omsluta ett uttryck inom citattecken ger oss namnet på ett uttryck, till exempel:

"Metalogic" är namnet på den här artikeln.

Den här artikeln handlar om metalogik.

Typ – token

Typ -token distinktionen är en distinktion inom metalogik, som skiljer ett abstrakt begrepp från de objekt som är särskilda instanser av begreppet. Till exempel är den speciella cykeln i ditt garage ett tecken på den typ av sak som kallas "cykeln". Medan cykeln i ditt garage är på en viss plats vid en viss tidpunkt, är det inte sant för "cykeln" som används i meningen: "Cykeln har blivit mer populär nyligen." Denna distinktion används för att klargöra innebörden av symboler för formella språk .

Historia

Aristoteles tid . Det var dock först med framväxten av formella språk i slutet av 1800-talet och början av 1900-talet som undersökningar av logikens grunder började blomstra. År 1904 David Hilbert att när man undersöker matematikens grunder förutsätts logiska föreställningar, och därför krävdes en samtidig redogörelse för metalliska och metamatematiska principer. Idag är metalogik och metamatematik till stor del synonyma med varandra, och båda har i hög grad subsumerats av matematisk logik i akademin. En möjlig alternativ, mindre matematisk modell kan hittas i skrifter av Charles Sanders Peirce och andra semiotiker .

Resultat

Resultat inom metalogik består av sådant som formella bevis som visar konsistensen , fullständigheten och avgörbarheten hos särskilda formella system .

Viktiga resultat inom metalogik inkluderar:

Bevis på oräkneligheten av potensmängden för de naturliga talen ( Cantors sats 1891)
Löwenheim–Skolem teorem ( Leopold Löwenheim 1915 och Thoralf Skolem 1919)
Bevis på konsekvensen av sanningsfunktionell propositionell logik ( Emil Post 1920)
Bevis på den semantiska fullständigheten av sanningsfunktionell propositionell logik ( Paul Bernays 1918), (Emil Post 1920)
Bevis på den syntaktiska fullständigheten av sanningsfunktionell propositionell logik (Emil Post 1920)
Bevis på avgörbarheten av sanningsfunktionell propositionell logik (Emil Post 1920)
Bevis på konsistensen av första ordningens monadiska predikatlogik ( Leopold Löwenheim 1915)
Bevis på den semantiska fullständigheten av första ordningens monadiska predikatlogik (Leopold Löwenheim 1915)
Bevis på avgörbarheten av första ordningens monadiska predikatlogik (Leopold Löwenheim 1915)
Bevis på konsistensen av första ordningens predikatlogik ( David Hilbert och Wilhelm Ackermann 1928)
Bevis på den semantiska fullständigheten av första ordningens predikatlogik ( Gödels fullständighetsteorem 1930)
Bevis på cut-elimineringssatsen för den efterföljande kalkylen ( Gentzens Hauptsatz 1934)
Bevis på oavgörbarheten hos första ordningens predikatlogik ( Kyrkans teorem 1936)
Gödels första ofullständighetsteorem 1931
Gödels andra ofullständighetsteorem 1931
Tarskis odefinierbarhetsteorem (Gödel och Tarski på 1930-talet)

Se även

^ Harry Gensler, Introduktion till logik , Routledge, 2001, s. 336.
^ ^a ^b ^c ^d ^e Hunter, Geoffrey , Metalogic: An Introduction to the Metatheory of Standard First-Order Logic , University of California Press, 1973
^ ^a ^b Rudolf Carnap (1958) Introduktion till symbolisk logik och dess tillämpningar, sid. 102.
^ Hao Wang, Reflektioner över Kurt Gödel

externa länkar

Media relaterade till Metalogic på Wikimedia Commons
Dragalin, AG (2001) [1994], "Meta-logic" , Encyclopedia of Mathematics , EMS Press

[1] Harry Gensler, Introduktion till logik , Routledge, 2001, s. 336.

[metalogic-2] Hunter, Geoffrey , Metalogic: An Introduction to the Metatheory of Standard First-Order Logic , University of California Press, 1973

[itslaia-3] Rudolf Carnap (1958) Introduktion till symbolisk logik och dess tillämpningar, sid. 102.

[reflections-4] Hao Wang, Reflektioner över Kurt Gödel