Теория формальных грамматик - Гросс М.
Скачать (прямая ссылка):
Сначала мы определим элементарные теоремы с помощью следующих соглашений:
Если слова X, Y, Z— формулы, то
Tl. [X zd [F zd X] ] есть элементарная теорема. Т2. [ =э ~i F]zd [У =э X] есть элементарная теорема. ТЗ. [ [X =э [Y=>Z] ] =э [ pf =э Г] =э [X =э Z]]] есть элементарная теорема.
Т4. Других элементарных теорем нет.
Если рассматривать элементарные теоремы как аксиомы, то выражения Tl—ТЗ, принадлежащие метаязыку, будут схемами аксиом.
Легко убедиться в том, что элементарные теоремы являются формулами в силу F2 и F3. Нетрудно показать также, что для любого слова M можно решить, является это слово элементарной теоремой или нет.
2.3.4. О выборе элементарных теорем
Отметим, что Tl отражает «квазипарадоксальный» характер импликации. Т2 есть правило контрапозиции. Необходимо oco6d обратить внимание на следующий факт: когда мы используем содержательное понятие истины, ясно, что
поэтому в этом случае безразлично, писать
[~l X ZD Г] [Y => X]
или
[Уг51]э[п1зп У].
Однако дело обстоит совсем не так, когда мы с самого начала не прибегаем к понятию истины (тг е. когда мы имеем в виду другую интерпретацию).
Выбор ТЗ обусловлен техническим удобством. Исходя из элементарных теорем, мы будем строить теоремы, задав a priori правило вывода.
2.3.5. Правило вывода
Если слова X и У] суть теоремы, то слово Y — тоже теорема.
Легко видеть, что теоремы обязательно являются формулами. Заметим, что введенное нами правило есть известное правило modus ponens. Г л //. Общие сведения о формальных системах
45
2 3.6• Примеры вывода
В качестве примера и одновременно упражнения мы покажем, ЧТ0 [ol ol] И вообще [X ZD X] суть теоремы.
Для этого мы построим теорему, в которой [aiZDui] окажется в позиции Y из правила 2.3.5.
(1) UI является формулой в силу Fl.
(2) Слово [ai zd ai], которое мы будем обозначать впредь через М, является формулой в силу (1) и F3.
(3) Слово [ai zdM] является формулой в силу (1), (2) и F3.
(4) Слово [ai ZD М] является теоремой в силу (1) и Tl.
(5) Слово [ai zd [М zd aj]] является теоремой в силу (1), (2) и Tl.
(6) Слово [Ia1 zd [Mzd aj] zd [[o1 zd М] zd [ai zdaj]], структура которого может быть изображена деревом
является теоремой в силу (1), (2) и ТЗ.
(7) Правая часть слова (6), под которой на рисунке помещена стрелка, является теоремой в силу (5), (6) и правила modus ро-nens.
(8) [ajZDaj] является теоремой в силу (4), (7) и правила modus ponens.
Точно так же можно доказать, что для любой формулы X выражение [X zd X] является теоремой.
2.3.7. Заключение
Итак, соблюдая некоторые «правила игры», мы построили «систему», состоящую из двух связанных частей. Мы можем придать этой системе определенный смысл: она формализует «исчисление высказываний, рассматриваемое на интуитивном уровне понимания»; стало быть, она формализует в какой-то степени «логику здравого смысла».
Заметим, что построенная система не зависит от интерпретации, которую мы ей даем; возможны и другие интерпретации.
I[а, э [м э о-,]] з Ia1 э м] о [а, 3 ^J 46
Часть /. Предварительные сведения из логики и алгебры
Теперь остается показать, каким образом в рамках данной формальной системы можно было бы, действуя вполне строго, ввести истинностные значения; однако мы этого делать не будем.
§2.4. ОПРЕДЕЛЕНИЕ ФОРМАЛЬНОЙ СИСТЕМЫ
2.4.1. Формальные системы
Резюмируем сказанное выше о формальных системах. Мы будем называть логистической системой') упорядоченную четверку множеств:
© = <$, 8, 2Ї, R),
где X — счетный алфавит, буквы которого могут считаться перенумерованными;
S — (формальный) язык над X, или множество формул (Sc=X*);
ЭД — некоторое подмножество множества S1 или множество аксиом, задаваемое с помощью схем аксиом;
R — множество правил вывода (их вид уточняется ниже).
2.4.2. Правила вывода
Рассмотрим декартово произведение S X ... X S, состоящее из п сомножителей (п1); его элементами являются упорядоченные гс-ки формул.
Правило вывода Я есть правило, позволяющее поставить в соответствие каждой ti-ке {уи у2.....уп) из некоторого подмножества произведения S X ... X S одну определенную формулу X.
Более точно, правило Я определяется некоторым подмножеством декартова произведения g" X S, причем это подмножество должно обладать следующим свойством: ни для какой м-ки {У\, У2, • • • > Уп) ^ Sn не может существовать более одной формулы xeg, для которой {{у и у2, ..., уп),х) принадлежит данному подмножеству. Областью определения правила Я является некоторое подмножество Sn-
При конкретном применении правила вывода формулы уи ... ..., уп называют посылками, а формулу х — заключением-, посылки и заключение вместе суть аргументы примененного правила.
2.4.3. Комбинаторные системы
Если алфавит X конечен, S совпадает с X* и имеется ровно одна аксиома, то © представляет собой комбинаторную систему, комбинаторные системы будут рассмотрены ниже (см. гл. III).
•) Термин заимствован у Ж. Порта (Porte J., Recherches sur la theorie generale des systemes formels et sur Ies systemes connectifs, Paris, Gauthier-Villars, 1965). Г л //. Общие сведения о формальных системах
