1
$\begingroup$

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$.

$\endgroup$
2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Thanks! But this example doesn't show that implication from (weak) to (strong) doesn't hold for a better system. I guess the implication is valid in compact logics, where we can reason as I suggested. $\endgroup$ – symplectomorphic Apr 29 '17 at 22:56
  • $\begingroup$ @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. $\endgroup$ – Noah Schweber Apr 29 '17 at 23:03
  • $\begingroup$ Thanks, that's helpful; yes, I was assuming a deduction theorem. $\endgroup$ – symplectomorphic Apr 29 '17 at 23:07
  • $\begingroup$ @symplectomorphic And it is not stupid to examine proof systems where DT fails! See this mathoverflow question, and this paper cited in that question. So even though my example is stupid, it serves a good purpose in pointing out the need to explicitly assume (the converse of) DT. $\endgroup$ – Noah Schweber Apr 29 '17 at 23:07

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.