I tried to prove the soundness of a Hilbert system over in this post and so now I am trying to prove completeness from the other direction:

$$\Gamma \models \varphi \implies \Gamma \vdash \varphi$$

I read this as "If $\varphi$ is true under all interpretations where $\Gamma$ is satisfied, then we can show that $\varphi$ is provable from $\Gamma$"

But then I realized I don't even know where to begin. We are starting from a position where we don't even have a proof written down. This led me to realize that maybe I don't fully understand semantic entailment. In absence of syntax / axioms / inference rules / etc, I don't even know what this really means.

What are some examples of what this even looks like before we move onto showing provability? Is this something we are only able to show strictly in terms of truth tables? (this perhaps the real question I am asking in all this)

For example: If $\Delta = \{p, (p \to q) \}$, can we say $\Delta \models q$? Meaning that when $p$ is true and $p \to q$ is true, then the truth tables suggest that $q$ is true? And then we can show the existence of a proof of $q$ in three lines: $\varphi_1 = p, \varphi_2 = p \to q$ by assumption, and then $\varphi_3 = q$ via modus ponens on $\varphi_1$ and $\varphi_2$?

And then proving completeness is showing that whenever all the statements of $\Delta$ are true and the righthand side is true, we can write a proof for it?

  • 2
    $\begingroup$ The completeness property is relative to a proof system : language + axioms + rules. It means that the proof system is "enough powerful" to match with the logical consequence relation for the semantics specific for that language. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 16:59
  • 2
    $\begingroup$ The completeness proof is by far more difficult than the soundness one; see math log textbooks. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 17:01
  • $\begingroup$ See e.g. the post What is the role of the proof system in a Henkin-proof of Completeness ? $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 17:02
  • 1
    $\begingroup$ Not necessarily $\varphi$ atomic. We have e.g. $\{ p \land q \} \vDash p \lor q$. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 18:50
  • 1
    $\begingroup$ @user525966 Note "$\wedge$" versus "$\vee$." $\endgroup$ – Noah Schweber Sep 25 '18 at 22:10

Your Answer

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

Browse other questions tagged or ask your own question.