3.10 Найдите результат подстановки константы a вместо X в формулу из задачи 3.4.

Когда мы намереваемся рассмотреть подстановки вместо переменной v в некоторую формулу, удобно обозначать эту формулу выражением F(v), и обозначать результат подстановки терма t вместо v в этой формуле через F(t) .

3.11 Если V не является свободной переменной f(V), тогда f(t) равно f(V).

Пусть F(x) обозначает формулу

" y (P(y) Й Q(x, y)),

предложенную выше как перевод условия ``все простые числа больше чем x'' (задача 3.5). Формула вида F(t), где t – терм, обыкновенно выражает то же условие применённое к значению t. Например, F(a) есть " y (P(y) Й Q(a, y)), что значит ``все простые числа больше чем 10'', F(z₂) есть " y (P(y) Й Q(z₂, y)), что значит ``все простые числа больше чем z<sub>2</sub>''. Существует, однако, одно исключение. Формула F(y), то есть, " y (P(y) Й Q(y, y)), выражает (неправильное) утверждение ``каждое простое число меньше чем оно само''. Проблема с этой подстановкой в том, что, когда мы подставляем переменную y вместо x в F(x), y ``захватывается'' квантором. Чтобы выразить утверждение ``все простые числа больше чем y'' предикатной формулой, мы будем использовать связанную переменную отличную от y и писать, например,

" z(P (z) Й Q(y, z))

Чтобы различать ``плохие'' подстановки, как в последнем примере, от ``хороших'', мы определим, когда терм t является подстановочным для переменной v в формуле F.

• Если F – атомарная, тогда t является подстановочным для переменной v в F,

• t является подстановочным для переменной v в ¬F тогда и только тогда, когда t является подстановочным для v в F,

• t является подстановочным для v в (F Д G) тогда и только тогда, когда t является подстановочным для v и в F и в G,

• t является подстановочным для v в Kw F тогда и только тогда, когда

9. t не содержит w и является подстановочным для v в F, или

10. V не является свободной переменной формулы Kw f.

3.12 Терм, не содержащий ни одной связанной переменной формулы f, является подстановочным в f для любой переменной.

Определение 26 (Универсальное замыкание). Универсальное замыкание формулы F – это предложение

" v₁ ··· v_n F,

где v₁, ... , v_n – все свободные переменные F.

Выводы в логике предикатов

В логике предикатов вывод определяется так же, как и в исчислении высказываний и секвенции имеют тот же синтаксис. Аксиомы тоже определяются так же, как в логике высказываний. Все правила вывода логики высказываний – правила введения и удаления для пропозициональных связок, правила противоречия и сведения к противоречию – включены в множество правил вывода логики предикатов, с метапеременными для формул понимаемыми теперь как предикатные формулы. В дополнение, есть четыре новых правил вывода: правила введения и удаления для кванторов.

Правила для кванторов всеобщности

		G |– F(v)				G |– " v F(v)
	(В")				(У")
		G |– " v F(v)				G |– F (t)
где v не является свободной	где t является
		Переменной для любой формулы в G	подстановочным для v в F(v)

В каждой из следующих задач выведите данную формулу из пустого множества посылок.

3.19 (P(a) & " x (P(x) Й Q(x))) Й Q(a).

3.20 " xy P(x, y) Й " x P (x, x).

Правила для кванторов существования

		G |– F(t)				G |– $ v F(v) G И { F(v) }|– C
	(В$)				(У$)
		G |– $ v F(v)				G |– C
где t – подстановочный	где для C и любой формулы из G
		для v в F(v)	v не является свободной переменной

В каждой из следующих задач выведите данную формулу из пустого множества посылок.

3.21 (P(a) Ъ P(b)) Й $ x P(x).

3.22 ¬$ x P(x) є " x ¬P(x).

Корректность и полнота логики предикатов

Множество правил вывода для логики предикатов обладает свойством корректности и полноты подобно свойствам пропозициональных выводов.

Теорема корректности. Если существует вывод замкнутой формулы F из множества формул G, тогда G влечёт F.

Теорема полноты. Для любой замкнутой формулы F и любого множества предложений G, если G влечёт F, то существует вывод F из некоторого подмножества G.

Полнота логики предикатов для случая счётного G и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.

Функциональные символы и равенство: синтаксис

Логика предикатов, определённая выше немного более ограничена, чем что обыкновенно называется ``логикой первого порядка'', и наша следующая цель – удалить эти ограничения. Во-первых, мы обобщим понятие терма. В дополнение к объектным константам и объектным переменным, мы разрешим построение термов с использованием символов для функций, ``функциональных констант''. Во-вторых, мы добавим к языку знак равенства, и уравнения будут включены как новый тип атомарных формул.

Наше наиболее общее понятие сигнатуры определяется следующим образом.

Определение 28 (Сигнатура,константы). Сигнатура – это множество символов двух типов – функциональных констант и предикатных констант – с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа – это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.

Определение 29 (Терм). Возьмём сигнатуру s, не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если

• каждая объектная константа принадлежит X,

• каждая объектная переменная принадлежит X,

• для каждой функциональной константы h арности n (n > 0) и любой строки t₁, ... , t_n, если t₁, ... , t_n принадлежит X, тогда также принадлежит h(t₁, ... , t_n).

Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения