Does weak completeness (“If $\vDash\phi$, then $\vdash\phi$”) imply strong completeness (“If $\Gamma\vDash\phi$, then $\Gamma\vdash\phi$”)?

Suppose we have a proof system for classical first-order logic, where $\vDash$ denotes model-theoretic consequence and $\vdash$ denotes proof-theoretic consequence.

We can distinguish two forms of completeness of the proof system. Call them weak and strong, respectively*:

$$\text{for all sentences \phi, if \vDash\phi, then \vdash\phi}\tag{weak}$$ $$\text{for all sets of sentences \Gamma and sentences \phi, if \Gamma\vDash\phi, then \Gamma\vdash\phi}\tag{strong}$$

Both of these statements are true of classical first-order logic with any of the standard proof systems. It is also obvious that strong completeness implies weak completeness, by taking $\Gamma=\emptyset$.

The weak statement of completeness also comes in two other equivalent forms: (1) every sentence $\phi$ is either satisfiable or refutable, and (2) if $\phi$ is consistent, then $\phi$ is satisfiable. Similarly, the strong statement of completeness is equivalent to (3) if $\Gamma$ is consistent, then $\Gamma$ is satisfiable. (My understanding is that in his 1930 dissertation Gödel proved a statement even stronger than (3), namely (4): if $\Gamma$ is consistent, then $\Gamma$ is satisfiable in a countable domain.)

Does weak completeness imply strong completeness? I get stuck when I try to prove it does.

Here is how I tried to prove that (weak) implies (strong). My thought was to show (weak) implies (3). Suppose $\Gamma$ is consistent. Then for all sentences $\phi$, $\Gamma\nvdash\phi\land\lnot\phi$. What you'd like to do at this point is use the syntactic deduction theorem** to say $\nvdash\Gamma\rightarrow(\phi\land\lnot\phi)$, and then use (weak) to conclude $\nvDash\Gamma\rightarrow(\phi\land\lnot\phi)$. From here it would follow that $\Gamma$ is satisfiable. But of course pushing $\Gamma$ into the antecedent of a conditional doesn't make sense for arbitrary sets of sentences $\Gamma$ (instead of a finite set, which can be pushed into the antecedent as a conjunction).

This suggests some sort of compactness trick would help, and that weak completeness does not imply strong completeness in general. Is this right?

*If there are more standard names for these properties, please tell me.

**Which says $\Gamma\cup\left\{\phi\right\}\vdash\psi$ if and only if $\Gamma\vdash\phi\rightarrow\psi$.

There's a good reason you're having trouble proving this equivalence - it's false! There are some very silly proof systems out there. For example, for any set $\Delta$ of formulas, we can cook up a proof system $\mathfrak{S}$ such that the sequents derivable from $\mathfrak{S}_\Delta$ are exactly those of the form $\Gamma\vdash\varphi$ for $\varphi\in \Delta$ - that is, $\mathfrak{S}_\Delta$ knows that $\Delta$ is true, and knows absolutely nothing else. Such a $\mathfrak{S}$ is never both sound and strongly complete - if "$\exists x(x\not=x)$" isn't in $\Delta$, then the valid sequent "$\{\exists x(x\not=x)\}\vdash\exists x(x\not=x)$" is not $\mathfrak{S}_\Delta$-derivable.
Now, do you see a choice of $\Delta$ which would yield a weakly complete system?
• @symplectomorphic That's not quite correct - even if we work with a compact logic (and indeed I was assuming we were working with first-order logic - note that otherwise Godel's completeness theorem need not be true!), we crucially need the deduction theorem (or rather its converse - I've usually seen DT stated as "If $\Gamma\cup\{\varphi\}\vdash\psi$ then $\Gamma\vdash \varphi\implies \psi$"), which does not hold in arbitrary proof systems. If you assume that this holds of your proof system, though, then you do get strong completeness as you indicate. – Noah Schweber Apr 29 '17 at 23:03