Take the 2-minute tour ×
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.

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|improve this question
add comment

1 Answer

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/

share|improve this answer
add comment

Your Answer

 
discard

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