Расширения бета-теории лямбда-исчисления

16

Бета-эта-теория лямбда-исчисления является пост-полной. Можно ли добавить дополнительные правила, чтобы расширить бета-теорию лямбда-исчисления, чтобы получить противоречивые теории, помимо теории бета-эта?

постскриптум

Этот вопрос противоречил моему собственному правилу, согласно которому вопросы должны объяснять, почему это волнует опрашивающего.

Однажды ночью, незадолго до того, как этот сайт перешел в приватную бета-версию, меня поразило, что, поскольку экстенсиональность и принцип исключенного среднего связаны, правило eta является своего рода правилом экстенсиональности, и между интуиционистской и классической логикой существуют промежуточные логики, тогда было бы интересно, если бы существовала такая теория, как "промежуточная эта".

Если бы я сделал это, было бы очевидно, что ответ Евгения поднимает очевидную проблему в том, как я сформулировал вопрос, а не в том, что я хотел.

Чарльз Стюарт
источник

Ответы:

8

Да. Существует, например, бета + правило {s = t | s и t замкнутые неразрешимые условия}. Это, насколько я помню, не равно бета-эту, и соответствует. См. Mathgate для краткого описания и ссылки на Barendregt.

Евгений Торстенсен
источник
Это действительно правильный ответ на мой вопрос: бета-эта не равняется (\ xx x) (\ xx xx) и (\ xx x) (\ x. Xx), хотя они имеют одно и то же дерево Бёма. Я неправильно сформулировал вопрос: я после наблюдаемых различий. Я, вероятно, должен принять это и задать вопрос, который я хотел задать ...
Чарльз Стюарт
Я думал об этом ответе ... эта теория не порождена новыми правилами (неразрешимость неразрешима), и я не могу думать ни о каком стекающем наборе правил, который порождает подвластие этой теории. Но, насколько я знаю, может быть один. Итак, новый вопрос: cstheory.stackexchange.com/questions/398/…
Чарльз Стюарт
И мой ответ на этот вопрос показывает, что интуиция Евгения была здравой, и предоставляет правила комбинаторного переписывания для подтеории этого. Так принято.
Чарльз Стюарт