论文标题
序言的建设性理论
Constructive theory of ordinals
论文作者
论文摘要
在他关于建设性数学的笔记的第3章中，Martin-L {Ö} F递归构造了序数。他给出了Kleene的可计算序列的建设性可接受的版本。实际上，从建设性的角度来看，不需要可计算功能的图灵定义。我们在本文中给出了一种与Martin-L {Ö} F的理论相似的序词的建设性理论，但仅基于两个关系“ $ x \ leq y $”和“ $ x <y $”，即，即没有考虑其直觉含义的序列是经典的分离。在我们的环境中，“列出的至高无上”的操作通过与关系“ $ x \ leq y $”和“ $ x <y $”的互动来发挥重要作用。这使我们能够尽可能多地接近线性顺序的概念，当时仅在经典逻辑中才能证明“ $α\ leqβ$或$β\ leqα$”的属性。我们的目的是给出与直觉相对应的正式定义，并证明我们的建设性列入符合建设性的所有理想特性。请注意，通过添加经典逻辑，我们将以通常的大多数语句以通常形式给出的大多数语句的损失，以丧失可计算性。
In Chapter 3 of his Notes on constructive mathematics, Martin-L{ö}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-L{ö}f's theory, but based only on the two relations "$x \leq y$" and "$x < y$", i.e., without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation "supremum of ordinals" plays an important rôle through its interactions with the relations "$x \leq y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$α\leq β$ or $β\leq α$" is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties. Note that by adding classical logic, we would recover the ordinals of usual classical mathematics, at the cost of a loss of computability for most statements given in the usual form.
