Universal Generalization properties

Question

So I am looking for a proof (it is probably simple) to :

$ \vdash (\forall x)A \rightarrow A$

Any help would be appreciate !!

Answer 1

Most systems of first-order logic have a universal quantifier instantiation rule of the form:

from $\forall xA$ infer $A[x/t]$,

where $A[x/t]$ is the result of substituting the term $t$ for all free occurrences of $x$ in $A$. Now take the particular case where the term we substitute for $x$ is ... $x$! Then, since $A[x/x]$ is trivially $A$, we have as a special case

from $\forall xA$ infer $A$.

Now use the deduction theorem or conditional proof to get as a theorem

$\forall xA \to A$.

Fine print: in some syntaxes, where free variables (parameters) are typographically distinguished from bound variables, and where empty quantifiers which bind no variable are not allowed, then you won't get theorems of exactly this form (where '$A$' is exactly replaced by the same wff both times).