I’m trying to understand the proof of Lemma 2112 in An Intro
to Mathematical Logic and Type Theory: To Truth Through Proof
by Peter B. Andrews (like what else is there to do on Sunday?).

2112 Lemma. Suppose H |- A and let U be a finite set of individual
variables not free in A or H. Then there is a proof of A from H
such that no member of U is generalized upon or occurs free in any
wff of the proof.

He says it’s sufficient to prove the lemma for the case where H
is finite, but he never uses the idea of a finite H in the proof
so is finiteness a big deal?

Am I right to think that generalizing on a variable x is to say
"for all x"?

–
Henry Choy
c…@cs.usask.ca

I’ll have two all beef patties, special sauce, lettuce, cheese,
pickles, onions, on a sesame seed bun, please.