An axiom schema is a template for generating formulas in a formal system. It’s an expression that follows the grammatical rules of the formal language but contains metavariables (typically represented by Greek letters). For example, consider the following axiom schema where φ and ψ are metavariables:

An instance of an axiom schema is the formula obtained by consistently substituting metavariables with a specific formula. For example, the following are all instances of the schema above:

An axiom schema is valid if and only if every instance of the schema is valid. For example, the schema above is valid, but the schema is not valid.

Both valid and non-valid schemas are useful. Valid schema are used as components of deductive proof systems serving as axioms. And non-schemas can be used as part of a inference rule, where the conclusion is not necessarily true for all substitutions but follows from the premises under specific conditions.