I'm reading "Introduction to mathematical logic" from Mendelson. I'm in chapter 2 "First-order logic and Model theory".I am interested in learning the axiomatic method without using the deduction theorem, but I'm having a hard time understanding how the axioms of first order logic are instantiated correctly. In this case I have some quiestions about Axiom 5: $(∀x_i )(B ⇒ C) ⇒ (B ⇒ (∀x_i )C)$ restriction: if $B$ contains no free occurrences of $x_i$ .
First instantiation: $(∀x)((∀x)B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$
Second instantiation: $(∀x)(∀y)((∀y)B ⇒ C) ⇒ ((∀y)B ⇒ (∀x)C)$
This is my thought process:
In the first instantiation I replace $B$ with $(∀x)B$, I think it is a correct instantiation because all occurrences of $x$ in $B$ are not free but the antecedent $(∀x)((∀x)B ⇒ C)$ worries me because I don't know if I'm allowed to do that.
In the second instantiation I replace $B$ with $(∀y)B$. I think it is a wrong instantiation because $B$ can be a formula like $Px ⇒ Qy$ so this way $Px$ is free in $B$ (since the quantifier is ∀y) and this violates the restriction of the axiom.
So my question is : Are my instantiations and thought process correct?
Also: Can you give more examples of correct instantiations of Axiom 5?