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?


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.

| cite | improve this answer | |
  • $\begingroup$ This is very similar to the point in my answer to your previous question, math.stackexchange.com/questions/1449041/…. $\endgroup$ – Noah Schweber Oct 4 '15 at 7:09
  • 4
    $\begingroup$ Step 6 is indeed the place where you need that you're using the right deductive system and not something silly, but the deductive system also enters, in a weaker way, at step 2. That step depends on the fact that, if a set of formulas is inconsistent, then so is some finite subset. That is, you need that deductions are finite, because each rule has only finitely many premises. $\endgroup$ – Andreas Blass Oct 4 '15 at 7:30
  • 1
    $\begingroup$ @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$\}$. $\endgroup$ – Noah Schweber Oct 4 '15 at 7:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.