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 E_n-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=E_i1, …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 T₁(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 T₁ a condition similar to that stated in (ii), §8, for T₁(N) is necessary.

7) Some metalogical restriction of the decomposition of some premises of TΣ₀ 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Σ₀, the same restrictions shall be assumed in TΣ (note that Σ₀≡Σ).

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 P₁ 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§⁶(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 P₁-formula the position where it was in P₀, 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 T₁(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**].