Доказуемое и недоказуемое - Манин Ю.И.
Скачать (прямая ссылка):
Имеется, вероятно, уникальный пример целой книги с сознательно введенной двумерной (блочной) структурой: Ч. Линдси, С. ван дер Мюйлен «Неформальное введение в Алгол-68» [23]. Она состоит из 8 глав, каждая из которых разбита на 7 параграфов (в числе которых для соблюдения системы восемь пустых!), Пусть (г, /) —'Имя /-го параграфа /-й главы, тогда книгу можно изучать «по строкам» матрицы (i, /) или по ее «столбцам», в зависимости от намерений читателя.
Как и все великие предприятия, это плод попытки решить, по всей видимости, неразрешимую задачу, ибо, по замечанию авторов, Алгол-68 нельзя описать для того, как он уже описан.
Kerf 1-Кегд Кег h
Глава II
ИСТИННОСТЬ И ВЫВОДИМОСТЬ
1. ЛЕММА ОБ ОДНОЗНАЧНОМ ЧТЕНИИ
Основное содержание этого параграфа — лемма 1.4 и определения 1.5 и 1.6. Лемма гарантирует однозначность расши-фровки термов и формул любого языка класса 2?\ и служит основой большинства индуктивных рассуждений. Читатель может принять ее на веру, если он сумел самостоятельно проанализировать последнюю формулу в п. 3.7 гл. I. Важно помнить, что конструкция любого формального языка начинается с заботы о недвусмысленности синтаксических правил.
Начнем со стандартных комбинаторных определений, чтобы фиксировать терминологию.
1.1. Пусть А — некоторое множество. Последовательностью длины п из элементов А называется отображение множества.{1, ..., п} в А. Образ ? при этом отображении называется ?-м членом последовательности. Значению п—0 отвечает пустая последовательность. Последовательности длины 1 иногда будут отождествляться с элементами А. '
Последовательность длины п записывается также в виде где щ — ее ?-й член. Число ? называется номером члена щ. Если Р=(аи ап), б)=(Ьи ..., Ьт)—две последовательности, их соединением Р(3 называется последоватздьность (а1, ..., ап, Ьи ..., Ьт) длины т + п, ?-й член которой есть а* при ?<;«, &,-п при п+1^Р^п+т. Аналогично определяется соединение конечной последовательности последовательностей.
Вхождением последовательности в Р называется любое представление Р в виде соединения PiQPг. Подставить последовательность Р вместо данного вхождения в Р — значит построить последовательность Р1рР2-
Пусть П+, П~—два неп'ересекающихся подмножества в {1, ... ..., «}. Отображение с: П+-+П- называется скобочной биекцией, если оно биективно и удовлетворяет условиям:
а) с(?)>? для всех ?еЯ+;
б) для каждого ? условие /е[?, с(?)] равносильно с(/)е «е[?, с (?) ].
1.2. Лемма.
Для данных П+, П~, если скобочная биекция существует, то она единственна.
Эта лемма будет применяться к выражениям в языках класса 2\\ П+ — номера мест в данном выражении, на которых стоит открывающаяся скобка, П~—номера мест, на которых стоит закры-
25
вающая скобка, отображение с сопоставляет каждой открывающей скобке соответствующую закрывающую.
Доказательство. Пусть функция е : {1, ..., п}—>-{0, ±1} принимает значение 1 на Я+, —1 на Я- и 0 в остальных местах. Утверждается, что тогда для каждого ?еЯ+, любой скобочной биекции с: П+—*-П~ и люббго ? (1=^6^ ^с(?)—1) выполнены соотношения
С (/) с (1)-к
2*(Л=°. 2 * СП> 0.
/=« /=/
Доказав их, мы установим лемму, ибо получим следующий рецепт, однозначно восстанавливающий с по Я+, П~ : с(?) есть наименьшее />г, для кото-I
рого 2 5 (Л = °-/=‘
Первое соотношение следует из того, что элементы Я+ и П~ входят в отрезок [?, с(?)] только парами (у, с(/)) и в(у)+в(с(у')) =0. Для доказательства
с (/) — к
второго допустим, что для некоторых I, к имеем 2 е0)^=0- Так как
у=?
с (I) —к
е (?) = 1, то 21 е(у)<0. Значит, на отрезке [?+1, с(?)—к\ число элементов|
/=г + 1
из Я- строго больше, чем из Я+. Пусть сЦа)<=П~ — такой элемент на этом отрезке, что /о [?+1, с(г)—6]. Тогда у‘о=ёД, даже /о<?, ибо с (г) лежит вне отрезка. Значит, лишь одни член пары /о, с (уо) лежит в [«', с(?)], что противоречит определению с,
1.3. Пусть теперь А—алфавит некоторого языка Ь класса 9?
меров закрывающих скобок существует скобочная биекция. Действительно, новые скобки в п. 1.3а, б находятся в естественной биекции, а старые (скрыты в сокращенных записях 1и ..., К, Р, <2) допускают такую биекцию по индуктивному предположению. Кроме того, новые скобки не разрезают пар старых.
Теперь мы можем сформулировать основной результат параграфа.
1.4. Лемма об однозначном чтении.
Каждое выражение языка Ь является либо термом, либо фор' мулой, либо ни тем, ни другим.
Эти альтернативы, а также все альтернативы, перечисленные в п. 1.3а, б являются взаимоисключающими.
Каждый терм (соответственно формула) представляется точно в одном из видов, описанных в п. 1.3а (соответственно п. 1.3,6), и однозначно.
Кроме того, по ходу доказательства мы установим, что если некоторое выражение является соединением конечной последовательности термов, то оно представляется в таком виде однозначно.
Доказательство. Проведем индукцию по длине выражения и опишем неформально алгоритм синтаксического анализа, однозначно выясняющий, какая из альтернатив имеет место.
а) Если в выражении Е нет скобок, то оно является либо термом-константой, либо термом-переменной, либо не термом и не формулой.
