Inference rule
In mathematical logic, an inference rule is a fundamental logical rule for carrying out deductions from a pair of premises to a conclusion. Inference rules are self-evident and require no proof.In propositional calculus, the most basic and necessary inference rule is Modus ponens. Modus Ponens by itself is sufficient for carrying out inferences in propositional calculus. A set of axioms is also needed but no other inference rule is needed. However, any theorem which is tautologically true could be turned into an inference rule if it is simple enough, though it is not necessary. An example is Modus tollens. An inference rule operates on the axioms just as it operates on contingent hypotheses or on proven theorems: the rule does not distinguish between axioms, hypotheses, and theorems, but operates on them in the same fashion in order to obtain a conclusion. So inference rules are stronger than axioms, because axioms, though they may be solid and true, are nevertheless passive, whereas the inference rule is the action which joins statements together in order to create new statements.
Here is an analogy: axioms are like laws passed by a legislature. But these laws have no effect unless they are enforced by an executive power. In a logical theory the inference rule is the executive power, but it executes on axioms or statements based on axioms. Inference rules are stated in this form: (1) some (usually two) premises, (2) a turnstile symbol which means "infers", "proves" or "concludes", (3) a conclusion. The turnstile symbolizes the executive power. The implication symbol has no such power: it only indicates potential inference. is another logical operator, it operates on truth values. is not a logical operator. It is rather a catalyst which metabolizes true statements to create new statements.
In predicate calculus, an additional inference rule is needed. It is called Generalization. It is actually a rule of induction, rather than of deduction.