Наши партнеры
— невыводимость предложения некоторой теории из данного множества ее предложений, напр. из системы ее аксиом. Система аксиом называется независимой (неизбыточной), если каждая входящая в нее аксиома невыводима из других аксиом. Если какую-то аксиому можно вывести из остальных, ее можно исключить из списка аксиом, при этом исходная теория не изменится, класс доказуемых в ней предложений останется тем же.
Зависимая система аксиом содержит лишние аксиомы и в этом смысле является менее совершенной, чем независимая.
Требование Н. распространяется и на правилавывода аксиоматической теории. Исходное правило вывода независимо, если оно не может быть получено в качестве производного правила в системе, из которой оно исключено. Можно также сказать, что аксиома или правило вывода независимы, если существует теорема, которая не может быть доказана без этой аксиомы или этого правила вывода.
Н. имеет по преимуществу эстетическую и дидактическую ценность. Исследование Н. способствует, как правило, лучшему пониманию строения изучаемой теории и ее возможностей.
Исторически первым доказательством Н. было доказательство невыводимости пятого постулата Евклида о параллельных из остальных его постулатов.
Требование Н. может быть распространено не только на аксиомы и правила вывода аксиоматических теорий, но и на исходные их термины (понятия). Термин независим, если он неопределим через остальные исходные термины. Теория с неизбыточным исходным словарем не содержит лишних понятий и является в этом отношении более совершенной, чем теория с зависимыми понятиями.
Зависимость некоторой аксиомы от остальных показывается путем вывода ее из них. Н. аксиомы можно доказать, найдя свойство, присущее всем другим аксиомам и не присущее рассматриваемой.
НЕКЛАССИЧЕСКАЯ ЛОГИКА,см.: Логика неклассическая.