The theory of constructive types (principles of logic and mathematics). By Leon Chwistek.

67
73,841 I-.1 p 73-81. {w", DC}. {R,C}..Re 1 -.
D. -' sm Da R.." sma J R.
[73 8 21 83 84]
7 386 1-: JaR C DOS:. C7S C DR. extens (R). extens(S). D
a a:Eas CD a(RIS):. D(RIS)= DIR..(RIS) CU S:
a a a a
-ZD. (3x):R: {DaR,: K ), DaR sZ DaS
[73 86'8412. (0-252)]
73-88 1-. sm '. sm C': M' C (o:. o' C: "{X, K}. c/',W,, O', ),C}
I) sm C
This is the Schrôder-Bernstein theorem. Note that this theorem is true, when,, o', c, W' are of the type K, but it is not
proved for, M ' (o, o' being of the type. DaC.
VII. Cardinal numbers.
The Theory of Cardinal numbers, as given în Principia, is
based on certain conventions enabling us to deal with numbers of
ambiguous types. These conventions are far from being general
directions of tneaning, as they concern arithmetical operations.
These conventions being required in proofs'of propositions, can
hardly be-omitted, therefore it may be doubted whether we can
build up Arithmetic without supplementary directions. Now the use
of ascending cardinals seems to be scarcely possible without these.
Moreover it would be quite useless in our system, as we can
prove nothing concerning cardinal number of the Universum of
a given type. There is this essential difference between the Pure
Theory of Types and a simplified one, that the simplified Theory
enables us to prove that the cardinal number of the classes of
classes contained in a given class is greater than the cardinal number of this class 1). With this theorem we can prove that if a is
a cardinal number other than the null-class, there is a cardinal
1) Cf. Principia * 102 *.