Непротиворечивая система аксиом называется независимой, если ни одна из аксиом этой системы не может быть выведена из остальных аксиом как теорема. В противном случае система аксиом называется зависимой.
Для иллюстрации этого свойства обратимся снова к геометрической теории, основанной на аксиоматике Гильберта. Ясно, что непосредственная проверка независимости каждой из 20 аксиом затруднительна. История V постулата "Начал" Евклида является поучительным тому примером. Четвертый постулат о конгруэнтности всех прямых углов впоследствии был доказан как логическое следствие других аксиом и постулатов (точнее, других "очевидных" утверждений). Возник вопрос о независимости или прямом доказательстве следующего, пятого постулата о параллельных прямых. Тем более что как бы "половина доказательства" аксиомы параллельности уже была известна. Более двух тысяч лет предпринимались попытки доказать одно из двух: либо то, что V постулат есть логическое следствие других "более очевидных" утверждений, либо то, что он не доказывается исходя из каких–либо "очевидных" утверждений, аксиом и постулатов. Обсуждением той роли, которую сыграл V постулат в теории познания вообще и в математике в частности, мы займемся чуть позже.
Возникает вопрос. Существует ли эффективное достаточное условие для проверки независимости какого–либо утверждения А от системы аксиом Т (проверенной уже на совместность)? Такое условие существует и для совместной системы аксиом формируется следующим образом в терминах реализаций.
Пусть Т – непротиворечивая система аксиом. Утверждение (аксиома) А не зависит от системы Т, если вместе с некоторой реализацией R1 (Т , А) системы Т и А существует некоторая реализация R2(T, ùA) системы Т и ùА.
Доказательство. Пусть существует реализация R2(T, ùA) системы Т и ù А и пусть ТА. Тогда реализация R2(T, ùA) содержит вместе со свойством ùА и его отрицание А=ù (ùА), что несовместимо с понятием реализации. Следовательно, предположение Т А (о том, что А следует из Т) неверно.