No CrossRef data available.
We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
Published online by Cambridge University Press: 22 January 2016
The consistency of the natural number theory was proved, as is well known, by G. Gentzen in 1935 for the first time in such generality that the mathematical induction can be consistently used for any arbitrary predicate of natural numbers, which is well-formed in his system so that every quantifier ranges over all natural numbers.
This Part (VIII) depends logically only on Part (I), § l-§ 11 and Part (II), § 12-§ 15, Hamburger Abh. vol. 22. The superscript such as§11>‘1) is the reference to §11, Part (I).
1) In the sequel we refer to his second formulation given in Semesterber. Munster (1938).
2) Simple type theory is reasonable and useful in some cases. We can dispense with it in UL, however. For, let E be any variable, independent or dependent, and put E1 = E, 
denotes the power set of En-1
, and Eij, …, im = ‹Eij,…, Eim› (‹E1› = Ei). Then we get a simple type theory in UL of finite order with E as basic type, if we only restrict every variable x, free or bound, to some T=Ei1, …im (1≤i1, …, s1≤im) in such a way that 
The UL with a kind of universal independent variables is thus sufficient to construct simple type theories as subsystems of UL.
3) For some theory T it may happen that some restriction of the decomposition of some premises is assumed by the definition of T. For instance, if T contains N as its set, the negative proof constituent associated with the defining formula of N should be prohibited as in T0(N) in order that T be elementarily consistent.
4) By formal knowledge we mean always theorems deduced in UL or in a consistent subsystem of UL, while intuitive knowledge is not necessarily obtained by deductions.
5) The consistency proof of T1(N) contains some simplification of that of GN. in particular, the unnecessary complication in Gentzen’s proof caused by the “Verdünnung” is completely eliminated.
6) In defining the sets for induction for T1 a condition similar to that stated in (ii), §8, for T1(N) is necessary.
7) Some metalogical restriction of the decomposition of some premises of TΣ0 may be assumed as the negative proof constituent associated with the defining formula of N is prohibited in To(N). If there are such restrictions in TΣ0, the same restrictions shall be assumed in TΣ (note that Σ0≡Σ).
8) For intuitive meaning see introduction in Part (I).
9) The words used here such as minimal closure, all the direct products, any finite number etc. can and shall be understood as terms of intuitive mathematics.
10) In this stage of consistency proof the significance of the consistency is still very weak, since the intuitive meaning of the abstract algebraic systems does not used in the consistency proof, so that the harmony between intuitive and formal knowledge can not yet be extended to the algebraic systems considered. Here is not the place to enter into the formulation of this problem precisely. However, these considerations, together with T∑(N) discussed above, show some examples to combine abstract and concrete mathematics consistently.
11) This condition does not restrict the usual way of inference by mathematical induction.
12) Since cuts may occur in P1 the top sequence of P may be void.
13) In order to fix the [NN**] on which the next procedure is applied, we select the boundary [NN**] with minimum lexicographic P-order§6(1). Wherever there is an ambiguity in other places concerning the position of application of procedure, one may refer to the lexicographic P-order, which is, however, not mentioned explicitly in each case.
14) See the remark in §11. See also §18.
15) In order to avoid the confusion which may arise by the transformation in this § 15 about the substitution of eigen variables by the constants assigned to them, we should remember for each P1-formula the position where it was in P0, or else we should transform the proof of each step of our transformations to a proof with distinct eigen variables.
16) The ordinal number associated to a column of a P-constituent is called also the ordinal number associated to a formula which is in the column.
17) In order to make this inference valid, the a of 
is necessary.
18) In order to make this inference valid, the 1 of a+1 in (ii, a) is necessary.
19) Owing to lemma 2 we may transform the proofs appearing in each step of our transformation to the proofs with properties (a), (b), (c′), and (d), given in Part (II).
20) Note that owing to the definition of the height of a formula of a T1(N)-proof (§14) it follows from λ′<λ that the p-number of the formula directly upon the cut 
in (4) is smaller than the P-number of the formula directly upon the [NN**] in (1).
21) Since E is in the intuitive part, E is not an [NN**].
You have
Access