Syntactical proof of universal instantiation rule 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?

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$.