Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question

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.


share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.