Эквивалентность двух определений элементарной формальной системы



Скачать 110.5 Kb.
Дата18.01.2013
Размер110.5 Kb.
ТипДокументы

Эквивалентность двух определений элементарной формальной системы

Посвящается А. Гейтингу по случаю его 70-летия

Хаскелл Б. Карри



Руководитель семинаров по философии: доц. С.Л. Катречко

Перевел: асп. каф Высшей Алгебры Е. Епифанов

Научный руководитель: д.ф.-м. наук, проф. Г.Б.Шабат

1. Введение


В своей книге «Теория формальных систем» Смульян вводит понятие элементарной формальной системы. Это определение, очевидно, близко связано с понятием, которое я называл таким же именем в книгах «Исчисления и формальные системы» (стр. 267) и «Основания математической логики» (стр. 68). Ясно, что эти два определения в некотором смысле эквивалентны, и мне показалось интересным исследовать точную связь между ними. В этой заметке представлен результат исследования.

Чтобы не возникала путаница, будем использовать термин элементарная формальная система (efs) именно в смысле, в котором он используется в книге «Исчисления и формальные системы», в то время как понятие, введенное Смульяном, будем называть smef. Так же, хотя я буду полностью следовать терминологии источников, будут использоваться эти модификации, чтобы избегать путаницы между одинаковыми терминами, обозначающими разные виды систем.

Здесь приводится достаточно полное объяснение, чтобы читатель мог разобраться в сути, не обращаясь к первоисточникам; однако, может быть полезным обратиться к ним за дополнительными деталями, наглядными примерами, обсуждением терминов, которые мы здесь считаем понятными, и т.д.

Некоторые изменения , соответствующие «Основаниям математической логики», рассматриваются, в основном, в сносках.

2. Элементарные формальные системы


Начнем с перечисления основных свойств понятия efs.

Формальная теория – это класс Т элементарных теорем, который является подклассом класса S элементарных высказываний. Класс Т строится из подкласса U по правилам R. Классы S, U и R – определенные классы в смысле §2А5 книги «Основания математической логики»1; также должен быть эффективный метод проверки доказательства элементарной теоремы, т.е. проверки правильности применения правил; но в общем случае класс Т лишь полуопределен.

Формальная система – это формальная теория, в которой мы выделяем класс формальных объектов D и класс J элементарных предикатов различных степеней (степень предиката – это количество его аргументов), таких что любое элементарное высказывание заключается в том, что предикат Р степени n истинен для упорядоченного набора из n объектов ; это высказывание можно записать так:



Что касается формальных объектов, то в «Основаниях математической логики» описаны две возможности.
В первой, которая называется синтаксической системой, формальные объекты являются словами (т.е. конечными строками), образованными из букв некоторого алфавита В. Во втором случае, который называется ob-системой, формальные объекты порождаются из определенных атомов при помощи определенных операций2. Различия между этими двумя случаями вряд ли существенны для наших нужд. Если мы присвоим атомам буквы из алфавита , операциям степени (т.е. с k аргументами) – буквы из алфавита и если мы присвоим ob’ам слова, образованные из всех этих букв некоторой стандартной записью, как, например, бесскобочная запись Лукашевича, тогда ob’ы в самом деле окажутся словами в алфавите В, который является объединением всех алфавитов . Однако, они не образуют всех слов этого алфавита, а лишь некоторое определенное подмножество3. Таким образом, если мы допускаем возможность того, что не все слова в В допустимы как формальные объекты, а только лишь «правильно образованные» из них, то мы получим и синтаксическую систему, и ob-систему4. Будем использовать термин ob для формального объекта в системе любого из этих типов; термин wef, который я иногда предлагал для употребления, оставим до случая связанного с smef.

Элементарная формальная система (efs) – это та, в которой правила имеют определенную форму. Элементарного правило – это утверждение вида

(1)

где - это элементарные утверждения; (1) означает, что если лежат в Т, то и лежит в этом классе. Схема элементарных правил – это утверждение вида (1), содержащее определенные интуитивные (или U-) переменные, такие что когда мы подставляем произвольные формальные объекты вместо них, то в результате получается пример элементарного правила. Элементарной формальной системой в таком случае будет та, в которой аксиомы заданы конечным числом схем, а правила заданы конечным числом5 элементарных схем правил.

Мы можем сформулировать это определение иначе, вводя понятие ob-расширения. Пусть - это все переменные, встречающиеся в схемах правил системы G. Пусть G* - это формальная система, полученная из G присоединением к формальным объектам в качестве букв, которые мы добавим к B (или ), оставив все остальное без изменения. Теперь, если мы определим схему элементарных правил G как элементарное правило из G*, то понятно, что подстановка элементарных объектов G вместо в схеме правил G, даст нам правило в G.

В efs элементарное утверждение B принадлежит Т тогда, когда есть последовательность , такая что - это B, и каждое лежит либо в U, либо является следствием какого-то из своих предшественников при помощи правила R; последнее означает, что есть правило вида (1) такое, что - , и каждое при - это какое-то из при . Далее, утверждение (1) – это выведенное правило тогда, когда существует последовательность такая, что - это , а каждое либо 1) лежит в U, либо 2) является одним из при , либо 3) является выводом из правила вида (1) (конечно, не с теми же ), чьи предпосылки являются при .

Возможно, стоит заметить, что выше мы считали, что алфавит состоит лишь из конечного количества объектов, которые называются буквами. В общем случае, эти буквы упорядочены. Этот порядок называется алфавитным порядком, но здесь это не играет роли. Какие из объектов являются буквами (или атомами) – абсолютно не важно.

3. Понятие smef


Теперь рассмотрим определение Смульяна. Как уже говорилось в §1, терминология будет немного изменена, когда есть конфликт с обозначениями, введенными в §2. Имея ввиду §2, дальнейшее повествование будет чуть более сжатым.

Smef – это набор G’, состоящий из следующих элементов:

  1. Алфавита A.

  2. Алфавита переменных В, отличного от А.

  3. Алфавита «предикатов» D, каждый из которых имеет определенную фиксированную степень. Чтобы избежать путаницы с понятием предиката, введенным в §2, буду называть эти предикаты атрибутами.

  4. Знак импликации «→»6 средства для обозначения того, что атрибут применяется к своим аргументам (Смульян для этого использовал запятую, я же буду использовать обычную математическую запись).

  5. Конечное множество7 аксиом, каждая из которых – это wef в смысле, указанном ниже.

В терминах этих понятий Смульян определяет категории таким образом:

Выражения. Это – определенные слова из букв алфавитов А и В. Смульян допускает любые слова, но он мог с тем же успехом допускать лишь определенное подмножество множества всех слов, так что они были бы ob’ами в ob-системе или её языковом расширении. Выражения без переменных будем называть постоянными.

Элементарные wef’ы. Имеют вид , где - выражения, а Ф – атрибут степени n.

Wef’ы (правильно образованные формулы). Они составляют класс, индуктивно определенный так: (f1) любая элементарная wef является wef, (f2) если - это wef, а это элементарная wef, то - это wef. Таким образом, wef’ы имеют вид

(2)

где все - элементарные wef8.

Теоремы в G’ образуют класс, который порожден аксиомами при помощи двух правил, подстановки и modus ponens. Элементарные теоремы – это те, которые также являются и элементарными wef. При помощи обычного процесса «Ruckverlegung der Einsetzungen» («Основания математической логики», §3D3, стр. 115)9 мы можем полагать, что в аксиомах делаются подстановки, так что аксиомы заданы схемами аксиом; тогда остается единственное правило modus ponens.

4. Теорема о эквивалентности


Основной результат этой заметки такой:

Теорема 1. Пусть G – это efs, а G’ – это smef, такие, что выполнены следующие условия:

  1. Формальные объекты G в точности являются постоянными выражениями G’.

  2. Существует взаимно однозначное соответствие, сохраняющее степень, между элементарными предикатами G и атрибутами G’. Это задает соответствие, которое присваивает каждому элементарному утверждению X из G (или некоторого его языкового расширения) единственное элементарное wef X’ из G’ и наоборот.

  3. Правила и (для n=0) аксиомы из G являются схемами вида

(3)

где - это ob’ы в языковом расширении G, неизвестные работают как U-переменные для формальных объектов; аксиомы G’ в точности являются соответствующими схемами

(4)

Далее, пусть - элементарные высказывания G, а - соответствующие элементарные wef G’.

Тогда необходимое и достаточное условие того, что (1) является выведенным правилом G, состоит в том, что должно быть элементарной теоремой в той smef G’, которая получается присоединением к аксиомам G’.
Доказательство необходимости.

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



где предшествуют в Δ. Тогда



будет аксиомой G’, и, следовательно, теоремой G’’. По предположению индукции каждое из будет теоремой G’’. Поэтому, применяя несколько раз modus ponens, получим, что также явзяется теоремой G’’.

Доказательство достаточности10.

Пусть - вывод Δ’ утверждения в G’’. Тогда каждое из имеет вид



где - элементарные. Теперь покажем по индукции по k, что

(5)

это – выведенное правило в G. Если - это , то r=0 и , и (5) очевидно. Если - это аксиома в G’, то (5) верно без , а, следовательно, с ними и подавно. Если получено при помощи вывода, то существует элементарное wef D’ такое, что D’ и обе являются теоремами G’’. По предположению индукции имеем





Пусть второй вывод представлен в виде дерева; вместо каждого вхождения D подставим его вывод, тогда в результате получится вывод (5).

Для k=p имеем r=0 и . Тогда (5) дает (1). Ч.т.д. Это завершает доказательство теоремы.

Замечание 1. Ограничение на то, что должны быть константами можно налагать отдельно, присоединяя все переменные, которые они содержат к G, т.е. используя подходящее языковое расширение G. Подстановки не должны вызывать трудностей, т.к. мы исключили правило подстановок.

Следствие 1.1. Элементарные теоремы G соответствуют элементарным теоремам G’ и наоборот.

Доказательство. Это частный случай с n=0.
Следствие 1.2. Любая теорема G’ соответствует выведенному правилу G.

Доказательство. Если



- теорема в G’, то - теорема G’’.

Замечание 2. Утверждение, обратное к следствию 1.2 не верно, т.к. в G’ нет теоремы дедукции. Контрпримером является случай, когда n=0 во всех аксиомах (4); тогда нельзя получить . Более того, не каждое выведенное правило G будет теоремой в G’. Фактически, каждая теорема G’ является концевым куском аксиомы, т.е. получается из аксиомы вида (4) отбрасыванием каких-то из начальных . Хотя, если аксиомы и (примитивные) правила G – это

, ,

то



- выведенное правило, но



не является теоремой G’.

Замечание 3. Если элементарные wef’ы являются высказываниями, то → является связкой, и smef не является efs. Это можно обойти, рассматривая и → как операторы, также как при редукции формальной системы к утвердительной форме («Основания математической логики», §2D1). Ограничения в modus ponens на то, что предшественник импликации должен быть элементарным, также можно избежать, благодаря тому, что аксиомы имеют такой характер11. Таким образом, smef превращается в efs особого вида.

5. Вывод из замечаний


Теорема 1 утверждает, что понятия smef и efs являются эквивалентными. Заметим, что и G, и G’ можно определить сначала, а затем вывести второе из него. Поэтому, каждая efs может быть представлена как smef и наоборот; и если кто-либо отождествит атрибуты G’ и элементарные предикаты G, то обе системы будут иметь одинаковые элементарные теоремы (следствие 1.1), и одинаковые выведенные элементарные правила12. У smef есть преимущество в том, что все smef имеют одинаковые правила; вместе с тем, у нее есть и недостатки, когда дело доходит до применения техник формального выводимости13.

1 Один из моих студентов, Л. Флейшхакер, предложил следующий комментарий по поводу замечаний, сделанных там. Понятие определенности имеет смысл, применительно к бесконечному классу, лишь в связи с более широким классом, который можно называть фундаментальным классом или абсолютом. Рассмотрим класс W конечных слов в конечном алфавите B; он приводился в «Основаниях математической логики» как первый пример определенного класса. Но если бы существовали слова бесконечной длины, то было бы невозможно определить в конечных терминах, имеет ли этот феномен место, или нет. Так что, когда мы говорим, что F – определенный класс, то мы неявно вводим некоторый абсолют с узнаваемой конечной структурой. В «Основаниях математической логики» F взят как определенный по отношению к классу U-выражений а в других местах, когда ситуация не требует такой строгости, просто говорится, что ответ на вопрос «принадлежит ли данное выражение к F?» известен. Подобное замечание применимо и к D, и к другим классам, который мы введем ниже. Но U и T рассматриваются со ссылкой на F как абсолют.

2 Это следует понимать в том смысле, что каждому ob’у соответствует единственная конструкция, которую можно представить в виде размеченного дерева. Так что ob’ы можно представлять как символьные конструкции, имеющие древоподобную структуру, вместо строк.

3 Обратное преобразование, от синтаксической к ob-системе, также возможно, но требует более сложных идей. Если операция – это конкатенация, а буквы – это атомы, то одно слово можно получить разными способами. Таким образом, синтаксическая система – это фактор-структура ob-системы по отношению равенства, которое задано законом ассоциативности.

4 Конечно, возможны и другие типы систем.

5 Возможно, это можно обобщить, разрешая, к примеру, рекурсивное множество аксиом и схем правил. В этом случае следует сделать соответствующие поправки в определении smef (см. §3).

6 Использование знака «→» здесь не надо путать с его использованием в «Основаниях математической логики»; также его не нужно путать со знаком «»

7 По поводу этого ограничения см. сноску 5.

8 Заметим, что если «→» рассматривается как знак операции, то он присваивает направо; т.е. (2) получено из и , а не, к примеру, из и

9 Это часто приписывают фон Нойманну; но в принципе, это же есть и у Поста («Введение в общую теорию элементарных утверждений», лемма 2, стр. 178)

10 Отметим, что в этом доказательстве - не обязательно элементарные wef.

11Это, конечно, зависит от отсутствия ассоциативности, указанного в сноске 8. Вывод получается по индукции на количество шагов в доказательстве.

12 Заметим, что в примере в конце замечания 2, в самом деле будет элементарным выведенным правилом (смысл понятен из формулировки) в G’, несмотря на то, что её аналог не будет теоремой в G’.

13 Такие, как рассмотренные во второй части «Оснований математической логики». Ситуация, упомянутая в замечании 2, является недостатком.

Похожие:

Эквивалентность двух определений элементарной формальной системы iconЭквивалентность за- и расшифрования
Теперь докажем алгоритмическую эквивалентность процедур за- и расшифрования. Для этого в приведенной ниже таблице сравним последовательность...
Эквивалентность двух определений элементарной формальной системы iconСоставляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы
Формальные системы (ФС) – это совокупность чисто абстрактных объектов, не связанных с внешним миром, в котором представлены правила...
Эквивалентность двух определений элементарной формальной системы icon1 формальные теории 1 Основные положения
Мы рассмотрели две логических системы: алгебру высказываний и логику предикатов. Это было содержательное рассмотрение. Попытаемся...
Эквивалентность двух определений элементарной формальной системы iconВопросы коллоквиума №2
...
Эквивалентность двух определений элементарной формальной системы iconЭквивалентность пяти классов функций элементарных по кальмару
Определение. Функция называется элементарной по Кальмару, если ее можно получить й из функций s 1, I n m, x+y, x-y, S, а также конечного...
Эквивалентность двух определений элементарной формальной системы iconРабочая программа курса «числовые системы»
Схема построения аксиоматической теории. Свойства аксиоматических теорий: независимость, непротиворечивость, категоричность, эквивалентность...
Эквивалентность двух определений элементарной формальной системы iconВопрос 1 Переводческая эквивалентность. Прагматический аспект
Эквивалентность – это степень сходства между текстами ия и пя, измеряемая на определённом уровне
Эквивалентность двух определений элементарной формальной системы iconКонспект комплексного занятия в старшей группе по развитию речи и познавательному развитию "В заколдованном лесу"
Упражнять детей в подборе определений к существительным и образовании определений, согласовании определений с заданным словом в роде...
Эквивалентность двух определений элементарной формальной системы iconВычислительные Машины и Системы Математическое Обеспечение Вычислительных Систем Разработка формальной грамматики

Эквивалентность двух определений элементарной формальной системы iconНормальные формы функций
Элементарной дизъюнкцией высказывательных переменных из системы (1) называется дизъюнкция некоторых высказывательных переменных этой...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org