26. Равенство и отношения порядка между ординальными числами

Мы введем сначала отношения порядка в терминах которых легко определяется отношение равенства

Конечное множество выражений вида или а где а и ординальные числа, будет называться секвенцией. Секвенции будут обозначаться через .

Мы будем рассматривать следующие два правила вывода:

Доказательство — это бесконечное дерево секвенций, в котором каждое разветвление является применением одного из правил вывода. В частности, верхние секвенции должны иметь вид Они

выводятся посредством первого правила вывода, когда а есть нуль, так что посылка выполнена автоматически. Говоря точнее, мы понимаем под бесконечным деревом секвенций ординальное число вместе с частично рекурсивной функцией, которая сопоставляет некоторую секвенцию каждому узлу этого ординального числа. Полагаем если выводима соответствующая секвенция.

тогда итолько тогда, когда длявсехп. Достаточность — просто применение первого правила выбора, а необходимость — следствие того факта, что обращение этого правила

имеет место как допустимое правило вывода. Мы доказываем это трансфинитной индукцией по длине доказательства посылки. Следует различать несколько случаев в зависимости от последнего применения правила в данном доказательстве секвенции а Если и это применение есть

то мы получаем по предположению индукции для всех тип. Отсюда по первому правилу вывода заключаем для всех что и требовалось доказать, Аналогично если и последнее применение правила есть

Остается рассмотреть случаи

и

в первом из которых все получается сразу, а во втором можно применить предположение индукции к

Г, а получая тем самым для всех Доказательство окончено.

Доказательство — трансфинитной индукцией по а, Допустим, что для всех Тогда по второму правилу вывода для всех так что по первому правилу вывода а а, что и требовалось доказать.

Мы докажем чуть больше, а именно что

имеют место как допустимые правила вывода. Это делается кратной трансфинитной индукцией. Индукционное предположение состоит в том, что первое правило справедливо для всех подординалов первого порядка ординалов а и у и что второе правило справедливо для всех подординалов первого порядка ординала Внутри индукционного перехода нам снова приходится применять трансфинитную индукцию, на этот раз предполагая, что правила справедливы, если уменьшилась длина вывода хотя бы одной из посылок.

Рассмотрим для начала первое правило. Следует различать несколько случаев в зависимости от последних применений правил в доказательствах посылок.

Основной случай возникает, когда они имеют вид

для некоторого

соответственно. В этом случае доказательство завершается следующими применениями правил:

Здесь верхние применения правил допустимы согласно предположению индукции по длинам доказательств посылок, а нижнее — согласно предположению индукции по

Второе правило рассматривается во многом тем же способом. Ограничимся случаем, когда последние применения правил в доказательствах посылок имеют вид

и

соответственно. Искомое заключение получается так:

Здесь верхние применения правил допустимы согласно предположению индукции по длинам выводов посылок, а следующее применение — согласно предположению индукции по а и у. Последние два применения — просто применения постулированных правил вывода. Доказательство окончено.

Если а то для всех . Из следует Таким образом, для всех так что а и требовалось доказать.

Транзитивность отношения следует из уже доказанного и того факта, что отношение сильнее, чем отношение

Достаточно доказать, что а для всех тк как тогда мы получим для всех что эквивалентно а Соотношение а доказывается трансфинитной индукцией по а с индукционным предположением для всех тип. Отсюда мы получаем по второму правилу вывода для любых а затем а по первому правилу вывода, что и требовалось доказать.

Следующую теорему можно рассматривать как конструктивный вариант теоремы о сравнимости ординальных чисел, которая в классической формулировке утверждает, что для любой пары ординальных чисел имеет место либо либо

Для любых ординалов а и доказуема секвенция

Мы докажем одновременной трансфинитной индукцией, что две секвенции

доказуемы. Индукционное предположение состоит в том, что первая секвенция доказана для всех подординалов первого порядка ординала а, а вторая секвенция — для всех подординалов первого порядка ординала Отсюда мы получаем

и

что и требовалось доказать.

Отношения а исключают друг друга.

Для того чтобы эта теорема имела место, необходимо и достаточно, чтобы было невозможно для любого ординала а. Учитывая непротиворечивость нашего исчисления, т. е. недоказуемость пустой

секвенции, достаточно доказать выводимое правило

что мы сделаем трансфинитной индукцией по а. Внутри индукционного перехода нам придется использовать трансфинитную индукцию по длине доказательства посылки. Если у и последнее применение правила в этом доказательстве есть

то мы получаем для всех следовательно, по первому правилу вывода. Аналогично и если Остается рассмотреть случаи

из которых более трудное — второе. Согласно предположению индукции по длине доказательства посылки мы получаем для некоторого что влечет Предположение индукции по а дает нам теперь искомое доказательство

Отношения равенства и неравенства между ординальными числами определяются следующим образом:

Рефлексивность, симметричность и транзитивность отношения следует из рефлексивности и транзитивности Далее, тот факт, что отношения а взаимно исключают друг друга, является непосредственным следствием несовместимости

Заметим, наконец, что если возможно, пустая или конечная последовательность ординалов, то это наименьший ординал а, такой, что для всех . А именно допустим, что для всех Тогда по первому правилу вывода как и утверждалось.