Portal de Periódicos da CAPES

On the theory of ordinal numbers

1957; Mathematical Society of Japan; Volume: 9; Issue: 1 Linguagem: Inglês

10.2969/jmsj/00910093

1881-1167

Gaisi Takeuti,

Logic, Reasoning, and Knowledge

In a former paper [3], the author formalized the theory of ordinal numbers in a logical system $G^{1}LC$ introduced in [4], and constructed in that theory the set theory of Fraenkel-von Neumann.The system $G^{1}LC$ is a large system containing the concept of ' arbitrary predicates '.Such a logical system Is convenient, on the one hand, in application.It allows us to form the theory of ordinal numbers, for example, on a quite simple system of axioms.On the other hand however, the nature of $G^{I}LC$ itself is not yet clarified.One does not know whether an analogue of Gentzen's theorem [1]: " Every pro- vable sequence in the system is provable without cut " (" Fundamental conjecture ) does or does not hold in $G^{1}LC$ .In this paper, we introduce a new logical system $FLC$ , obtained by a slight modification of $GLC$ .It will not contain the concept of " arbitrary predicates " but will contain that of "arbitrary functions".We shall prove that the " fundamental conjecture '' is valid in $FLC$ .The theory of ordinal numbers will be then reformalized in $FLC$ , and the set theory of Fraenkel-von Neumann will be constructed in it.The author has in view to show, in a forth-coming paper, that, conversely, the theory of ordinal numbers as formalized in this paper can be constructed in the Fraenkel-von Neumann set theory.The logical system $FLC$ is, as said above, a modification of $GLC$ .The formulas in $FLC$ consist of variables, functions of various types, predicates and logical symbols described below.It is to be noticed that we have a wider domain of types than in $GLC$ .Chapter I.The system of logic $FLC$.\S 1. Type symbols.The type symbol is defined recursively as follows.1.1.1.$0$ is a type symbol G. TAKEUTI 1.1.2.If $\alpha_{1},\cdots,$ $\alpha_{n}$ are type symbols, then $(\alpha_{1},\cdots, \alpha_{n})$ is a type symbol.$(n=1,2,3,\cdots)$The height of a type symbol is defined recursively as follows. 1.2.1.The height of the type symbol $0$ is zero.1.2.2.The height of the type symbol $(\alpha_{1},\cdots, \alpha_{n})$ is $h+1$ , where $h$ is the maximal number of the heights of $\alpha_{1},\cdots,$ $\alpha_{n}$ .\S 2. Variables Functions etc. 2.1.Variables, which are also called function of type $0$ or variable of type $0$ . Free variables$a,$ $b,$ $ c,\cdots$ 2.1.2.Bound variables $x,$ $y,$ $ z,\cdots$ 2.1.3.Special variables $0,$ $\omega,\cdots$ 2.2.Functions of type $\alpha$ (the height of $\alpha>0$ ), which are also called variable of type $\alpha$ .2.2.1.Free functions of type $\alpha$ $f\alpha,$ $g\alpha,$ $ h\alpha,\cdots$ 2.2.2.Bound functions of type $\alpha$ $p\alpha,$ $q\alpha,$ $ r\alpha,\cdots$ 2.2.3.Special functions $*^{\prime},$ $\max(*, *_{2}),\cdots$ Predicates$*_{1}=*2'*_{1}<*_{2}$ 2.4.Logical symbols 7, $\Lambda,$ $\vee,$ $\forall,$ $\exists$If no confusion is likely to occur, the notation may be abbreviated by the following conventions; we may write $f,p$ for $f\alpha_{1},p\alpha_{2}$ respec- tively.\S 3. Terms and functionals.Terms and functionals are defined recursively as follows.3.1.Every free or special variable is a term.3.2.Let $f_{1},\cdots,f_{n}$ be free functions of type $\alpha_{1},\ldots,$ $\alpha_{n}$ respectively, where $f_{i}\neq f_{j}$ , for $i\neq j$ .Moreover, let $p_{1},\ldots,p_{n}$ be bound functions of types $\alpha_{1},\cdots,$ $\alpha_{n}$ respectively such that $p_{1},\cdots,p_{n}$ are not contained in a term $T$ and $p_{j}\neq p_{j}$ for $i\neq j$ .If we substitute $p_{j}$ for $f_{i}$ In $T$ for all $i(1\leqq i\leqq n)$ at all places where $f_{i}$ are, and add $\{p_{1},\cdots$ , $p_{n}\}$ in front of the so constructed figure, then we obtain a func- tional of type $(\alpha_{1},\cdots, \alpha_{n})$ .3.3.Let $f$ be a free or a special function of type $(\alpha_{1},\cdots, \alpha_{n})$ and $F_{i}$ be a functional of type $\alpha_{j}(i=1,\cdots, n)$ .Then $f(F_{1},\ldots, F_{n})$ is a term.Term is called functional of type $0$ .