A note on a formalized arithmetic with function symbols ' and $+$
Tsuyoshi Yukami · Tsukuba Journal of Mathematics · 1978
Introduction.Let $\mathfrak{L}_{0}$ be the first order language with function symbols ' , $+and$ the equality symbol $=$ .By $\mathfrak{L}$ we denote the first order language obtained from $\mathfrak{L}_{0}$ by adding a ternary predicate symbol $P$ .The theory in $\mathfrak{L}$ with the following axioms and axiom schemata is signified by $\mathfrak{N}$ .(N-6) $\forall x\forall y\forall z\{P(x, y, z)\supset P(x, y^{\prime}, z+x)\}$ .(N-7) $\forall x\forall y\forall z\forall w\{(P(x, y, z)\wedge P(x, y, w))\supset z=w\}$ .(N-S) $\forall x(x=x)$ .In [3] we proved that: For any formula $\mathfrak{A}(a)$ of $\mathfrak{L}$ ; if there is a number $m$ such that, for any natural number $n$ , there exists a proof $\mathfrak{P}$ of $\mathfrak{A}(\overline{n})$ in $\mathfrak{N}$ with the following ProPerties (1) and (2), then $\forall x\mathfrak{A}(x)$ is provable in $\mathfrak{N}$ .(1) The length of $\mathfrak{P}$ is less than $m$ .(2) For any induction schema $\mathfrak{B}$ in $\mathfrak{P}$ which is not a formula of $\mathfrak{L}_{0},$ $b(\mathfrak{B})\leq m$ .The purpose of this paper is to prove the following theorem.THEOBEM.There are a fomaula $\mathfrak{A}(a)$ and a natural number $M$ such that: $(a)$