构造性序数理论
Constructive theory of ordinals
AI总结：
本文提出一种仅基于两种序关系的构造性序数理论，利用上确界运算与序关系的相互作用逼近线性序概念，证明其满足构造性性质，加入经典逻辑可恢复通常序数但会损失可计算性。
摘要：
Martin-Löf在其《构造性数学札记》的第3章中描述了递归构造的序数，给出了Kleene可计算序数的构造性可接受版本。实际上，从构造性视角来看，并不需要图灵对可计算函数的定义。本文提出了一种与Martin-Löf理论类似的构造性序数理论，但仅基于“$x \nleq y$”和“$x < y$”两种关系，即不考虑直观含义为经典析取的矢列式。在我们的框架中，“序数的上确界”运算通过与“$x \nleq y$”和“$x < y$”关系的相互作用发挥重要作用。这使得我们在“$α\nleq β$ 或 $β\nleq α$”这一性质仅能在经典逻辑中得证的情况下，能够尽可能逼近线性序的概念。我们的目标是给出符合直觉的形式化定义，并证明我们的构造性序数能在构造性意义下满足所有期望的性质。需要注意的是，通过加入经典逻辑，我们可以恢复通常经典数学中的序数，但代价是大多数以通常形式给出的命题会丧失可计算性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
