Peter Andrews has proposed, in 1971, the problem of finding an analog of the Skolem theorem for Simple Type Theory. A first idea lead to a naive rule that worked only for Simple Type Theory with the axiom of choice and the general case has only been solved, more than ten years later, by Dale Miller. More recently, we have proposed with Th{\'e}r{\`e}se Hardin and Claude Kirchner a new way to prove analogs of the Miller theorem for different, but equivalent, formulations of Simple Type Theory. In this paper, that does not contain new technical results, I try to show that the history of the skolemization problem and of its various solutions is an illustration of a tension between two points of view on Simple Type Theory: the logical and the theoretical points of view.

翻译：Peter Andrews于1971年提出了在简单类型理论中寻找斯科伦定理类似物的问题。最初的一个想法引出了一种朴素规则，该规则仅适用于带有选择公理的简单类型理论，而一般情形在十多年后才由Dale Miller解决。最近，我们与Thérèse Hardin和Claude Kirchner合作，提出了一种新的方法，用于证明Miller定理在不同但等价的简单类型理论表述中的类似形式。本文不包含新的技术成果，试图展示斯科伦化问题及其各种解决历史如何体现了简单类型理论中两种观点——逻辑观点与理论观点——之间的张力。