What is the dependency between the equivalence of consistence and satisfiability, and correctness and completeness theorems?

83 Views Asked by At

In Ebbinghaus' Mathematical Logic (2ed), in first order logic:

  • It first proves IV.6.2 the correctness of sequent calculus on p70 (if I am correct, the soundness of sequent calculus);

  • It then proves IV.7.5 a satisfiable set of formulas is also consistent on p73, based on the correctness of sequent calculus;

    Proof. Suppose $\Phi$ is inconsistent. Then for a suitable $\phi$ both $\Phi \vdash \phi$ and $\Phi \vdash \neg \phi$; hence, by the theorem on the correctness of sequent calculus, $\Phi |= \phi$ and $\Phi |= \neg \phi$. But then $\Phi$ cannot be satisfiable.

  • It then proves V.(**) a consistent set of formulas is also satisfiable on p75:

    Proof Sketch: we have to find a model for any consistent set of formulas. In Section 1 we shall see that there is a natural way to do this if the set of formulas is negation complete and if it contains witnesses (Henkin's Theorem). Then we reduce the general case to this one: in Section 2 for at most countable symbol sets, and in Section 3 for arbitrary symbol sets. Unless stated otherwise, we refer to a fixed symbol set S.

  • It finally proves V.(*) the completeness theorem on p75:

    We assume for $\Phi$ and $\phi$ that $\Phi |= \phi$, but not $\Phi \vdash \phi$. Then $\Phi \cup \{\neg \phi\}$ is consistent but not satisfiable (cf. III.4.4 and IV.7.6(a)), a contradiction to (**).

Questions:

  • Does it prove "a consistent set of formulas is also satisfiable" based on both the correntness of sequent calculus and "a satisfiable set of formulas is also consistent"?

  • Does it prove the completeness theorem, based on all the other three?

I am not sure if the proofs in the book are the only ways.

  • Can the equivalence of consistence and satisfiability (i.e. the second and the third) be proved without being based on the equivalence of consequential relation and provability (i.e. the correctness and completeness theorems, i.e. the first and the fourth)?

  • Both consistence implying satisfiability and provability implying consequential relation go from syntax to semantics, while the other two (satisfiability implying consistence and consequential relation implying provability) go from semantics to syntax. Can they be proved without being based on the other two? Similarly, can the other two be proved without being based on them?

Thanks.

1

There are 1 best solutions below

10
On

The "syntax-to-semantics vs. semantics-to-syntax" distinction is the wrong one, since it's really just about phrasing (the contrapositive of a "syntax-to-semantics" result is a "semantics-to-syntax" result). Rather, we should think instead about the positive content of the relevant results: are they designed to yield instances of $\vdash$, or instances of $\models$?

We really have only two theorems here, although they appear in many different guises:

Building instances of $\models$: "If $\Phi\vdash \varphi$ then $\Phi\models\varphi$." This is the soundness theorem. It's easily equivalent to the theorem that satisfiability implies consistency - note in particular that the latter is an instance of the contrapositive of the former (it says $\Phi\not\models\perp\implies\Phi\not\vdash\perp$).

Building instances of $\vdash$: "If $\Phi\models\varphi$ then $\Phi\vdash\varphi$." This is the completeness theorem. As above, it's easily equivalent to the theorem that consistency implies satisfiability, via basically the same argument. Interestingly, the former is generally deduced as a consequence of the latter - it's easier to build structures than proofs, it turns out.

These two (classes of) results are completely independent of each other: consider the silly proof systems $\vdash_{arrogant}$ which lets you deduce anything from anything and $\vdash_{bashful}$ which doesn't let you deduce anything from anything. Trivially, $\vdash_{arrogant}$ is complete and $\vdash_{bashful}$ is sound for indeed any semantics whatsoever.

We can also find less trivial examples of one property holding without the other. If we take a very lax approach to deduction systems and allow them to be non-finitary and non-effective, then for example we have:

  • The semantic entailment relation of Henkin semantics for second-order logic, thought of as a deduction system, is sound but not complete for the full semantics for second-order logic.

  • The semantic entailment relation of full semantics for second-order logic, thought of as a deduction system, is complete but not sound for the Henkin semantics for second-order logic.

Basically, whenever we have one semantics which is strictly "narrower" than another, we'll get this phenomenon. I'll leave the search for better examples (e.g. effective and finitary) as an exercise.


It's worth noting that the soundness theorem is massively easier than the completeness theorem. The former is basically an exercise in induction on complexity, while the latter requires multiple fundamentally new ideas:

  • Maximal consistent sets.

  • Term structures.

  • The witness property.

(Incidentally, the second of these is in my opinion the most significant.)