Глобальные свойства теории P

Лемма об истинности при фиксированной оценке и ее следствие.

Введенное нами понятие вывода из гипотез сохраняет истинность формул при фиксирован- ной модели и фиксированной оценке.

Лемма 5.1. Пусть Γ — список формул X₁, X₂, ..., X_m и Γ ⊢ Y. Если для данной модели M и данной оценки θ формул X₁, X₂, ..., X_m, Y в M истинны X₁θ, X₂θ, ..., X_mθ, то и Yθ в M истинна.

◀Доказательство проводится индукцией по длине вывода. Утверждение очевидно, если вывод содержит одну формулу, которая в этом случае есть либо аксиома (являющаяся логическим законом), либо гипотеза X_j. Но тогда Y θ и X_jθ — одно и то же.

Предположим утверждение доказано для всех выводов длины менее k. Рассмотрим произвольный вывод Z₁, Z₂, . . . , Z_k из гипотез Γ длины k с конечной формулой Y = Z_k. Формула Y есть либо логический закон, либо гипотеза, либо получена по правилу модус поненс, либо по правилу всеобщности. В первых двух случаях рассуждения те же, что и при k = 1. В третьем случае в выводе есть формулы Z_j и Z_l = Z_j → Y . В силу предположения индукции формулы Z_j θ и (Z_j → Y )θ истинны в M . В этом случае правило модус поненс гарантирует истинность в M формулы Y θ.

Если Y получена по правилу обобщения из формулы Z_j для некоторого j, то Y = ∀xZ_j. В силу структурного требования формула Z_j получена из гипотез X_i1 , . . . , X_is , каждая из которых не имеет свободных вхождений переменной x. Для всякого объекта a того же сорта, что и x из истинности формул X_i следует истинность (X_i)^xa (это то же самое, что и X_i). В силу индуктивного предположения заключаем, что M |= ((Z_j)^xa)θ, а в силу интерпретации квантора всеобщности это равносильно истинности (∀x X)θ, т.е. Y θ▶

Следствие 5.1. Если Γ ⊢ X и все формулы в Γ являются логическими законами, то и X есть логический закон. В частности, если ⊢ X, то X — логический закон.