Soundness: $a \vdash b \implies a \vDash b$, i.e. if we can prove something, it will also be true. We don't want a system where we start out with something true and dedice something false. However it is conceivable that even if our system is sound, maybe it's quite incomplete/limited regarding what we can express, which is why we also would like...

Completeness: $a \vDash b \implies a \vdash b$, i.e. if we can show something is true, it's also provable. We want to be able to prove all true statements. However it is conceivable that even though we can prove all true statements, maybe it also proves false ones as well, which is why we'd also like the soundness property from before.

Do I have the right idea?

If so, how would I begin to prove soundness? If we are already given $a \vdash b$ I'm not sure what all we must iterate over in e.g. propositional logic to show that we always get true statements. Especially since it seems possible I could pick a false $b$ that contradicts.

  • $\begingroup$ Your question is a little unclear, but the standard pattern for a soundness proof is by induction on the structure of a proof: you show that the axioms are valid and you show that if the antecedents of an inference are valid then the succedent is valid. $\endgroup$ – Rob Arthan Sep 9 '18 at 15:43
  • $\begingroup$ But doesn't induction require logic to state itself in the first place? $\endgroup$ – user525966 Sep 9 '18 at 15:44
  • 1
    $\begingroup$ @user525966 We're studying logic from within mathematics, here; note for example that we're taking the existence of structures for granted, so a bit of set theory is already implicit. There are two ways of thinking about mathematical logic: as a "grounding" for all of math, or as an object of mathematical study (and a tool for mathematical study) in its own right. We're doing the latter here. In fact, I'd argue we can never really do the former; any reasoning has to take some reasoning for granted. $\endgroup$ – Noah Schweber Sep 9 '18 at 15:53
  • $\begingroup$ See the post Method of Proving Soundness of Propositional Logic that answer to you questions. $\endgroup$ – Mauro ALLEGRANZA Sep 9 '18 at 16:50

You have the right understanding of what soundness and completeness are. As to how to prove soundness, the right tool is induction - specifically, by induction on proof complexity, you show that there is no witness to "$a\vdash b$" unless in fact $a\models b$.

Exactly what this looks like will depend on the specific proof system you use. In the case of sequent calculus, it amounts to showing that the "basic sequent rules" are soundness-preserving: each rule only deduces sound sequents from sound sequents. Since every proof is well-founded, this means that no unsound sequent can every "creep in."

For example, consider the rule which takes in the sequents $\Gamma\vdash\varphi$ and $\Gamma\vdash\psi$ and outputs the sequent $\Gamma\vdash\varphi\wedge\psi$. Supposing that our "input sequents" are sound, in any model $\mathcal{M}$ of $\Gamma$, $\varphi$ is true (by the first sequent's soundness) and $\psi$ is true (by the second sequent's soundness). But then by the definition of satisfaction, $\varphi\wedge\psi$ is true in $\mathcal{M}$.

That is, from the assumption that $\Gamma\vdash\varphi$ and $\Gamma\vdash\psi$ are each sound, we've concluded "every model of $\Gamma$ satisfies $\varphi\wedge\psi$;" but this latter statement is exactly the soundness of the sequent $\Gamma\vdash\varphi\wedge\psi$!

  • $\begingroup$ Can you show an example in classical propositional logic for Hilbert, and ND so I can try the rest out myself once I see the general idea? $\endgroup$ – user525966 Sep 9 '18 at 16:02
  • $\begingroup$ @user525966 I'm not sure what you mean. Everything I've done above is in classical propositional logic. $\endgroup$ – Noah Schweber Sep 9 '18 at 16:02
  • $\begingroup$ I assume sequent is different from Hilbert and ND? $\endgroup$ – user525966 Sep 9 '18 at 16:03
  • $\begingroup$ They're all classical propositional logic, they're just different proof systems for it. And they'll all follow the same basic pattern; e.g. the example I gave above is just $\wedge F$ in natural deduction. $\endgroup$ – Noah Schweber Sep 9 '18 at 16:05
  • $\begingroup$ So we basically need to show (true variable) (operator) (true variable) = true, for all operators we've defined? $\endgroup$ – user525966 Sep 9 '18 at 16:08

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.