If $\Gamma \vdash \phi$, is $\Gamma$ always finite in Classical and Intuitionistic Logic? I've been studying the Compactness Theorem in van Dalen's Logic and Structure. In the book, its proof seems to assume that every derivation has a finite number of premises. But this is not explicitly said in the text, as far as I know.
Here is van Dalen's proof (p.111):

$⇒$: Suppose $Γ$ has no model, then by the Model Existence Lemma $Γ$ is inconsistent, i.e. $Γ \vdash ⊥$. Therefore there are $σ_1,...,σ_n ∈ Γ$ such that $σ_1,...,σ_n \vdash ⊥$. This shows that $∆ = {σ_1,...,σ_n}$ has no model. 

My problem is how to justify the bold passage.
Is it true then that if $\Gamma \vdash \phi$, $\Gamma$ is always finite in Classical (and Intuitionistic Logic)?
 A: Hopefully not, otherwise set theory would be no fun at all!  When we prove a theorem $\phi$ of ordinary mathematics, we end up showing that $\mathsf{ZFC} \vdash \phi$, and the axioms $\mathsf{ZFC}$ are most definitely an infinite set of sentences.
Writing $\Gamma \vdash \phi$ means that there is a proof of $\phi$, in which we are allowed to use as premises any of the sentences from the set $\Gamma$, as well as any axioms of logic.  Nobody says we have to use all the sentences from $\Gamma$.  Indeed, if $\Gamma$ is infinite, we can't: our proof can only have finitely many lines, so we can't even mention all the sentences from $\Gamma$, much less use them in an essential way.  So in fact, if we get a proof of $\phi$, we can look back and see which sentences from $\Gamma$ we used.  We can only have used finitely many, and all the others were not actually needed.  With enough foresight, we could have started with a smaller set $\Gamma_0$ that only contained the finitely many sentences we were actually going to use.
And that is essentially the proof of the compactness theorem: if $\Gamma \vdash \phi$, there is a finite $\Gamma_0 \subset \Gamma$ such that $\Gamma_0 \vdash \phi$ as well.
A: No, we are often interested in infinite $\Gamma$. But because a proof is a finite sequence of sentences, it can only invoke finitely many axioms; so if $\Gamma\vdash \varphi$ then some finite subset of $\Gamma$ suffices to prove $\varphi$. Van Dalen is taking this for granted (it's a straightforward exercise) in the bolded sentence.
This is true of classical and intuitionistic logic, and in general of any logic where a proof is a finite object.
