Syntactical proof of universal instantiation rule

Question

First: I am not mathematician but philosopher. I understand why the universal instantiation rule is working.

$\frac{\vdash\forall xA}{\vdash A^x_t}$

But is there actually a serious proof in a logical proof system (Hilbert etc.) ? I don't personally find the critical step on how to get rid of the universal quantifier from one to the next line.

An idea of a syntactical proof:

1: $\vdash\forall A$

2: $\vdash\forall A\to A$

3: $\vdash A$

The first is the assumption, the second is a fact which I found in a book and which seems serious and the third line is modus ponens on the first two. But now, I have got the same result, but without the substitution in A?

Answer 1

The rule of Universal instantiation simply formalizes the evident intuitive principle that "what holds of all, holds of any"

In other words, if property $A$ holds of every object in the "universe" (this means $\forall x A(x)$), then it holds also of the object named by $t$ (i.e. $A(t)$).

In Natural Deduction it is one of the basic rules for quantifiers.

In Hilbert-style proof system we can derive it from the quantifier axiom :

$\forall x A \to A^x_t$.