Choice functions and well-orderings over the infinite binary tree
Choice functions and well-orderings over the infinite binary tree
复制标题
无限二叉树上的选择函数和良序
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
I. Walukiewicz
中科院分区：
文献类型：
--
作者：
Arnaud Carayol;Christof Löding;D. Niwinski;I. Walukiewicz
本文给出了一个新的证明，证明了在一元二阶逻辑（MSO）中不可能在无限二叉树上定义一个选择函数。这个结果首先由Gurevich和Shelah使用集合理论论证获得。我们的证明要简单得多，只使用了自动机理论的基本工具。我们展示了如何使用结果来证明无限树语言的固有歧义。在第二部分中，我们加强了结果的不存在的MSO定义的良好的基础秩序的无限二叉树，通过显示，每一个无限的二叉树与良好的基础秩序有一个不可判定的MSO理论。
We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We show how the result can be used to prove the inherent ambiguity of languages of infinite trees. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.