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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

Примеры формальныхтеорийÌÃÒÓУпражнение на транзитивность посложнее:` ∃u(x + u = y) ∧ ∃u(y + u = z) → ∃u(x + u = z)x + u1 = y, y + u2 = z ` ∃u(x + u = z)x + u1 = y, y + u2 = z ` x + (u1 + u2 ) = zx + u1 = y, y + u2 = z ` (x + u1 ) + u2 = zx + u1 = y, y + u2 = z ` (x + u1 ) + u2 = y + u2x + u1 = y, y + u2 = z ` y + u2 = zÔÍ-12ÔÍ-12∃u(x + u = y), ∃u(y + u = z) ` ∃u(x + u = z)мулой 7, которую легко превратить в правилаΓ`X +Y =0Γ`X +Y =0и.Γ`X=0Γ`Y =0∃u(X + u = Y ), ∃u(Y + u = X) ` X = YX + u1 = Y, Y + u2 = X ` X = YΓ ` Y + u2 = YΓ ` X = Y + u2Γ ` u2 = 0Γ ` Y + u2 = XΓ ` u 1 + u2 = 0Γ ` X + u1 + u2 = XΓ ` X + u 1 + u2 = Y + u2Γ ` Y + u2 = XÌÃÒÓÌÃÒÓТеперь выведем формулу (X 6 Y ) ∧ (Y 6 X) → (X = Y ). Эта задача сводится к доказательству выводимости ∃u(X + u = Y ), ∃u(Y + u = X) ` X = Y .

Вывод сводится к удалениюкванторов существования (список Γ содержит формулы X + u1 = Y , и Y + u2 = X):ÔÍ-12ÔÍ-12Но самое сложное — антисимметричность. В основе — утверждение, что если сумма двухчисел равна нулю, то каждое слагаемое равно нулю. Это утверждение устанавливается фор-ÌÃÒÓÌÃÒÓx + u1 = y, y + u2 = z ` x + u1 = yÔÍ-12ÔÍ-12Γ ` X + u1 = YÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ОГЛАВЛЕНИЕ151517223. Алгебра предикатов3.1. Предикаты и кванторы .

. . . . . . . . . .3.2. Логико-математические языки . . . . . . .3.3. Переименования и подстановки . . . . . .3.4. Семантика логико-математического языка3.5. Логические законы . . . . . . . . . . . . .3.6. Замены . . . . . . . . . . . . . . . . . . . .3.7. Упрощение формул . . . . . .

. . . . . . ........27272831343639414. Исчисление предикатов4.1. Построение теории P . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.3. Глобальные свойства теории P .

. . . . . . . . . . . . . . . . . . . . . . . . . . . .434344465. Генценовские формальные системы5.1. Исчисление GV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.2. Исчисление GP . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . .5454586. Примеры формальных теорий6.1. Теория групп . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2. Формальная арифметика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6161647. Метод резолюций7.1. Скулемовские функции . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . .7.2. Метод резолюций для исчисления высказываний . . . . . . . . . . . . . . . . . . .7.3. Метод резолюций для исчисления предикатов . . . . . . . . . . . . . . . . . . . . .70707275......................................................................................................................................................................................................................................................ÌÃÒÓ2. Исчисление высказываний2.1. Основные положения теории N .

. . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.3. Глобальные свойства теории N . . . . . . . . . . . . . . . . . . . . . . . . . . . . .....ÔÍ-12....224610ÔÍ-12ÔÍ-121. Алгебра высказываний1.1. Введение . . . . . . . . . . . . . . . . .1.2. Алгебра логики . . . . . . . . . . . . .1.3. Тавтологии и эквивалентность формул1.4. Функции алгебры логики . .

. . . . . .ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÃÒÓÔÍ-1270ÌÃÒÓÔÍ-12ÌÃÒÓ.

Характеристики

Список файлов лекций