Розділ «4.2. Класична символічна логіка»

Аксіоматична побудова числення висловлювань

Логічні системи такого типу називаються гільбертовськими за ім'ям німецького математика Д. Гільберта (1862-1943). Порівняно із системами натурального числення в численнях гільбертовського типу формальна структура доведення суттєво відрізняється від логічної будови звичних міркувань.

У процесі побудови числень висловлювань гільбертовського типу вибирають кінцевий запас логічних тотожностей як аксіом і зазначають правила, за допомогою котрих можна отримати з аксіом нові логічні тотожності як теорем відповідної логічної системи.

Розглянемо систему 5, в якій аксіомами є такі формули: А, А (В -" А)

Єдиним правилом виводу є правило модус поненс (А -> В, А) -> В.

Доведення в системі 8 формули будується в такий спосіб. На будь-якому кроці доведення можна визначити:

1. Одну із аксіом.

2. Формулу, що слідує із раніше визначених формул за правилом модус поненс.

Доведення формули Р вважають побудованим, якщо відповідно до 1-2 отримуємо послідовність формул, що завершуються формулою Р. Наприклад, доведення формули А А будують так. Доведення:

Металогічна оцінка логіки висловлювань