 The same goes for free variable occurrences—semantically, variables are essentially names, so free variable occurrences in logical truths should also be seen as implicitly universally quantified. Hence, properly expressed, the axioms of a logical system, a system designed to have all and only logical truths as its theorems, should be purely general and, hence, should be purged of individual constants and free variable occurrences. In particular, universal instantiation, properly expressed, will replace the instantiated term \(\tau\) in the consequent of  Q2  with a universally quantified variable: