6 - Примеры формальных теорий. Теория групп. Формальная арифметика (Конспект лекций), страница 2

Подчеркнем, что под натуральным мы будем понимать целое неотрицательное число(т.е. включая нуль).Логико-математический язык должен быть односортным. Есть одна константа, которую мыобозначим через 0, две основные арифметические операции сложение и умножение реализуемдвумя бинарными функциональными символами, которые будем обозначать в инфиксной формезнаками + и · (этот знак по традиции опускается между двумя переменными). Описание двухопераций кольца недостаточно.

Характерным свойством натуральных чисел является переход кследующему натуральному числу, вытекающий из процесса пересчета предметов. Это отразимунарным функциональным символом, который будем обозначать в виде x+ . Наконец, нуженпредикатный символ, в качестве которого выбираем формальное равенство.В основе нашей формальной теории лежит аксиоматика натуральных чисел Пеано, включающая пять аксиом:ÃÒÓÌÃÒÓ6.2. Формальная арифметикаÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ64ÌÃÒÓΓ ` Ax0 ∧ ∀x(A → Axx+ )Γ ` ∀x(A → Axx+ )` Ax0 ∧ ∀x(A → Axx+ ) → A` ∀x(Ax0 ∧ ∀x(A → Axx+ ) → A)1. (X = Y ) → (X + Z = Y + Z).ÔÍ-12Отметим, что в этом правиле выбор переменной x не является существенным: последний шагможет идти с переименованием. На практике в качестве переменной x следует выбирать любую,не входящую свободно в формулы списка Γ.Правила C4–C6 отражают характерные черты формального равенства как предиката дляотношения эквивалентности, они полностью определяются аксиомами A4 и A6.

Вывод этихправил повторяет вывод соответствующих правил формальной теории групп.Многие ключевые факты арифметики (например, коммутативность сложения) вытекают изсформулированных аксиом. В их доказательстве особую роль играет схема аксиом, отражающая принцип математической индукции. Рассмотрим некоторые формулы.ÌÃÒÓΓ ` Ax0Γ ` Ax0 ∧ ∀x(A → Axx+ ) → AÔÍ-12Γ`AÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Γ ` Ax0 ; Γ ` ∀x(A → Axx+ );Γ`AΓ ` X+ = Y +C2.;Γ`X=YC3.

` ¬(X + = 0);C4. ` X = X;Γ`X=Y;C5.Γ`Y =XΓ`X =Y; Γ`Y =Z;C6.Γ`X=ZΓ`X=YC7.;Γ ` X+ = Y +C8. ` X + 0 = X;C9. ` X + Y + = (X + Y )+ ;C10. ` X · 0 = 0;C11. ` X · Y + = X · Y + X.Все эти правила устанавливаются так же как и в теории групп. Например правило C1:C1.ÌÃÒÓÌÃÒÓнеявно полагая, что формулы замкнуты кванторами всеобщности по всем свободным переменным). Исключение составляет аксиома индукции. Эта аксиома связана с произвольнымсвойством, которое характеризуется некоторым предикатом A, и задается некоторой схемой.В результате мы получаем одну схему аксиом и восемь аксиом:A1.

Ax0 ∧ ∀x(A → Axx+ ) → A.A2. (x+ = y + ) → (x = y).A3. ¬(x+ = 0).A4. (x = y) → ((x = z) → (y = z)).A5. (x = y) → (x+ = y + ).A6. x + 0 = x.A7. x + y + = (x + y)+ .A8. x · 0 = 0.A9. xy + = xy + x.Как и в случае теории G, эти аксиомы удобно преобразовать в правила вывода:ÌÃÒÓÔÍ-12ÌÃÒÓ65ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-126. Примеры формальныхтеорийÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.J На содержательном уровне рассуждение таково. При z = 0 равенство X + z = Y + z сводитсяк очевидному равенству X + 0 = Y + 0, вытекающему из цепочки X + 0 = X = Y = Y + 0. Есливерно равенство X + z = Y + z, то X + z + = (X + z)+ = (Y + z)+ = Y + z + .

На основании методаматематической индукции делаем вывод, что равенство X + z = Y + z верно для любого z.Формальный вывод рассматриваемой формулы строится на сведении к правилу C1 и можетвыглядеть так:ÔÍ-12ÔÍ-12ÌÃÒÓ66ÌÃÒÓÌÃÒÓ`X =Y →X +Z =Y +ZX =Y `X +Z =Y +ZX = Y ` ∀z(X + z = Y + z)X =Y `X +0=Y +0X = Y ` ∀z(X + z = Y + z → X + z + = Y + z + )1X = Y ` X + z = Y + z → X + z+ = Y + z+ÔÍ-12ÔÍ-12X =Y `X +z =Y +zX = Y, X + z = Y + z ` X + z + = Y + z +X + z = Y + z ` X + z+ = Y + z+Обе ветки заканчиваются секвенциями, которые можно обосновать цепочкой равенств.

Ветка 1 подробно раскрывается так:X =Y `X +0=Y +0`X +0=XX =Y `X =Y +0X=Y `X=YX =Y `Y =Y +0`Y =Y +0`Y +0=YВетка 2 ракрывается аналогично (список Γ содержит одну формулу X + z = Y + z):ÔÍ-12ÔÍ-12X =Y `X +0=XÌÃÒÓÌÃÒÓ2` X + z + = (X + z)+Γ ` (X + z)+ = Y + z +Γ ` (X + z)+ = (Y + z)+Γ ` (Y + z)+ = Y + z +Γ`X +z =Y +z` (Y + z)+ = Y + z +` Y + z + = (Y + z)+Как видим, формальный вывод заметно длиннее содержательного. I2.

0 + X = X.J Содержательное доказательство основано на замене Z переменной и применении индукциипо этой переменной. Имеем 0 + 0 = 0. Если 0 + x = x, то 0 + x+ = (0 + x)+ = x+ . Значит,ÔÍ-12ÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Γ ` X + z + = (X + z)+ÌÃÒÓÌÃÒÓΓ ` X + z+ = Y + z+ÌÃÒÓ0 + x = x. Формальное доказательство следующее:`0+X =X` ∀x(0 + x = x)`0+x=x` 0 + x = x → 0 + x+ = x+0 + x = x ` 0 + x+ = x+0 + x = x ` 0 + x+ = (0 + x)+` 0 + x+ = (0 + x)+0 + x = x ` (0 + x)+ = x+0+x=x`0+x=xОтметим переход от формулы X к переменной x, совершенный в начале вывода. Это стандартная подготовка к применению идукции, состоящая в замене одной из подформул переменной,которая становится переменной индукции. I3.

X + + Y = X + Y + .J Ограничимся содержательным рассуждением. Имеем x+ + 0 = x+ = (x + 0)+ = x + 0+ .Пусть x+ + y = x + y + . Тогда x+ + y + = (x+ + y)+ = (x + y + )+ = x + y ++ . Таким образом,x+ + y = x + y + . I4. X = Y → Z + X = Z + Y .J Содержательное рассуждение можно строить на переменной z, поставленной взамен формулы Z.

при z = 0 имеем 0 + X = X = Y = 0 + Y (использовано уже установленное свойство 2).Пусть доказано, что z + X = z + Y . Тогда, согласно свойству 3В соответствии с методом математической индукции, если X = Y , то z + X = z + Y . I5. (X + Y ) + Z = X + (Y + Z).(X + Y ) + z + = ((X + Y ) + z)+ = ((X + (Y + z))+ = X + (Y + z)+ = X + (Y + z + ).В соответствии с методом математической индукции заключаем, что (X +Y )+z = X +(Y +z). I6. X + Y = Y + X.7. X + Y = 0 → X = 0.J Заменяем формулу X индуктивной переменной x, При x = 0 имеем формулу 0+Y = 0→0 = 0,которая получается из истинной формулы 0 = 0 присоединением посылки.

Пусть формулаÔÍ-12J Заменяем формулу Y индутивной переменной y. При y = 0 имеем X + 0 = X = 0 + X. ЕслиX + y = y + X, то X + y + = (X + y)+ = (y + X)+ = y + X + = y + + X. Значит, X + y = y + Xдля любого значения переменной y. IÌÃÒÓJ Содержательное доказательство основано на методе математической индукции по переменной z, включенной в формулу взамен Z. Согласно свойству 4 имеем: (X + Y ) + 0 = X + Y == X + (Y + 0), поскольку Y = Y + 0. Предположим (X + Y ) + z = X + (Y + z).

ТогдаÔÍ-12z + + X = z + X + = (z + X)+ = (z + Y )+ = z + Y + = z + + Y.ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓ` ∀x(0 + x = x → 0 + x+ = x+ )ÌÃÒÓÔÍ-12ÌÃÒÓ`0+0=0ÌÃÒÓÔÍ-12ÌÃÒÓ67ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-126. Примеры формальныхтеорийÌÃÒÓx+ +Y =0`(x+Y )+ =x+ +Yx+ +Y =0`x+ +Y =0(x + Y )+ = 0 ` x+ = 0Γ`(x+Y )+ =0` (x + Y )+ = x+ + YΓ`¬((x+Y )+ =0)` ¬((x + Y )+ = 0)Следовательно, формула x + Y = 0 → x = 0 истинна при любом x. Отметим, что индуктивное предположение об истинности формулы x + Y = 0 → x = 0 фактически не нужно:общезначимость формулы (x+ + y = 0) → (x+ = 0) устанавливается без использования аксиомыиндукции.

I8. 0 · X = 0.J Заменяем формулу X индуктивной переменной x. При x = 0 равенство 0 · 0 = 0 вытекает изправила C10. Предположим 0 · x = 0. Тогда 0 · x+ = 0 · x + 0 = 0 + 0 = 0. Значит, формула0 · x = 0 истинна для любого значения переменной x. I9. Введем обозначение 1 = 0+ . Тогда X · 1 = X и 1 · X = X.J Для первого равенства имеем x · 1 = x · 0+ = x · 0 + x = 0 + x = x. Второе равенство 1 · x вернопри x = 0 (по аксиоме).

Пусть 1·x = x. Тогда 1·x+ = 1·x+1 = 1·x+0+ = x+0+ = (x+0)+ = x+ .Значит, 1 · x = 1. I10. X + · Y = X · Y + Y .J Содержательное доказательство проводится индукцией по переменной y, включенной в формулу взамен подформулы Y . При y = 0 имеем X + ·0 = 0 = 0+0 = X ·0+0.

Пусть X + ·y = X ·y+y.Тогда+ X · y + (y + + X) = X · y + (X + y + ) = (X · y + X) + y + = X · y + + y + .Поэтому формула X + · y = X · y + y верна при любом значении переменной y. I11. Умножение коммутативно: X · Y = Y · X.x+ · Y = x · Y + Y = Y · x + Y = Y · x+ .Следовательно, формула x · Y = Y · x верна при любом значении переменной x. I12. Умножение дистрибутивно относительно сложения: (X + Y ) · Z = X · Z + Y · Z.(X + Y ) · 0 = 0 = 0 + 0 = X · 0 + Y · 0.Пусть (X + Y ) · z = X · z + Y · z. Тогда(X +Y )·z + = (X +Y )·z+(X +Y ) = (X ·z+Y ·z)+(X +Y ) = (X ·z+X)+(Y ·z+Y ) = X ·z + +Y ·z + .ÔÍ-12J Доказательство также строится на принципе математической индукции по переменной z,включенной в формулу взамен подформулы Z. При z = 0 имеемÌÃÒÓJ Содержательное доказательство проводится индукцией по переменной x, включенной в формулу взамен X.

При x = 0 имеем x · Y = 0 · Y = 0 = Y · 0 = Y · x, т.е. при x = 0 формула верна.Пусть x · Y = Y · x. ТогдаÔÍ-12X + · y + = X + · y + X + = (X · y + y) + X + = X · y + (y + X + ) =ÌÃÒÓÔÍ-12ÌÃÒÓx+ + Y = 0 ` (x + Y )+ = 0ÔÍ-12ÔÍ-12x+ + Y = 0 ` x+ = 0ÃÒÓÌÃÒÓ` (x+ + Y = 0) → (x+ = 0)ÌÃÒÓÔÍ-12x + Y = 0 → x = 0 истинна. ТогдаÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ68ÌÃÒÓÔÍ-12ÌÃÒÓ69Следовательно, формула (X + Y ) · z = X · z + Y · z истинна при любом значении переменной z. I(x 6 x) ≡ ∃z(x + z = x) ⇐ x + 0 = x.На множестве натуральных чисел существует отношение порядка.

Можно рассмотреть формулу p(x, y) ≡ ∃z(x + z = y) и переобозначить ее как x 6 y. Двуместный предикатный символможно интерпретировать как бинарное отношение. Это отношение оказывается рефлексивным,транзитивным и антисимметричным, т.е. истинны формулы x 6 x, (x 6 y) ∧ (y 6 z) → (x 6 z)и (x 6 y) ∧ (y 6 x) → (x = y). Рефлексивность устанавливается просто:ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-126.