Теория формальных грамматик - Гросс М.
Скачать (прямая ссылка):
47
2.4.4. Выводимость
Пусть Ф = (fi, /2, - • -, h)—упорядоченное множество (последовательность) формул.
Если существуют правило К и формула х, такие, что Ф9Ъс, то X называется непосредственным следствием из Ф.
Множество правил вывода R определяет, таким образом, отношение непосредственной выводимости: ФЯ* тогда и только тогда, когда существует правило вывода К, такое, что Ф№х. Отношение R определяется в декартовом произведении множества последовательностей формул на множество формул.
Пусть M — произвольное множество формул. Обозначим через Eo объединение M и множества аксиом. Образуем всевозможные конечные последовательности элементов E0 и добавим к E0 все формулы, являющиеся непосредственными следствиями из таких последовательностей. Полученное множество обозначим через Ei. Построим, далее, множество E2 с помощью E1 точно так же, как Ei строилось с помощью E0, и т. д. Формулы, принадлежащие Ei, E2, ..., En, ..., будем называть выводимыми из М, или следствиями из М. Выделяя формулы, действительно участвующие в получении выводимой из M формулы у, получим вывод этой формулы из М. (Точнее, вывод есть дерево, строящееся следующим образом: корнем его служит у, в концах дуг, исходящих из корня, стоят формулы, непосредственным следствием которых является у, и т. д.; висячие вершины дерева будут элементами E0.) Запись
MH= У означает, что «у выводима из M в ®».
®
Замечания, a) M определяется только составом своих элементов; их порядок значения не имеет. Множество M называется множеством посылок.
б) Если множество N содержит все элементы из M (Mcr N) и
M I= г/, то ясно, что N f=-= г/; иначе говоря, к посылкам можно при-
® ®
соединять любые другие.
в) Из непосредственной выводимости следует выводимость.
г) Всякая формула выводима из самой себя.
2.4.5. Теоремы
Формулы, выводимые из аксиом некоторой формальной системы, называются ее теоремами.
Характеристическое свойство теорем состоит в том, что они выводимы из любого множества посылок, в том числе — из пустого множества.
Вместо 0 I= г/ мы будем писать сокращенно \=у. @ ®
2.4.6. Упражнения
1. Доказать, что из непосредственной выводимости следует выводимость и что всякая формула выводима из самой себя. 48
Часть /. Предварительные сведения из логики и алгебры
2. Определим формальную систему, имеющую тот же алфавит, то же множество формул и то же правило вывода, что и система, введенная выше (стр. 42—44), для описания исчисления высказываний.
Схемы аксиом этой системы таковы:
Tl'. [X г> [К => X] ].
12'.
ТЗ'. ["I X zd [X => Y] ]. Выяснить, являются ли следующие формулы теоремами:
(1) [[KrDZ]:=) [[X=DK] ^[XrDZ] 11;
(2) [X :=>[[*:=> Г] =>П]ї
(3) [[X zdY]ZD [[Y ZD Z]ZD[X ZD Z]].
3. Можно ли в рамках системы поедыдущего упражнения вывести [Y ^IXzdZ]] из [Xzd [Yzd Z]]?
4. В п. 2.3.1 мы рассматривали бесконечный алфавит. Показать, что определение можно изменить таким образом, чтобы алфавит был конечным.
5. В п. 2.2.1 были приведены некоторые аксиомы, касающиеся точек и прямых.
Опираясь на семантические соображения, т. е. привлекая содержательную интерпретацию формальной системы, показать, что аксиома «через две точки можно провести только одну прямую» не следует из аксиомы «через любые две точки можно провести некоторую прямую».
Для этого можно, например, заменить слово «точка» словом «штучка», а слово «прямая» — словом «вещь». Затем надо подобрать такую интерпретацию штучки и вещи, для которой вторая аксиома выполняется, а первая — нет. Глава III КОМБИНАТОРНЫЕ СИСТЕМЫ
Комбинаторные системы — это формальные системы особого типа. Как показывает само их название, они используются при исследовании задач комбинаторного характера (а именно, относящихся к словам).
Введем сначала понятия, необходимые для формулирования правил вывода в комбинаторной системе.
Будем рассматривать свободную полугруппу, определенную над алфавитом
Я = {а,| 1 <г<п};
в примерах буквы этого алфавита обозначаются строчными латинскими буквами.
Напомним, что через E обозначается пустое слово, а через |Л| —длина слова А.
§ 3.1. ОПРЕДЕЛЕНИЕ КОМБИНАТОРНЫХ СИСТЕМ
3.1.1. Продукции
Когда мы говорили об исчислении слов, мы рассматривали двусторонние соотношения вроде 'ара' ~ \ю\
В настоящей главе мы встанем на несколько иную точку зрения, а именно введем в наши правила направление.
Попытаемся построить как можно более общее определение, из которого в дальнейшем будет получено много полезных определений более частного вида. Пусть имеется упорядоченная шестерка слов (G, Я, К\ Є, Я, К), записанных в алфавите 9L Рассмотрим слово X вида
X = GPHQK,
т. е. слово, начинающееся вхождением слова G, за которым следует вхождение И, отделенное от G вхождением некоторого слова P (возможно, пустого) и оканчивающееся вхождением слова К, отделенным от H вхождением слова Q (которое также может быть пустым).
Замещая вхождения G1HnK вхождениями слов G, H и К соответственно, мы получаем слово Y = GPHQK. 50
