Abstract
1.1 It is assumed that the reader is familiar with the definition of the system K of basic logic [5,8,11,12] and the system K' of extended basic logic [7,10] as described by Fitch. In order to avoid confusion between various formulations of basic logic and extended basic logic, a sketch of a definition of these systems which is similar to the definitions given by Hermes [15] is given here. 1.2 This essay is organized as follows. In section 2 there is a definition of the system K together with a statement of a number of theorems about the system. The subject of section 3 is K'. Section 4 contains some results, which are used in section 6. The relation of identity of the system R of combinatory logic [19,20] is defined and it is shown that this relation is completely represented in K'. There is an outline of a proof that the identity relation of R and, consequently, its theory of numbers and functions of numbers are available in K'. Section 5 contains an informal discussion of constructible ordinals in the second number class. This is preparation for the two main sections: 1.3 The concept of a U-expression representing an ordinal is introduced in section 6. It is shown that each Church-Kleene [1] ordinal is represented by a M-expression and that there is a U-expression which completely represents the set of U-expressions which represent ordinals. Schutte [21] introduces ordinals by defining another order relation on the natural numbers. After this is done, it is easy to establish connections between constructive ordinals and the natural numbers in Schutte's ordering. In section 7 it is shown that Schutte's order relation is completely represented in K' and that transfinite induction on these ordinals is a derived rule of K'. 1.4 The remainder of this section contains a statement of notational conventions and a definition of the set U of well-formed formulas (wffs) of the systems K' and K'. The conventions used here are taken from the Dictionary of Symbols of Mathematical Logic [4]. 1.5 Convention. An expression consisting of single quotation marks together with the expression enclosed by them serves as a met linguistic name for the expression thus enclosed. For example, the following expression is used as a name for the following expression 'a' is used as a name for the following expression 'a' . 1.6 Convention. If an expression contains occurrences of the following italic letters, with or without subscripts, 'a', 'b', 'c', 'd', 'x', 'y', 'z' or is itself one of these letters, then the total expression serves as a met linguistic variable referring to one or more expressions obtainable from the expression by replacing these letters by wffs in various ways. Numerical sub scripts attached to these letters are, of course, counted as parts of the letters. For example, the expression 'b' serves as a met linguistic variable which refers to wffs. 1.7Convention. The lower case italic letters i j k m n are used as met variables whose range is natural numbers. Furthermore, as a general convention, if an expression in Roman type occurs, the object, which it represents, will appear in italics. For example, 1'0','1','2',...are U expressions which represent the natural numbers 0, 1, 2, ., respectively. 1.8Definition. The set U of well-formed formulas (also the set of U-expressions) is defined inductively as follows: (1)'#' Is a wff. (2)If 'a' and 'b' are wffs then '(ab)' is a wff. (3) The only expressions which are wffs are those which can be shown to be such by virtue of (1) and (2). 1.9 Convention. Outermost parentheses of wffs may be omitted if no ambiguity results from doing so. When internal parentheses are omitted from wffs, the omitted parentheses are to be thought of as inserted as far to the left as is consistent with the expression being well-formed. For example, 'abc' is an abbreviation for '(ab)c' which is an abbreviation for '((ab)c)'. Also, '[b a c]', with spaces left on each side of the central expression, serves as an abbreviation for 'abc'; if there is no possibility of confusion, the outer square brackets are omitted. 1.10 '#(##)', '#(###)', "#(####)' and "#(#####)' are abbreviated as '=', 'v', '&', and 'A', respectively. Also, we assign the following abbreviations: 'x1' for '#(######)' 'X2' for '#(########)' 'A3' for '#(##########)' . . . 'xn' for '#. . .)' 2n+4 times