Числення висловлень і алгебра висловлень. Основні проблеми числення висловлень, Детальна інформація

Нарешті, розглянемо ще одну важливу проблему для формальних теорій.

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

Зрозуміло, що аксіому, яку можна вивести з інших, можна виключити зі системи аксіом, і при цьому множина теорем теорії залишиться тією ж самою (тобто отримаємо рівносильне числення). Отже, залежна система аксіом у певному розумінні менш досконала, ніж незалежна система, бо вона містить зайві аксіоми.

Можна довести, що системи аксіом числень висловлень ЧВ і ЧВ1 є незалежними.

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