*9. Extension of the Theory of Deduction from Lower to Higher Types of Propositions
Summary of *9.
In the present number, we introduce two new primitive ideas, which may be expressed as " is always[1] true" and " is sometimes[1] true," or, more correctly, as " always" and " sometimes." When we assert " always," we are asserting all values of , where "" means the function itself, as opposed to an ambiguous value of the function (cf. pp. 15, 42); we are not asserting that is true for all values of , because, in accordance with the theory of types, there are values of for which "" is meaningless; for example, the function itself must be such a value. We shall denote " always" by the notation
,
where the "" will be followed by a sufficiently large number of dots to cover the function of which "all values" are concerned. The form in which such propositions most frequently occur is the "formal implication," i.e. such a proposition as
,
i.e." always implies ." This is the form in which we express the universal affirmative "all objects having the property have the property ."
We shall denote " sometimes" by the notation
.
Here "" stands for "there exists," and the whole symbol may be read "there exists an such that ."
In a proposition of either of the two forms ,, the is called an apparent variable. A proposition which contains no apparent variables is called "elementary," and a function, all whose values are
↑ 1.01.1We use "always" as meaning "in all cases," not "at all times." A similar remark applies to "sometimes."