Можем ли мы доказать слабую нормализацию для системы F индукцией по трансфинитному ординалу

16

Слабая нормализация для простого типизированного лямбда-исчисления может быть доказана (Тьюринг) индукцией по . Расширенное лямбда-исчисление с рекурсорами на натуральные числа (Генцен) имеет слабую стратегию нормализации по индукции на ϵ 0 .ω2ϵ0

А как насчет системы F (или слабее)? Есть ли слабое доказательство нормализации в этом стиле? Если нет, можно ли это сделать вообще?

Кава
источник
1
Это, вероятно , полезно отметить , что каждая последовательная (счетная) теория с достаточной выразительностью имеет «а» доказательство теоретико-порядковое меньше , чем определяется как наималейшие вычислимыми порядковой , который не является доказуемо обоснованным в данной теории. Хитрость описывает этот ординал "естественным" способом. ωСК
Коди

Ответы:

10

Наиболее полным обзором взаимосвязи между теорией конструктивного доказательства (которая тесно связана с теорией конструктивных ординалов) и импредикативной арифметикой второго порядка (которая, как указывает Ульрик, эквивалентна по силе Системе F) является Girard (1989). Там он опирается на свою теорию дилататоров (1981), которой я на самом деле не следую, но, по-моему, по сути, предоставляет неконструктивную теорию сколемизации высшего порядка.

Насколько я понимаю, вы не можете выразить формулу конструктивно в смысле епископа-Мартина-Лёфа, потому что они являются непредсказуемыми, и вы не можете их исключить, добавив какую-либо схему индукции первого порядка.Σ21

Я помню, как предлагал теоретическому ординалу, что можно просто оговорить, что вы можете обосновать непредсказуемый конструктивизм в теории типов, основанной на полиморфном лямбда-исчислении, и использовать технику сокращения кандидата из доказательства SN Жирара для системы F, чтобы наложить разумный общий порядок на вселенная конструкций, вызывающая классы эквивалентности, которые вы получаете от этих ординалов; он сказал что-то умное, что я забрал, сказав, что вы можете заставить это работать, но у этого будут все преимущества воровства перед честным трудом. Чтобы заставить его работать, недостаточно, чтобы вы могли доказать в теории множеств существование таких ординалов, вам понадобится конструктивное доказательство трихотомии для порядка.

Подводя итог, можно сказать, что благодаря регулярному понятию интуиционистской конструкции, присущему епископу - Мартину-Лёфу, литература, о которой я знаю, настоятельно не рекомендует. Если вы не склонны к честному труду и примете чрезмерный конструктивизм, то я думаю, что это возможно сделать. Естественно, вам понадобится более сильная теория, чтобы Система F конструктивно доказывала требуемую трихотомию, но Исчисление Индуктивных Конструкций предоставляет очевидного кандидата.

Ссылки

  1. Girard, Жан-Ив (1981), -logic. I. Дилаторы, Анналы математической логики 21 (2): 75–219.Π21
  2. Жирар (1989) Теория доказательств и логическая сложность, вып. Я , Неаполь: Библиополис. Там нет тома II.
Чарльз Стюарт
источник
13

Π20ω2

ε0Γ0

Надеемся, что однажды кто-нибудь придумает порядковую запись для арифметики второго порядка, что все согласятся, что это естественно, и затем это можно было бы честно использовать, чтобы доказать слабую нормализацию для Системы F.

Ульрик Бухгольц
источник
11

NN

Кроме того, я думаю, что арифметика второго порядка довольно сильна, и что ее «теоретический ординал доказательства» еще не известен конструктивной верхней границей ( Искусство ординального анализа, раздел 3 ).

Я думаю, что эта конструктивная порядковая граница - это то, что необходимо для выполнения индукции, которую вы запрашиваете.

jbapple
источник