  (Here it is assumed that \(A(x)\) is any well-formed formula of predicate logic, and that \(A(y)\) and \(A(n)\) result from replacing \(y\) and \(n\) properly for each occurrence of \(x\) in \(A(x)\).) Note that the instantiation axiom is restricted by mention of \(En\) in the antecedent. The rule of Universial Generalization is modified in the same way. In \(\mathbf{FL}\), proofs of formulas like \(\exists x\Box(x=t)\), \(\forall y\Box \exists x(x=y)\), \((CBF)\), and \((BF)\), which seem incompatible with the world-relative interpretation, are blocked. 