# 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?

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.
• @AndreasBlass that's a very good point - I was implicitly assuming that deductive systems are defined as monotonic maps from $\{$finite sets of formulas$\}$ to $\{$formulas$\}$. – Noah Schweber Oct 4 '15 at 7:59