 Classical first-order logic includes quantifiers that are denoted by \(\forall\) (“for all”) and \(\exists\) (“there is a”). A simple sentence such as “All birds are animals” may be formalized as \(\forall x(Bx\supset Ax)\), where \(x\) is a variable, \(B\) and \(A\) are one-place predicates, and \(\supset\) is a symbol for (material) implication. The occurrences of the variables in the closed formula \(\forall x(Bx\supset Ax)\) are bound, whereas those in the open formula \(Bx\supset Ax\) are free. If we assume that \(t\) (for “Tweety”) is a name constant, then an instance of the above sentence is \(Bt\supset At\), that may be read as “Tweety is an animal, provided Tweety is a bird.” This illustrates that the instantiation of a (universal) quantifier involves substitution.