Аксіоматика і правила виведення

4.3.1 Мета занять

Ознайомитися з аксіоматикою числення предикатів, основними властивостями теорій першого порядку.

4.3.2 Методичні вказівки з організації самостійної роботи роботи студентів

При вивченні теоретичного матеріалу зверніть увагу на те, що ЧВ дозволяє доводити теореми для внутрішніх потреб логіки, а ЧП дозволяє описувати і доводити теореми для конкретних областей математики. Крім математики, ЛП дозволяє формулювати співвідношення між елементами реального миру та виводити подібні відношення як теореми у математиці. Як і в ЧВ, у ЧП розглядаються аксіоматичні системи та системи природного виведенння. Використовуйте конспект лекцій та літературу: [1; 4, с. 90-98; 7, с. 228-238; 8; 9, с. 197-209].

Розглянемо числення предикатів першого порядку К, яке визначається аксіоматичним шляхом. Аксіоми поділяються на два класи: логічні аксіоми і власні аксіоми. Логічні аксіоми: для будь-яких А, В, С Î К формули

(П1)

(П2)

(П3)

(П4) "х_i А(х_i) ® А(t), де А(х_i) є формула із К і t є терм із К, вільний для х_i в А(х_i);

(П5) "х_i (А ® В) ® (А ® "х_i В), якщо формула А не включає вільних входжень х_i, є аксіомами числення К.