Oberoende i första ordningens logik — definition och exempel
Oberoende i första ordningens logik: tydlig definition, konkreta exempel och skillnaden mot oavgörbarhet i en teori — guide för studenter och forskare.
I matematisk logik är en mening oberoende av en teori av första ordningen om teorin inte kan användas för att bevisa att meningen är sann eller falsk. Ibland talar man också om att meningen är "oavgörbar", men detta har inget att göra med begreppet avgörbarhet som i lösningen av ett beslutsproblem.
Formell definition
Låt T vara en teori i första ordningen (en mängd axiomsatser) och låt φ vara en mening i samma språk. Vi säger att φ är oberoende av T precis när
T ⊬ φ och T ⊬ ¬φ,
det vill säga varken φ eller dess negation kan härledas ur T med det givna bevisregelsystemet.
Semantisk karaktärisering
Tack vare Gödel:s fullständighetssats för första ordningens logik kan man också uttrycka oberoende semantiskt: φ är oberoende av T (under antagandet att T är konsistent) precis när både T ∪ {φ} och T ∪ {¬φ} är satisfierbara, alltså har modeller. Med andra ord finns det en modell M av T med M ⊨ φ och en modell N av T med N ⊨ ¬φ.
Observera att begreppet är relativt: samma mening kan vara oberoende av en teori men följas av en annan, beroende på vilka axiomer som ingår i teorin. Om T är inkonsistent är begreppet meningslöst i praktiken, eftersom en inkonsistent teori härleder alla meningar.
Vanliga exempel
- Euclidias parallellaxiom: Det klassiska exemplet är Euklides femte postulat (parallellaxiomet), som är oberoende av de andra euklidiska axiomen. Genom att antaga eller förkasta detta axiom får man olika icke-ekvivalenta geometrier (hyperbolisk respektive elliptisk geometri).
- Kontinuitetshypotesen (CH): Inom mängdteori är Cantors kontinuitetshypotes ett välkänt exempel. Gödel visade att CH är konsekvent med ZF (finns modell där CH gäller) under antagandet att ZF är konsistent, och Cohen visade genom forcing att ¬CH också är konsekvent med ZF. Därmed är CH oberoende av ZF (och även av ZFC).
- Valbarhetsaxiomet (AC): Axiom om val är ett annat klassiskt exempel: AC är varken bevisbart eller motbevisbart utifrån ZF, vilket innebär att det är oberoende av ZF (givet ZF:s konsistens).
- Satser i aritmetik: Gödel:s ofullständighetssatser visar att för varje tillräckligt stark, rekursivt axiomatiseerbar och konsekvent teori för aritmetik (t.ex. Peanoaritmetik) finns aritmetiska satser som är oberoende av teorin.
Metoder för att bevisa oberoende
Att visa att en mening är oberoende av en teori innebär normalt att konstruera två modeller: en modell där meningen är sann och en annan där dess negation är sann. Vanliga tekniker och verktyg är:
- Gödel:s konstruktiva universum L: används för att visa relativ konsistens (t.ex. att en sats kan hålla i en särskild inre modell).
- Cohen-forcing: en kraftfull metod för att bygga modeller där vissa satser blir sanna eller falska (bl.a. använd för kontinuitetshypotesen).
- Kompakthets- och uppräknelighetsmetoder: inom modellteorin används teknik som kompakthetsatsen och ultraprodukter för att konstruera modeller med önskade egenskaper.
- Syntaktiska konsistensbevis: ibland visar man relativ konsistens genom att reducera den ena teorin till en annan.
Skillnad mellan "oavgörbar" och "oberoende"
Terminologin kan vara förvirrande: när man säger att en mening är oavgörbar i relation till en teori menas ofta just att den är oberoende (varken bevisbar eller motbevisbar) av teorin. Däremot används ordet oavgörbar också i en annan mening inom datavetenskap och logik för att beskriva ett beslutproblem utan algoritmisk lösning — detta är en annan typ av "oavgörbarhet" och ska inte blandas ihop med satsens oberoende av en given axiomatisk teori.
Konsekvenser
När en sats är oberoende av en teori innebär det praktiskt att man fritt kan lägga till satsen eller dess negation som nytt axiom och därigenom få olika konsistenta utvidgningar av teorin, förutsatt att den ursprungliga teorin är konsekvent. Detta spelar en viktig roll i förståelsen av vilka frågor som kan avgöras enbart med givna axiomer och vilka som kräver nya antaganden.
Frågor och svar
F: Vad betyder självständighet inom matematisk logik?
S: Inom matematisk logik avser oberoende en mening som inte kan bevisas vara sann eller falsk med hjälp av en teori av första ordningen.
F: Hur talar man ibland om en oberoende mening?
S: En oberoende mening kallas ibland för "oavgörbar", även om denna term inte är relaterad till begreppet att lösa ett beslutsproblem.
F: Vad är en första ordningens teori?
S: En första ordningens teori är en uppsättning axiom och slutledningsregler som kan användas för att bevisa eller motbevisa meningar.
F: Kan en oberoende mening bevisas vara sann eller falsk med hjälp av en första ordningens teori?
S: Nej, en oberoende mening kan inte bevisas vara sann eller falsk med hjälp av en första ordningens teori, eftersom den inte är beroende av teorin.
F: Vad är skillnaden mellan oberoende och decidabilitet i matematisk logik?
S: Oberoende avser en mening som inte kan bevisas vara sann eller falsk med hjälp av en första ordningens teori, medan avgörbarhet avser förmågan att lösa ett beslutsproblem.
F: Hur refererar man till en oberoende mening?
S: Vissa kallar en oberoende mening för "oavgörbar", men det är inte korrekt eftersom det inte har något att göra med konceptet att avgöra ett problem.
F: Hur viktigt är det att förstå oberoende i matematisk logik?
S: Att förstå oberoende är viktigt inom matematisk logik eftersom det gör det möjligt för oss att identifiera satser som inte kan bevisas eller motbevisas med hjälp av en första ordningens teori, vilket kan bidra till att informera framtida matematisk forskning.
Sök