On predicates with constructive infinitely long expressions
Gaisi Takeuti, Akiko Kino · Journal of the Mathematical Society of Japan · 1963
In recent years the logic with infinitely long expressions has been considered and developed by Berkeley school.(For this see [1], [2], [7] and also cf.[6].)In this paper, we shall consider ' constructive ' infinitely long expres- sions.In the following we shall give a language for the logic with infinitely long expressions and define a ' formula with constructive infinitely long expressions' as a formula with infinitely long expressions (sometimes called simply a formula) to which a so-called Godel number is assigned.We shall show that the nesting number of a formula with constructive infinitely long expressions (see below) is less than Church-Kleene's $\omega_{1}$ (Theorem 1).Moreover we shall establish a correspondence between formulas with constructive infinitely long expressions and predicates in Kleene's analytic hierarchy (cf.[4]).We shall prove that a formula $\mathfrak{A}$ with constructive infinitely long expressions is representable in the(Theorem 2).On the other hand, any predicate expressible in the n-function quantifier form is representable by a formula $\mathfrak{A}$ with constructive infinitely long expressions such that $n^{\prime}(?l)=n$(Theorem 3).We shall also prove that every hyperarithmetical formula is representable by a quantifier-free formula with constructive infinitely long expressions (Theorem 4).0. In this paper we shall use the following language:Prime formulas are of the form $i=j,$ $i=v_{n},$ $v_{m}=j$ and $v_{m}=v_{n}$ , where $i$ and $j$ are individual constants.Formulas are composed from prime formulas as follows: 0.1.If $\mathfrak{A}$ is a formula, then $7\mathfrak{A}$ is a formula.