The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consistent and that proofs strongly normalize in this theory. Deduction modulo is a formulation of first-order logic with a general notion of cut. It is known that proofs normalize in a theory modulo if it has some kind of many-valued model called a pre-model. We show in this paper that the Stratified Foundations can be presented in deduction modulo and that the method used in the original normalization proof can be adapted to construct a pre-model for this theory.
翻译:分层基础是对朴素集合论的一种限制,其中概括方案被限制于可分层命题。已知该理论是一致的,且其中的证明可以强规范化。模演绎是一种带有广义切割概念的一阶逻辑形式化。已知如果一个模理论具有某种称为前模型的多值模型,则其中的证明可以规范化。本文表明,分层基础可以在模演绎中呈现,并且原始规范化证明中使用的方法可以适应于为该理论构建一个前模型。