connectives are only "" for negation of the immediately following proposition and "" for implication from antecedent to consequent propositions: Each of these patterns is an axiom schema, a rule for generating an infinite number of axioms. For example, if , , and are propositional variables, then and are both instances of axiom schema 1, and hence are axioms. It can be shown that with only these three axiom schemata and modus ponens, one can prove all tautologies of the propositional calculus. It can also be shown that no pair of these schemata is sufficient for proving all tautologies with modus ponens. Other axiom schemata involving the same or different sets of primitive connectives can be alternatively constructed. These axiom schemata are also used in the predicate calculus, but additional logical axioms are needed to include a quantifier in the calculus. First-order logic Axiom of Equality. Let be a first-order language. For each variable , the formula is universally valid. This means that, for any variable symbol the formula can be regarded as an axiom. Also, in this example, for this not to fall into vagueness and a never-ending series of "primitive notions", either a precise notion of what we mean by (or, for that matter, "to be equal") has to be well established first, or a purely formal and syntactical usage of the symbol has to be enforced, only regarding it as a string and only a string of symbols, and mathematical logic does indeed do that. Another, more interesting example axiom scheme, is that which provides us with what is known as Universal Instantiation: Axiom scheme for Universal Instantiation. Given a formula in a first-order language , a variable and a term that is substitutable for in , the formula is universally valid. Where the symbol stands for the formula with the term substituted for . (See Substitution of variables.) In informal terms, this example allows us to state that, if we know that a certain property holds for every and that stands for a particular object in our structure, then we should be able to claim . Again, we are claiming that the formula is valid, that is, we must be able to give a "proof" of this fact, or more properly speaking, a metaproof. These examples are metatheorems of our theory of mathematical logic since we are dealing with the very concept of proof itself. Aside