作者: Alonzo Church
DOI: 10.2307/2272393
关键词:
摘要: In this paper we treat the ramified type theory of Russell [6], afterwards adopted by Whitehead and in Principia mathematica [12], so that may compare Russell's resolution semantical antinomies with now widely accepted them method Tarski [7], [8], [9].To avoid impredicativity essential restriction is quantification over any domain (type) must not be allowed to add new members domain, as it held adding changes meaning such a way vicious circle results. As point out, there no one particular form doctrine types indispensable accomplishing restriction, they have themselves offered two different versions hierarchy first edition (see Preface, p. vii). The version §§58–59 writer's [1], which will followed paper, still slightly different.To distinguish Russellian or sense from simple types, let us call former r-types.There an r-type i individual variables belong. If β1, β2, …, βm are given r-types, m ≧ 0, (β1, βm)/n belong m-ary functional level n, n 1. (α1, α2, αm)/k said directly lower than if α1 = α2 αm βm, k < n.