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
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.