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?
$\endgroup$ 51 Answer
$\begingroup$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 :
$\endgroup$ 1$\forall x A \to A^x_t$.
