Metalogic , studiet och analysen av semantiken (sambandet mellan uttryck och betydelser) och syntax (samband mellan uttryck) av formella språk och formella system. Det är relaterat till, men inkluderar inte, den formella behandlingen av naturliga språk. (För en diskussion om syntax och semantik för naturliga språk, se lingvistik och semantik.)
Natur, ursprung och influenser av metalogic
Syntax och semantik
Ett formellt språk kräver vanligtvis en uppsättning formningsregler - dvs. en fullständig specifikation av de typer av uttryck som ska räknas som välformade formler (meningar eller meningsfulla uttryck), tillämpliga mekaniskt, i den meningen att en maskin kan kontrollera om en kandidat uppfyller kraven. Denna specifikation innehåller vanligtvis tre delar: (1) en lista med primitiva symboler (basenheter) som ges mekaniskt, (2) vissa kombinationer av dessa symboler, som utpekas mekaniskt som bildande av de enkla (atom) meningarna, och (3) en uppsättning induktiva klausuler - induktiva i den mån de föreskriver att naturliga kombinationer av givna meningar bildas av sådana logiska förbindelser som disjunktionen "eller", som symboliseras "∨"; "Inte", symboliserade "∼"; och "för alla", symboliserade "(∀)," är återigen meningar. [“(∀)” kallas en kvantifierare,som också "det finns några", symboliserade "(∃)".] Eftersom dessa specifikationer endast handlar om symboler och deras kombinationer och inte med betydelser, involverar de endast språkets syntax.
En tolkning av ett formellt språk bestäms genom att formulera en tolkning av atomens meningar i språket med avseende på en domän av objekt - dvs genom att bestämma vilka objekt av domänen som betecknas med vilka konstanter av språket och vilka relationer och funktioner som är betecknas med vilka predikatbokstäver och funktionssymboler. Sanningsvärdet (oavsett om det är "sant" eller "falskt") för varje mening bestäms således enligt standardtolkningen av logiska anslutningar. Till exempel är p · q sant om och bara om p och qär sanna. (Här betyder punkten sammankopplingen ”och”, inte multiplikationsoperationen ”gånger.”) Med tanke på vilken tolkning som helst av ett formellt språk erhålls således ett formellt sanningsbegrepp. Sanning, mening och denotation är semantiska begrepp.
Om det dessutom införs ett formellt system på ett formellt språk, uppstår vissa syntaktiska begrepp - nämligen axiom, inferensregler och teorem. Vissa meningar utpekas som axiomer. Dessa är (grundläggande) satser. Varje slutregel är en induktiv klausul som säger att, om vissa meningar är satser, så är en annan mening relaterad till dem på ett lämpligt sätt också en sats. Om till exempel p och “antingen inte p eller q ” (∼ p ∨ q ) är satser, så är q en sats. I allmänhet är en sats antingen ett axiom eller slutsatsen av en slutsatsregel vars förutsättningar är satser.
1931 gjorde Kurt Gödel den grundläggande upptäckten att i de flesta intressanta (eller betydelsefulla) formella system inte alla sanna meningar är satser. Det följer av denna upptäckt att semantik inte kan reduceras till syntax; Därför måste syntax, som är nära besläktad med bevisteori, ofta skiljas från semantik, som är nära relaterad till modellteori. Grovt sett är syntax - som tänkt i matematikens filosofi - en gren av talteori, och semantik är en gren av uppsättningsteori, som handlar om aggregatens natur och relationer.
Historiskt, när logik och axiomatiska system blev mer och mer exakta, uppstod, som svar på en önskan om större klarhet, en tendens att ägna större uppmärksamhet åt de syntaktiska egenskaperna hos de använda språken snarare än att koncentrera sig uteslutande på intuitiva betydelser. På detta sätt konvergerade logiken, den axiomatiska metoden (som den som används i geometri) och den semiotiska (den allmänna vetenskapen om tecken) mot metalogik.
Den axiomatiska metoden
Det mest kända axiomatiska systemet är det av Euclid för geometri. På ett sätt som liknar Euklids involverar varje vetenskaplig teori en mängd meningsfulla begrepp och en samling sanna eller troda påståenden. Betydelsen av ett begrepp kan ofta förklaras eller definieras i termer av andra begrepp, och på samma sätt kan sanningen i ett påstående eller anledningen till att tro att det vanligtvis klargöras genom att indikera att det kan härledas från vissa andra påståenden som redan är accepterade. Den axiomatiska metoden fortsätter i en sekvens av steg, som börjar med en uppsättning primitiva begrepp och propositioner och sedan definierar eller drar alla andra begrepp och propositioner i teorin från dem.
Förståelsen som uppstod på 1800-talet att det finns olika möjliga geometrier ledde till en önskan att separera abstrakt matematik från rumslig intuition; följaktligen upptäcktes många dolda axiomer i Euklids geometri. Dessa upptäckter organiserades i ett mer rigoröst axiomatiskt system av David Hilbert i hans Grundlagen der Geometrie (1899; The Foundations of Geometry ). I detta och relaterade system tas dock logiska anslutningar och deras egenskaper för givet och förblir implicita. Om den inblandade logiken anses vara den för predikatberäkningen kan logikern sedan komma fram till sådana formella system som det som diskuterats ovan.
När sådana formella system väl erhållits är det möjligt att omvandla vissa semantiska problem till skarpare syntaktiska problem. Man har till exempel hävdat att icke-euklidiska geometrier måste vara självkonsistenta system eftersom de har modeller (eller tolkningar) i euklidisk geometri, som i sin tur har en modell i teorin om reella tal. Man kan dock fråga sig hur det är känt att teorin om reella tal är konsekvent i den meningen att ingen motsägelse kan härledas inom den. Självklart kan modellering bara skapa en relativ konsistens och måste stoppas någonstans. Efter att ha kommit till ett formellt system (säg med verkliga siffror) har konsistensproblemet dock det skarpare fokus för ett syntaktiskt problem:det att överväga alla möjliga bevis (som syntaktiska objekt) och fråga om någon av dem någonsin har (säg) 0 = 1 som sista meningen.
Som ett annat exempel kan frågan huruvida ett system är kategoriskt - det vill säga om det i huvudsak bestämmer en unik tolkning i den meningen att två tolkningar är isomorfa - undersökas. Denna semantiska fråga kan till viss del ersättas med en relaterad syntaktisk fråga, den fullständighet: huruvida det i systemet finns någon mening som har ett bestämt sanningsvärde i den avsedda tolkningen så att varken den meningen eller dess negation är en sats. Även om det nu är känt att de semantiska och syntaktiska begreppen är olika, klargörs det vaga kravet på att ett system ska vara "adekvat" av båda begreppen. Studien av sådana skarpa syntaktiska frågor som konsekvens och fullständighet, som betonades av Hilbert, utsågs av honom till "metamatematik" (eller "bevissteori") omkring 1920.
