# Soundness for $\forall$Introduction

I have some troubles proving soundness for $\forall$ Introduction. Let $T_1,...,T_n\vdash Q$. $\forall$ Intro gives that $T_1,...,T_n\vdash \forall x Q[x/t]$. Here, t is a constant symbol that does not occur in ${T_1,...,T_n}$, x is a variable which does not occur in Q.

I understand it intuitively, but have some problems with tarskis' truth definitions. Thank you for your answer.

-

Note that $x$ cannot occur free in any of the $T_{i}$ in order to apply the Generalization Theorem (namely: $\forall$ Introduction).
1. Enderton proves the Generalization Theorem purely syntactically by induction on the logical axioms, formulas in which $x$ does not occur, and formulas derivable by modus ponens. (In Enderton's system, modus ponens is the only actual rule of inference; all the rest is lumped into lots of logical axioms.)