Proof of completeness, what is the point of this lemma?

The sources is this notes http://www.maths.manchester.ac.uk/~jeff/lecture-notes/MATH33001.pdf

The thing is I'm confused about the proof of MON.

We know that if $\Gamma | \theta$, then $\Gamma \cup \Delta | \theta$

So to prove it you need to say let $\Gamma \vdash \theta$

So exists a proof $\Gamma_1 | \theta_1, \Gamma_2 | \theta_2 ,...,\Gamma_k | \theta_k$ where $\Gamma_i \subset \Gamma$ and $\theta_k=\theta$

Hence

$\Gamma_1 | \theta_1, \Gamma_2 | \theta_2 ,...,\Gamma_k | \theta_k, \Gamma_k \cup \Delta_1 | \theta$

But, does $\Delta_1$ have to be finite. Also, what the point of this anyway? Having a discussion that says the point is extending it to infinity. However, I think just think you can give a proof in the form of finite subset.

-
@SamuelReid But, the condition to be a proof is that it follows from finite subset. However, for MON you can add infinite stuff. I'm just worried does this proof MON. I suppose it's really pedantic through. It's hard to see what the lemma is doing. Like don't really understand it so more wanted clarification on what the hell is happening. – simplicity Jan 13 '12 at 19:28

This looks like a pretty painful proof of what Enderton in his first edition calls Rule T, which he proves in two lines. My understanding of it is that this is the theorem that shows that it's mathematically sound to use lemmas rather than building huge monolithic proofs all the time. This is analogous to using subprocedures in programming rather than writing huge monolithic programs all the time.

As for MON, it looks from the lecture notes that it's treated as a logical axiom, and therefore doesn't need proof.

Monotonicity is an understated part of first-order logic. And yes, it holds even when $\Delta$ is infinite. So if a set of axioms proves something, you can add as many more axioms as you want, even infinitely many, and you'll still be able to prove the same thing. Stated another way, adding axioms doesn't disturb provability in classical first-order logic.

Monotonicity breaks down in non-monotonic logics, though.

-