[Duplicate? This question is not simply asking for a proof, it deals with the logical structure of the proof, and particularly, with the use of sustitutions in relation with quantifiers.]
Although Burton's Introduction To Abstract Mathematical Systems is the most reader-friendly elementary book on abstract algebra, the proof it gives of the above theorem is to me difficult to understand, more precisely, in it's second part, dealing with the reverse implication:
If $a,b\in H$ implies $ab^{-1}\in H$ then $(H, *)$ is a subgroup of $G$.
Could anyone give a proof with an endeavour at making as clear as possible the logical structure of the argument? A proof using the natural deduction method would be much appreciated.
More precisely, what makes standard proofs of this theorem difficult is the use of substitutions that seem arbitrary and ad hoc: the underlying mechanism is not made explicit in terms of quantifiers and instantiation.
The theorem reads as follows:
Suppose that $(G,*)$ is a group and $H$ is a non-empty subset of $G$.
Then $(H, *)$ is a subgroup of $G$ if and only if $a,b\in H$ implies $ab^{-1}\in H$.
One direction is clear and I'll leave it to you to flesh out the details. As for the other direction . . .
Associativity of the operation in $H$ is inherited from that of $G$. (Showing this rigourously is a matter of restricting the domain of a predicate. Can you see why?)
Since $H$ is nonempty, there exists an $x\in H$ (by existential instantiation). Thus to prove that the identity is in $H$, we have $xx^{-1}=e\in H$ (by letting $a=b=x$ via universal instantiation).
Since now $e\in H$, we have for any $x\in H$ that $ex^{-1}=x^{-1}\in H$ (by letting $a=e, b=x$ via universal instantiation). Hence $H$ is closed under taking inverses.
For closure of $H$ under the operation, if $x,y\in H$, let $a=x, b=y^{-1}$ via universal instantiation. Then $x(y^{-1})^{-1}=xy\in H$.
Hence $H$ is a subgroup of $G$.