Несуперечність, повнота і розв’язуваність числення висловлень

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

Метатеорема 2 (МТ2). Кожна теорема числення висловлень є тавтологією.

МТ2 встановлює дуже важливу властивість теорем числення висловлень. Вона дає впевненість у тому, що серед теорем числення висловлень не має жодної формули, відмінної від тотожно істиної.

Цю властивість називають несуперечністю відносно істинності, несуперечністю відносно інтерпретації або семантичною несуперечністю.

Метатеорема 2 іноді формулюється так:

Числення висловлень – теорія семантично не суперечна.

Введемо тепер поняття не суперечності, яке на відміну від семантичної несуперечності, є незалежним від інтерпретації.

Означення. Теорія 𝔂 називається внутрішньо несуперечною або несуперечною в класичному розумінні, якщо не існує формули 𝔄, вираженої в термінах 𝔙, такої що 𝔄 і ┐𝔄 одночасно є теоремами теорії 𝔙. Теорія, яка не є внутрішньою суперечною, назив. внутрішньо суперечною.

Метатеорема 3(МТ3). Числення висловлень – теорія внутрішньо не суперечна.

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

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

Теорія, яка не є синтаксично несуперечною, називається синтаксично суперечною.

Лема. Для довільної формули числення висловлень 𝔄(,…, ) має місце вивідність ,…, ├𝔄(,…, ).

Метатеорема 5(МТ5). Для довільної формули числення висловлень 𝔄, якщо ├ 𝔄, то 𝔄, тобто, якщо 𝔄 – тавтологія, то 𝔄- теорема.

Доведена в МТ5 властивість числення висловлень називається семантичною повнотою, або повнотою відносно інтерпретації, або повнотою в широкому розумінні.

Розв’язувальним методом, для формальної теорії L називають метод за допомогою якого для довільної формули 𝔄 із L можна за скінченне число кроків визначити, чи буде 𝔄 теоремою L, чи ні.

Проблема вирішення для L полягая в тому, щоб знати розв’язувальний метод для L, або довести що такого методу немає.

У першому випадку кажуть що проблема вирішення для L розв’язується позитивно, а у другому – негативно. У першому випадку теорію L називають розв’язною, в другому нерозв’язною.

Метатеорема 6(МТ6). Числення висловлень- теорія розв’язна.

Доведення. Нехай 𝔄 – довільна формула числення висловлень. Застосуємо до неї один з відомих алгоритмів перевірки 𝔄 на тавтологію. Складемо для 𝔄 таблицю істинності і розглянемо її останній стовпчик. Це звичайно можна зробити за скінченне число кроків. Якщо виявиться, що 𝔄 – тавтологія (останній стовпчик містить таблиці буде містити лише одиниці), то за МТ5 𝔄 – теорема.Якщо 𝔄 – не тавтологія (останній стовпчик таблиці істиності містить хоча б один нуль), то за МТ2 (за її контрапозицією) 𝔄 не є теоремою.

Означення. Підмножину А множини аксіом теорії L називать незалежною, якщо жодну аксіому з А не можна вивести за допомогою правил виводу теорії L з аксіом L, які не входять в А.