0
$\begingroup$

In Sets, Logic and Computation the following is said of the Completeness Theorem:

When completeness is thought of as “whenever $\models A$ then $\vdash A$,” it may be hard to even come up with an idea: for to show that $\vdash A$ we have to find a derivation, and it does not look like the hypothesis that $\models A$ helps us for this in any way. For some proof systems it is possible to directly construct a derivation, but we will take a slightly different approach.

I'm interested, first of all, what these systems are in which it is possible to construct such a proof. Secondly, though, I'm curious if this is translatable to natural deduction. In particular, I'm curious if there are any texts which prove this statement constructively, preferably in Fitch notation.

$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

First, it is easy to show that natural deduction systems prove exactly the same sentences as Hilbert systems. This is a purely syntactic fact and can be proved constructively. It is therefore straightforward to conclude the completeness theorem applies to one of these deductive system if and only if it applies to the other. Most of the standard proofs of the completeness theorem should be easily translated to natural deduction systems; I’m hard-pressed to think of one that wouldn’t.

Second, the completeness theorem cannot be proved constructively. In fact, it cannot even be proved in ZF; over ZF, it is equivalent to the ultrafilter lemma (and a great many other things besides), which is independent of ZF.

$\endgroup$
5
  • 1
    $\begingroup$ Exactly so. +1. Do you know what Stilwell meant by "for some proof systems it is possible to directly construct a derivation"? $\endgroup$
    – Rob Arthan
    Jun 5 at 19:07
  • $\begingroup$ @RobArthan That's what I'm wondering now, too. Doesn't make any sense that he would mention that if it can not be proved constructively. $\endgroup$
    – zaq
    Jun 5 at 22:28
  • 1
    $\begingroup$ @RobArthan I believe that he might be referring to countable languages. For countable languages, you can prove the theorem over ZF (though I believe still not constructively). Perhaps he’s referring to some other specific languages $\endgroup$
    – Mark Saving
    Jun 6 at 14:11
  • 2
    $\begingroup$ Wikipedia says that for countable languages, the completeness theorem is equivalent to the weak Kőnig lemma. This is indeed false in e.g. the effective topos (for constructive=type 1 computable). But, it doesn't seem unreasonable to expect that the premises could be further limited to actually make the theorem constructive, but still encompass most 'on paper' sorts of theories (say). Perhaps that's only because I don't know the details of the correspondence, though. $\endgroup$
    – Dan Doel
    Jun 6 at 14:56
  • 1
    $\begingroup$ I don't know where I got "Stilwell" from. I believe the Open Logic publication that zaq refers to was actually written by Richard Zach. I have contacted him to ask if he can enlighten us. $\endgroup$
    – Rob Arthan
    Jun 7 at 21:10
2
$\begingroup$

What I had in mind was simply that some proof systems lend themselves to systematic proof search which, if $\models A$, is guaranteed to be successful. E.g., in sequent calculus LK, you basically apply the rules in reverse, and if you do it systematically (in particular, apply the strong quantifier rules often enough), you eventually find a derivation. This is the basis of the direct completeness proof for LK, I believe first due to Schütte. Completeness is proved this way in Takeuti's proof theory book; I'm sure there are more readily available references but none come to mind off the top of my head. As @Mark Savig mentioned, any such derivation in the sequent calculus LK can be translated into one in natural deduction or Hilbert-style systems. You can do systematic proof search in natural deduction directly as well, but Fitch-style is not the best notation to do that in. But essentially the "proof construction strategies" in intro textbooks that use Fitch-style proofs are such proof search methods.

(Asides: 1. Putting this as "it is possible to construct a derivation" is perhaps misleading as this question shows; I'll clarify this in the text. 2. The Henkin-style completeness proof essentially also includes such a proof search procedure, but the proof obscures this. Basically, if your set is inconsistent, the Lindenbaum construction will fail to produce a maximally consistent set, and the derivation of an explicit contradiction from some stage $\Gamma_i$ will give you a derivation of a contradiction from the starting set $\Gamma$. But that is very roundabout. 3. Proof search is possible for every proof systems where the derivations are computably enumerable, and is guaranteed to terminate if the system is complete. But that it is complete can't be shown this way except if you can construct a countermodel from an infinite failed proof search, like in Schütte's proof. And this requires some non-constructive principle such as WKL.)

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .