Oberoendet av ett system av axiom är en egenskap hos axiomsystemet för en given axiomteori, som består i det faktum att varje axiom är oberoende, det vill säga det är inte en logisk konsekvens av uppsättningen av andra axiom i denna teori . Ett system av axiom med denna egenskap kallas oberoende.
Oberoendet av ett eller annat axiom för en given axiometori innebär att detta axiom kan ersättas av dess negation utan motsägelse. Med andra ord är ett axiom oberoende om och endast om det finns en tolkning där detta axiom är falskt och alla andra axiom i den givna teorin är sanna. Konstruktionen av en sådan tolkning är en klassisk metod för att bevisa oberoende.
När man konstruerar en axiomatisk teori i form av ett formellt system, där relationen av logisk konsekvens formaliseras i form av begreppet härledning, anses ett axiom vara oberoende om det inte kan härledas från andra axiom med hjälp av härledningsreglerna i detta formell. systemet. För en bred klass av formella system (de så kallade första ordningens teorier) sammanfaller oberoende med avseende på härledning med oberoende med avseende på logisk konsekvens.
I förhållande till formella system och kalkyler i allmänhet är det meningsfullt att tala om slutledningsreglernas oberoende. En slutledningsregel sägs vara oberoende om det finns ett teorem för den givna kalkylen som inte kan härledas utan att använda denna regel.
Oberoendet av ett system av axiom är inte i sig en nödvändig egenskap hos en axiomatisk teori. Det indikerar bara att helheten av de första bestämmelserna i teorin inte är överflödiga, och presenterar vissa tekniska bekvämligheter.
Studier om oberoendet av axiomsystemet och bevis på oberoende bidrar dock till en bättre förståelse av teorin som studeras. Det räcker med att påminna om vilket inflytande frågan om oberoendet av Euklids femte postulat i geometrisystemets axiom hade på matematikens utveckling.