What is the role of the proof system in a Henkin-proof of Completeness?

Completeness is a property of proof systems. Roughly, we say that a proof system is complete iff truth implies derivability. Yet, the proofs for FOL we usually find in logic textbooks, i.e. "Henkin-proofs", do not seem to make any reference to any deductive system at all.

Consider the following proof sketch:

Lemma 1 (Model Existence). $\Gamma$ is consistent $\Rightarrow \Gamma$ is satisfiable

Proof. Let $\mathcal{L}$ be our referring language. An usual proof goes more or less along the lines of

1. Let $\Gamma$ be consistent.
2. Extend $\Gamma$ to a maximal consistent set $\Delta$
3. Show that $\Delta$ preserves consistency and that $\Gamma \subseteq \Delta$
4. Define a valuation $v$ for $\Delta$ such that $v(\psi)=1$ iff $\psi \in \Delta$ for all atomic $\psi \in \mathcal{L}$
5. Define $v$'s unique extension $\bar v$ as usual.
6. Then $\bar v \vDash \Delta$ and, since $\Gamma \subseteq \Delta$,
7. $\bar v \vDash \Gamma$. $\qquad \qquad \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \Box$

Theorem (Completeness) $\Gamma \vDash \varphi \Rightarrow \Gamma \vdash \varphi$

Proof. By contraposition. Let $\Gamma \nvdash \varphi$. Then $\Gamma \cup \{\neg \varphi\}$ is consistent and, by the Model Existence Lemma, it has a model. Hence, $\Gamma \nvDash \varphi$. $\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \Box$

Note that I did not make any explicit mention to any intended deductive system at all. In fact, it seems to me the only syntactic notion I need is:

Definition (Consistency) A set of sentences $\Gamma$ is consistent if there is $\varphi$ such that $\Gamma \nvdash \varphi$.

But yet, I can define this notion generally, for any deductive system.

Now I seemed to have proven completeness. But completeness of which deductive system? I don't know. For the above proof of completeness, I didn't make explicit any axiom or inference rule. This doesn't seem strange?

If this is so, it seems to me I could apply the same argument mutatis mutandis for any other deductive system (even those for that are not complete?).

Question. What is the role of the proof system in a Henkin-proof of Completeness?

I am probably missing something. So can someone explain this topic in details?

Solution 1:

Step 6 in your proof of model existence is not as obvious as it sounds!

For instance, imagine a deductive system which cannot conclude "$\varphi$" from "$\varphi\wedge \psi$". Then take $\Gamma=\{\varphi\wedge\psi, \neg\varphi\}$. $\Gamma$ is consistent for this proof system, but if we extend $\Gamma$ to a maximally consistent(-for-this-system) $\Delta$, the valuation $\nu$ you describe will not make $\Gamma$ true! So that's where the specifics of the proof system are hiding.