The propositional calculus is characterized by the fact that all its propositions have as hypothesis and as consequent the assertion of a material implication. Usually the hypothesis is of the form p implies p, etc. which (§ 16) is equivalent to the assertion that the letters which occur in the consequent are propositions. Thus the consequents consist of propositional functions which are true of all propositions. It is important to observe that, though the letters employed are symbols for variables, and the consequents are true when the variables are given values which are propositions, these values must be genuine propositions, not propositional functions. The hypothesis p is a proposition is not satisfied if for p we put x is a man, but it is satisfied if we put Socrates is a man or if we put x is a man implies x is a mortal for all values of x. Shortly, we may say that the propositions represented by single letters in this calculus are variables, but do not contain variables—in the case, that is to say, where the hypotheses of the propositions which the calculus asserts are satisfied.(§ 14 ¶ 1)