When we say "there are men," that means that the propositional function " is a man" is sometimes true. When we say "some men are Greeks," that means that the propositional function " is a man and a Greek" is sometimes true. When we say "cannibals still exist in Africa," that means that the propositional function " is a cannibal now in Africa" is sometimes true, i.e. is true for some values of . To say "there are at least individuals in the world" is to say that the propositional function " is a class of individuals and a member of the cardinal number " is sometimes true, or, as we may say, is true for certain [Pg 159] values of . This form of expression is more convenient when it is necessary to indicate which is the variable constituent which we are taking as the argument to our propositional function. For example, the above propositional function, which we may shorten to " is a class of individuals," contains two variables, and . The axiom of infinity, in the language of propositional functions, is: "The propositional function 'if is an inductive number, it is true for some values of that is a class of individuals' is true for all possible values of ." Here there is a subordinate function, " is a class of individuals," which is said to be, in respect of , sometimes true; and the assertion that this happens if is an inductive number is said to be, in respect of , always true. The statement that a function is always true is the negation of the statement that not- is sometimes true, and the statement that is sometimes true is the negation of the statement that not- is always true. Thus the statement "all men are mortals" is the negation of the statement that the function " is an immortal man" is sometimes true. And the statement "there are unicorns" is the negation of the statement that the function " is not a unicorn" is always true.[38] We say that is "never true" or "always false" if not- is always true. We can, if we choose, take one of the pair "always," "sometimes" as a primitive idea, and define the other by means of the one and negation. Thus if we choose "sometimes" as our primitive idea, we can define: "' is always true' is to mean 'it is false that not- is sometimes true.'"[39] But for reasons connected with the theory of types it seems more correct to take both "always" and "sometimes" as primitive ideas, and define by their means the negation of propositions in which they occur. That is to say, assuming that we have already [Pg 160] defined (or adopted as a primitive idea) the negation of propositions of the type to which belongs, we define: "The negation of ' always' is 'not- sometimes'; and the negation of ' sometimes' is 'not- always.'" In like manner we can re-define disjunction and the other truth-functions, as applied to propositions containing apparent variables, in terms of the definitions and primitive ideas for propositions containing no apparent variables. Propositions containing no