В.А. Успенский - Курс лекций по математической логике, страница 3

. ..Пример 2.3. Формула ∃ x : ∀ y (x 4 y) существования минимального элемента отличает N и отрезок отмножеств Z, Q и R.Определение. Упорядоченное множество M, между любыми двумя различными элементами которого существует промежуточный элемент, т. е. ∀ x, y : x 6= y, ∃ z : x ≺ z ≺ y, называется плотным.Пример 2.4. R и Q являются плотными, а Z и N — нет.Определение. Если ξ и η — метапеременные (произвольные переменные языка), то выражения (ξ = η),(ξ 4 η) и (ξ ≺ η) называются атомными (атомарными) формулами.1 Обозначениевведено автором данного документа8При построении языка логики высказываний мы уже давали определение формулы.

Естественно, что в новомязыке формулы будут строиться по-другому.Определение.••••Всякая атомная формула есть формула.Если A — формула, то A — тоже формула.Если A и B — формулы, то (A ∨ B), (A&B), (A ⇒ B) — тоже формулы.Если A — формула, а ξ — метапеременная, то ( ∀ ξA) и ( ∃ ξA) — тоже формулы.1.2.3. Связанные и свободные вхождения переменныхРассмотрим понятия связанных и свободных вхождений переменных в формулы. В формулах ∃ xA и ∀ xAвыражения ∃ x и ∀ x называются кванторными приставками, а A — областью действия квантора. Послеквантора может стоять только переменная, но не имя.

Иначе говоря, бессмысленно подставлять вместо этойпеременной какое либо имя: ∃ 5A не определено.Определение. Вхождение переменной в область действия квантора или в кванторную приставку означает,что вхождение этой переменной связанное. Вхождения, не являющиеся связанными, называются свободными.Пример 2.5.

Рассмотрим формулу∀ x P f (x) & ∃ x(x = z) ⇒ ∃ xR(x, x) ∨ z = x.В этой формуле подчёркнуты все связанные вхождения переменной x, причём вхождения, связанные однойкванторной приставкой, подчёркнуты одинаковым числом чёрточек. Неподчёркнутые вхождения переменных —свободные.Определение. Подстановка переменной — замена всех свободных вхождений переменной.

Подстановкаобозначается символом [. . . / . . . ].Пример 2.6. Результатом (x = y)& ∃ x(x = z)[5/x] будет (5 = y)& ∃ x(x = z).Определение. Графическое равенство — совпадение слов. Обозначается знаком ≖.Пример 2.7. ∃ x ∀ x(x = x)[5/x] ≖ ∃ x ∀ x(x = x), поскольку переменная x везде связана.Символом K мы будем обозначать квантор ∀ или ∃. Символом ∇ мы будем обозначать логические связки∨ и &.

Если эти символы встречаются в формуле, то всякий раз они заменяют один и тот же квантор илисвязку. Иначе говоря, если написана формула типа KξA(ξ) ≡ KηA(η), то это значит, что имеют место формулы∃ ξA(ξ) ≡ ∃ ηA(η) и ∀ ξA(ξ) ≡ ∀ ηA(η).В общем случае можнорассматривать разные связывающие операторы. Примерами таких связывающихRоператоров являются . . . dξ и ξ | . . . . Так, все вхождения ξ под знаком интеграла и слева от вертикальнойчерты в имени множества будут связанными.

Здесь ξ — метапеременная.Определение. Именная форма — форма, при подстановке вместо переменных конкретных значений в которую получается имя.Пример 2.8. Формаex −1xявляется именной формой.ex −1x→x0 xЗамечание. Связанные переменные можно разумно переименовывать. Например, limПеременная x0 в данном выражении свободна, поэтому её переименовывать нельзя.Утверждение 1.6.

Справедливы следующие законы:••••∀ ξA ≡ ∃ ξA.∃ ξA ≡ ∀ ξA.∃ ξ(A ∨ B) ≡ ∃ ξA ∨ ∃ ξB .∀ ξ(A&B) ≡ ∀ ξA & ∀ ξB .Кроме того, если ξ не входит свободно в A, то• (A∇B)[e/ξ] ≖ A∇B[e/ξ].• Kξ(A&B) ≡ A& KξB.• Kξ(A ∨ B) ≡ A ∨ KξB.Задача 1.11. Пусть a — имя. Тогда ∃ x (x = a)&A ≡ A[a/x].9ey −1.y→x0 y= lim1.2.4. Приведение формулы к предварённой формеОпределение.

Формула в предварённой форме — формула, в которой все кванторы вынесены в начало. Онаимеет вид K 1 ξ1 . . . K n ξn A, где A — бескванторная формула.Определение. Переменная ξ называется свежей по отношению к формуле A, если ξ не встречается в A.Существует алгоритм приведения формулы к предварённой форме. Вместо того, чтобы формально его описывать, рассмотрим пример, на котором всё станет ясно. Для начала избавимся от импликаций. Пусть теперьA — безымпликативная формула, например, такая: A = ∃ xA ∨ ∀yB. Пусть w — свежая переменная по отношению к A и B. Тогда A ≡ ∃ wA[w/x] ∨ ∀ yB ≡ ∃ w A[w/x] ∨ ∀ yB .

Пусть t — свежая переменная по отношениюк A и B. Тогда A ≡ ∃ w A[w/x] ∨ ∀ tB[t/y] ≡ ∃ w ∀ t A[w/x] ∨ B[y/t] , и формула приведена к предварённойформе.1.2.5. Теорема о свободной подстановкеПокажем, что не всякие подстановки бывают правильными. Пусть a — имя, а x и y — переменные. Зададимся вопросом, всегда ли верно ли утверждение A[a/x][a/y] ≖ A[y/x][a/y]? Приведём пример, когда это неверно,R1R1например, рассмотрим A = x dy и a = 5. Результатом первой подстановки, как легко видеть, будет 5 dy,00а результатом второй —R1y dy. В этом примере при подстановке [y/x] переменная x, бывшая свободной, поRпала в область действия связывающего оператора .

. . dy. Чтобы исключить такие оказии, определим класс«правильных» подстановок.Определение. Свободной (разрешённой, допустимой) подстановкой переменной называется такая подстановка [y/x], при которой каждое свободное вхождение переменной x превращается в свободное вхождение переменной y.Очевидно, что если y — свежая переменная для A, то подстановка A[y/x] будет свободной.

В дальнейшеммы будем рассматривать только свободные подстановки, а если A[y/x] — несвободная подстановка, то такуюзапись будем считать бессмысленной.Теорема 1.7 (О свободной подстановке). Для свободных подстановок имеем A[a/x][a/y] ≖ A[y/x][a/y]. Пусть, например, A = . . . x . . . y . . . .

Тогда при подстановке слева получаем A[a/x] = . . . a . . . y . . ., а затемA[a/x][a/y] = . . . a . . . a . . .. Справа будет так: A[y/x] = . . . a . . . y . . ., а затем A[y/x][a/y] = . . . a . . . a . . .. Разницыникакой, потому что никакое свободное вхождение при промежуточных подстановках не стало связанным. Таким образом, графически результат левой и правой подстановки одинаков. Общий случай ничем не отличаетсяот частного. Следствие 1.4. Пусть y — переменная. Если A[y/x] определено, то ∃ x (x = y)&A ≡ A[y/x].

Слева и справа стоят высказывательные формы, зависящие как минимум от y, но не от x. Подставимвместо всех свободных переменныхпроизвольные константы, причём вместо y подставим имя a. Надо доказать,что ∃ x (x = a)&A[a/y] ≡ A[y/x][a/y]. Но, как мы знаем, левая часть эквивалентна формуле A[a/y][a/x].Осталось применить теорему о свободной подстановке и заметить, что доказанное утверждение не зависит от a,а потому оно верно для всех a. 01.2.6. Теорема об элиминации кванторовЯзык упорядоченных множеств называется элементарным, поскольку в нём все переменные имеют один итот же сорт (т. е.

одну и ту же область значений, называемую носителем).Определение. Формула называется замкнутой, если в ней нет свободных переменных. Ясно, что такаяформула может быть либо истинной, либо ложной.Определение. Назовём хорошим плотное линейно упорядоченное множество без наименьшего и наибольшего элемента.Определение. Пусть на множестве M введены отношения порядка ≺ и ≻, тогда интервалом (a, b) называется множество {x ∈ M : a ≺ x ≺ b}.Добавим в наш язык символы ⊤ и ⊥, чтобы можно было построить замкнутую формулу без переменных.Теорема 1.8 (Об элиминации кванторов).

Пусть M — хорошее множество. Для всякой формулы Aможно эффективно построить такую бескванторную формулу B, что всякая переменная, свободно входящаяв B, свободно входит в A, и при этом A ≡ B. Доказательство разобьём на несколько этапов.0◦ Если A — бескванторная, то доказывать нечего.101◦ Пусть A имеет вид ∃ z (A1 & . . .

&As ), причём Ai — атомные формулы. Следовательно, Ai имеют вид ⊤,⊥, (ξ = ξ), (ξ ≺ ξ), (ξ ≺ η), (ξ = η) или (ξ ≻ η). Очевидно, что (ξ = ξ) — это ⊤, а (ξ ≺ ξ) и (ξ ≻ ξ) — это ⊥.Ясно, что ⊤ можно зачеркнуть, а если есть хоть одна ⊥, то и вся конъюнкция ложна. Все Ai , не содержащие z,можно вынести за знак квантора.Осталось три возможности: (ξ = z), (ξ ≺ z) и (ξ ≻ z). Если есть хоть одно равенство, то от формулыQ& ∃ z (z = ξ)&B можно перейти к равносильной формуле Q&B[ξ/z]. В этом случае последняя формула будетискомой формулой B.В случае, когда ни одного равенства нет, возможны три случая:z Все формулы имеют вид (ξ ≺ z). Поскольку в хороших множествах нет наименьшего элемента, формула∃ z (ξ ≺ z)& . . . &(ξn ≺ z) тождественно истинна.z Все формулы имеют вид(ξ ≻ z).