Незалежність системи аксіом - властивість системи аксіом даної аксіоматичної теорії, яке у тому, що кожна аксіома є незалежною, тобто не є логічним наслідком з безлічі інших аксіом цієї теорії. Система аксіом, що має цією властивістю, називається незалежною.

Незалежність тієї чи іншої аксіоми даної аксіоматичної теорії означає, що цю аксіому можна без протиріччя замінити її запереченням. Іншими словами, аксіома незалежна в тому і тільки в тому випадку, якщо мається інтерпретація, при якій ця аксіома помилкова, а всі інші аксіоми цієї теорії правдиві. Побудова такої інтерпретації є класичним методом докази незалежності.

При побудові аксіоматичної теорії у вигляді формальної системи, де відношення логічного слідування формалізується у вигляді поняття виводимості, аксіома вважається незалежною, якщо вона не може бути виведена з інших аксіом за допомогою правил виведення даної формальної системи. Для широкого класу формальних систем (так званих теорій 1-го порядку) незалежність щодо виводимості збігається з незалежністю щодо логічного слідування.

По відношенню до формальних систем і взагалі численням має сенс говорити про незалежність правил виводу. Правило виводу називаються незалежним, якщо існує теорема даного числення, яка не може бути виведена без використання цього правила.

Незалежність системи аксіом сама по собі не є обов'язковою властивістю аксіоматичної теорії. Вона лише свідчить про те, що сукупність вихідних положень теорії не є надмірною, і представляє деякі технічні зручності. Однак дослідження, присвячені незалежності системи аксіом, і докази незалежності сприяють кращому розумінню досліджуваної теорії. Досить згадати, який вплив на розвиток математики надав питання про незалежність п'ятого постулату Евкліда в системі аксіом геометрії.