 In general, we use \(A, B, C\) as metavariables for well-formed formulas and \(x, y, z\) as metavariables for individual variables. Anticipating applications (for example to intuitionistic arithmetic) we use \(s, t\) as metavariables for terms; in the case of pure predicate logic, terms are simply individual variables. An occurrence of a variable \(x\) in a formula \(A\) is bound if it is within the scope of a quantifier \(\forall x\) or \(\exists x,\) otherwise free. Intuitionistically as classically, \((A \leftrightarrow B)\) abbreviates \(((A \rightarrow B) \oldand (B \rightarrow A)),\) and parentheses will be omitted when this causes no confusion.