1
$\begingroup$

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.

1 Answers 1

1

Note that $x$ cannot occur free in any of the $T_{i}$ in order to apply the Generalization Theorem (namely: $\forall$ Introduction).

A quick look at my old copy of [1] revealed the following:

  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.)
  2. He then proves Soundness entirely separately from the Generalization Theorem with a similar inductive argument with a lemma added to assure the validity of the logical axioms which surprisingly occupies the bulk of the proof.

[1] http://www.math.ucla.edu/~hbe/amil/