Do we have to use free variables in Hilbert systems?

103 Views Asked by At

I find it very unpleasant using free variables in proofs, because it puts lines in proofs which have no intuitive meaning. This is clearly necessary for natural deduction, but I was wondering if it was necessary for the (standard) Hilbert system. Clearly, we could just modify any system so that all inference rules work inside quantifiers, i.e. if we have quantifier $Q$ and inference rule $A,B,C...\vdash Z$, then we add $Qx A,Qx B,Qx C...\vdash Qx Z$, but I was wondering if this was necessary. We just need to do this with the universal quantifier, and we can do this with modus ponens: if we start off with a universally quantified formula $A$ and the universally quantified formula $A\rightarrow B$, we can distribute the quantifiers over the second to obtain $B$ with a universal quantifier. But can we do this for modus ponens with multiple quantifiers, and can we obtain the axioms of the Hilbert system with arbitrarily many multiple quantifiers within the Hilbert system, while avoiding using free variables? I'm sure the answer is no, but it would be nice to have it confirmed.