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

96
_- (2).(3).D|1- Hp.D ( =7v) (4)
L
1-.13513. Intax. p. (P **=a). o {a}.. (, = a). {a}:
L L
[(13-46)] D o {P.}.
[Hp] ) )o{}. -{ }
[Transp] 3. (o {a. } (P* )
L
[Hp] D:' (a — V). { a}. },* -a) (5)
L L
- (1)(3)(a). D - Hp D. o(v) U (ivA)() { } (6)
[Hp] U (i ) ) D
D ~ r) U (^)((. {}. )() *- { y}-). D (7)
L
- (6)(7). Z) Prop.
1.52 `- Hp 13514:- =Nc'(' U,, ( U,,A"':
A"' (T)," (P). (+ 1) = Nc(i. O(v) J (iv*)(.) U. A'
(V)
[110631]
13-521 -.Intax. 'Int(a). Z) 'Int(o — 1)
[13,514'51352]
13-53 -. Intax. ael(NCinduct - t' 0). Z) ['Int(a)
[120-47. 13-521-5-512
13-54 |- Intax 3 Infinax [13-53]
This is the theorem of Mr. Greniewski.
B. Realism and hyperrealism.
Let us assume the following definition:
Transcax (x). X S' Cls induct = (- ) ' 'Cis induct.
dJ a
If we assume Transcax, we can prove without any difficulty'
that V() is a finite class, i. e. a class which is not similar to any
proper part of itself, not being an inductive class. We also prove
the proposition:
Transeax ) Infinax.
It is easy to see that Transcax is not consistent with Multax.
Nevertheless there is an hypothesis, which is practically as much
fruitful as the multiplicative axiom, being consistent with the
Transcax. To get this hypothesis, I shall use the idea of self