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

ÔÍ-12ÔÍ-12ÌÃÒÓМосковский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»ÌÃÒÓÀ.Í. ÊàíàòíèêîâÈ ÒÅÎÐÈß ÀËÃÎÐÈÒÌÎÂÊîíñïåêò ëåêöèéÔÍ-12Москва2009ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Äëÿ ñòóäåíòîâ êàôåäðû ÈÓ9ÌÃÒÓÌÃÒÓÌÀÒÅÌÀÒÈ×ÅÑÊÀß ËÎÃÈÊÀÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓ6. ПРИМЕРЫ ФОРМАЛЬНЫХ ТЕОРИЙÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-1261ÌÃÒÓПодбор составляющих любой формальной теории — творческий процесс, не дающий однозначного результата. В основе, конечно, лежат содержательные аксиомы соответствующейдисциплины.

В теории групп встречаются объекты одного типа. Значит, можно использоватьодин сорт переменных. Для обозначения операции группы нужен один функциональный символарности 2. Но есть еще две вторичные операции, точнее очевидная константа и унарная операция вычисления обратного элемента. Для записей условий нужен хотя бы один предикатныйсимвол и наиболее уместным является символ равенства. Это бинарный символ, но чтобы бинарный предикатный символ мог расцениваться именно как знак равенства, нужны некоторыетребования (аксиомы).Учитывая вышесказанное опишем формальную теорию групп G.

Рассмотрим односортный логико-математический язык с одной константой, которую мы обозначим через e, двумяфункциональными символами m(x, y) и i(x) и одним бинарным предикатным символом p(x, y).Правила вывода — стандартные для исчисления предикатов. Запишем нелогические аксиомы:1) p(x, y) → (p(x, z) → p(y, z));2) p(x, y) → p(m(x, z), m(y, z));3) p(x, y) → p(m(z, x), m(z, y));4) p(m(m(x, y), z), m(x, m(y, z)));5) p(m(x, e), x);6) p(m(x, i(x)), e).Напомним, что нелогические аксиомы любой формальной теории должны быть замкнутыми формулами. Поэтому здесь неявно предполагается, что аксиомы теории групп замкнутыкванторами весобщности по всем свободным переменным.Запись нелогических аксиом прямо следует описанию логико-математического языка, но неудобна для восприятия человеком.

Введем альтернативные обозначенияЖ x ∗ y вместо m(x, y),x−1 вместо i(x), 1 вместо e и x = y вместо p(x, y). Тогда перечисленные аксиомы будут выглядеть следующим образом:1◦ (x = y) → ((x = z) → (y = z));2◦ (x = y) → (x ∗ z = y ∗ z);3◦ (x = y) → (z ∗ x = z ∗ y);4◦ (x ∗ y) ∗ z = x ∗ (y ∗ z);5◦ x ∗ 1 = x;6◦ x ∗ x−1 = 1.Из рассмотренных аксиом (в любой записи) первая характеризует предикат, вторая и третья связывают предикат с основной операцией, а последние три фиксируют свойства операцийгруппы. Вообще говоря, бинарный предикат определяет на носителе интерпретации отношение, и если мы хотим рассматривать предикат как равенство, указанное отношение должнобыть отношением эквивалентности, т.е.

должны быть истинными утверждения о рефлексивности, симметричности и транзитивности. В аксиоме 1 можно усмотреть рефлексивность, но нехватает двух других свойств.ÔÍ-12ÔÍ-126.1. Теория группÌÃÒÓÌÃÒÓРассмотрим построение формальных теорий, описывающих некоторые конкретные математические дисциплины.ÌÃÒÓÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.Не следует ожидать, что выбором некоторых формул в качестве аксиом можно гарантировать, что рассматриваемый предикат будет именно равенством, т.е. истинным при совпаденииобъектов, обозначаемых двумя термами. Для теории групп такие попытки даже вредны. Делов том, что термин равны“ следует понимать как неразличимы“, т.е.

это могут быть разные,””вообще говоря, объекты, но подпадающие под одно понятие. В математике формирование понятий связано с отношением эквивалентности. Так и здесь: отношение x = y на самом деле —это отношение эквивалентности.Отметим, что в G сохраняются все правила естественного вывода, а доказательство теоремпредставляет собой частный вывод, в котором роль гипотез играют нелогические аксиомы.Для сокращения вывода сами нелогические аксиомы удобно заменить некоторыми правиламивывода, налогичными правилам естественного вывода.

Так, аксиомам 2 и 3 соответствуютправилаΓ`X=YΓ`X=Y,,(6.1)Γ`X ∗Z =Y ∗ZΓ`Z ∗X =Z ∗Yа аксиомы 4–6 трансформируются в схемы выводимых формул:` X ∗ 1 = X,` X ∗ X −1 = 1.(6.2)Например, первое из правил (6.1) устанавливается следующим образом:Γ`X ∗Z =Y ∗ZΓ`X=YΓ`X =Y →X ∗Z =Y ∗ZÔÍ-12` (X ∗ Y ) ∗ Z = X ∗ (Y ∗ Z),ÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ62` ∀y∀z(X = y → X ∗ z = y ∗ z)` ∀x∀y∀z(x = y → x ∗ z = y ∗ z)Обращаем внимание на переход от переменной (например x) к произвольной формуле (в данномслучае X) через снятие квантора с подстановкой. Аналогично устанавливаются секвенции (6.2).приведем вывод второй из них:` X ∗ 1 = X ⇐ ∀x(x ∗ 1 = x).Аксиома 1 позволяет установить правила` X = X,Γ`X=Y,Γ`Y =XΓ ` X = Y ;Γ ` Y = Z,Γ`X=Z`X=X` X ∗ 1 = X → (X ∗ 1 = X → X = X)`X ∗1=XÔÍ-12`X ∗1=X` ∀z(X ∗ 1 = X → (X ∗ 1 = z → X = z))` ∀y∀z(X ∗ 1 = y → (X ∗ 1 = z → y = z))` ∀x∀y∀z(x = y → (x = z → y = z))ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12`X ∗1=X →X =XÌÃÒÓвыражающие свойства, характеризующие отношение эквивалентности (рефлексивность, симметричность, транзитивность).В принципе формулу X = X (точнее ∀x(x = x)) следовало бы ввести как аксиому поддержкиформального равенства.

Однако в данном случае эта формула оказывается выводимой в теорииG. Действительно,ÃÒÓÔÍ-12` ∀z(X = Y → X ∗ z = Y ∗ z)ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓ`X =Y →X ∗Z =Y ∗ZÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ63Используя доказанную рефлексивность, можно доказать и симметричность:ÔÍ-12ÌÃÒÓÔÍ-126. Примеры формальныхтеорийÌÃÒÓΓ`Y =XΓ`X=YX=Y `Y =XX = Y, X = X ` Y = X`X=X` X = Y → (X = X → Y = X)` ∀x∀y∀z(x = y → (x = z → y = z)Транзитивность можно получить из аксиомы 1 с доказанным свойством симметричности:Γ`X=ZΓ`X=YX =Y ∧Y =Z `X =ZΓ`Y =ZÔÍ-12ÔÍ-12Γ`X =Y ∧Y =ZÌÃÒÓÌÃÒÓX =Y `X =X →Y =XX = Y, Y = Z ` X = ZY = X, Y = Z ` X = ZY =X `Y =Z →X =ZX=Y `Y =XX=Y `X=Y` Y = X → (Y = Z → X = Z)Остальные свойства могут быть получены использованием цепи равенств. Докажем формулу (A ∗ X = A) → (X = 1), означающую, что правая единица единственная.

Содержательноерассуждение таково. Если A ∗ X = A, то A−1 ∗ (A ∗ X) = A−1 ∗ A = 1. Но A−1 ∗ (A ∗ X) =(A−1 ∗ A) ∗ X = 1 ∗ X = X. Поэтому X = 1.Соответствующий вывод формулы (A∗X = A)→(X = 1) может быть таким (для сокращениязнак умножения опущен):` AX = A → X = 1AX = A ` X = 1AX = A ` A−1 A = 1AX = A ` X = A−1 AXAX = A ` A−1 AX = A−1 AAX = A ` A−1 AX = XAX = A ` AX = A` A−1 AX = 1 ∗ X` A−1 A = 1`1∗X =X` A−1 A = 1ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12AX = A ` X = A−1 AÌÃÒÓÔÍ-121 ∗ x = (x ∗ x−1 ) ∗ x = x ∗ (x−1 ∗ x) = x ∗ 1 = x.ÌÃÒÓÌÃÒÓТеперь докажем, что правая единица является левой:ÔÍ-12Действие симметричности, рефлексивности и транзитивности можно записывать как цепочку равенств: X = Y = Z = . .

.Отметим, что существование левой единицы и левого обратного в аксиомах не оговорено.Однако это можно получить из существования правой единицы и правого обратного для каждого элемента. Действительно, докажем, что правый обратный является левым:x−1 ∗ x = (x−1 ∗ x) ∗ 1 = (x−1 ∗ x) ∗ (x−1 ∗ (x−1 )−1 ) = x−1 ∗ x ∗ (x−1 ∗ (x−1 )−1 ) == x−1 ∗ (x ∗ x−1 ) ∗ (x−1 )−1 = x−1 ∗ 1 ∗ (x−1 )−1 = (x−1 ∗ 1) ∗ (x−1 )−1 = x−1 ∗ (x−1 )−1 = 1.ÌÃÒÓÌÃÒÓ` ∀x∀y∀z(x = y → (x = z → y = z)ÌÃÒÓP6.P7.P8.P9.m + 0 = m;m + n+ = (m + n)+ ;m · 0 = 0;m · n+ = m · n + m.ÔÍ-12При построении формальной теории первые две аксиомы Пеано не нужны, поскольку реализуются на уровне логико-математического языка. Например, первая аксиома фактическиутверждает, что в языке арифметики есть константа.

В то же время в состав аксиом необходимо включить аксиомы поддержки формального равенства. Кроме того, в состав аксиоммы включаем формулы определения арифметических операций. Все аксиомы, кроме аксиомыиндукции, должны быть замкнутыми формулами (хотя для краткости мы кванторы опустим,ÌÃÒÓНетрудно убедиться в том, что все эти аксиомы необходимы.

Первые две дают, по существу, индуктивное определение натуральных чисел. Отсутствие аксиомы P3 приводит ксуществованию древовидной модели, в которой некоторые ветви начинаются не с нуля. Аксиома P4 препятствует появлению циклической модели (например, комплексных корней n-йстепени из 1).

Наконец, аксиома P5 обеспечивает связность натурального ряда, т.е. свойство,что любое натуральное число получается с помощью аксиом P1 и P2. Она же лежит в основепринципа математической индукции. С помощью этой аксиомы вводятся основные арифметические операции — сложение и умножение:ÔÍ-12P1. 0 — натуральное число.P2.

Если n — натуральное число, то n+ — натуральное число.P3. Если m, n — натуральные числа и m+ = n+ , то m = n.P4. Если n — натуральное число, то n+ 6= 0.P5. Пусть A — некоторое свойство, которым могут обладать натуральные числа. Предположим, что: а) 0 обладает свойством A; б) из того, что n обладает свойством A, вытекает, чтои n+ обладает свойством A. Тогда любое натуральное число обладает свойством A.ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Рассмотрим формальную теорию AP , описывающую элементарную теорию чисел (арифметику), т.е. теорию натуральных чисел с арифметическими операциями.

Отметим, что припостроении формальных систем всегда руководствуются некоторой реальной математическойдисциплиной, которая в таком случае обеспечивает естественную интерпретацию строящейся теории. Построенная теория может иметь множество интерпретаций (как теория G).Но может быть (а в некоторых случаях должно быть) так, что все интерпретации являются изоморфными, т.е. между этими интерпретациями есть взаимно однозначное соответствие,сохраняющее все свойства этих интерпретаций.Так должно быть в случае формальной арифметики, поскольку наличие нескольких моделейнатуральных чисел, ясно различающихся по своим свойствам, вряд ли можно считать приемлемым.