Числення предикатiв. Теорiя першого порядку, Детальна інформація

Поняття виведення (доведення) формули, поняття теореми, виведення формули з множини гiпотез означаються у численнi предикатiв аналогiчно тому, як це було зроблено у численнi висловлень. Мають мiсце також теореми, подiбнi до теорем 5.5 i 5.6 числення висловлень.

Теорема 5.7. Будь-яка вивiдна формула (теорема) числення предикатiв є тотожно iстиною (логiчно загальнозначущою) формулою.

Ця теорема доводиться аналогiчно теоремi 5.5. Спочатку безпосередньо перевiряється, що всi аксiоми є лзз формулами. Вiдтак, доводиться, що усi правила виведення зберiгають властивiсть лзз.

Теорема 5.8. Будь-яка тотожно iстинна предикатна формула є вивiдною (теоремою) в численнi предикатiв.

Доведення цiєї теореми досить складне i тут не наводитиметься.

З останнiх теорем випливає твердження, подiбне до твердження теореми 5.1.

Теорема 5.9. Предикатнi формули A i B рiвносильнi тодi i тiльки тодi, коли формула ((A(B)((B(A)) є вивiдною в численнi предикатiв, тобто є лзз.

Як i ранiше, для скорочення виразу ((A(B)((B(A)) вводять операцiю ~ i записують даний вираз у виглядi (A~B). Отже, останню теорему можна переформулювати так: формули A i B рiвносильнi (A = B) тодi i тiльки тодi, коли формула (A~B) є вивiдною в численнi предикатiв.

Оскiльки, як вже зазначалось вище, встановлення рiвносильностi формул у логiцi предикатiв є задачею значно складнiшою, нiж у логiцi висловлень, то дуже важливе значення останнього твердження полягає у тому, що цю задачу можна звести до пошуку формального виведення для вiдповiдної формули.

Побудоване числення предикатiв називають численням предикатiв першого порядку, або теорiєю першого порядку. У такiй теорiї аргументами фунцiй i предикатiв, а також змiнними, що зв’язуються кванторами, можуть бути лише предметнi змiннi. У численнях другого i вищих порядкiв аргументами предикатiв можуть бути i предикати, а квантори можуть зв’язувати i предикатнi змiннi, тобто допустимi вирази, наприклад, вигляду (P(P(x)). Застосування таких числень зустрiчається значно рiдше, тому в математичнiй логiцi їм придiляють менше уваги.