What is the difference between Completeness and Soundness in first order logic?

Completeness is defined as if given $\Sigma\models\Phi$ then $\Sigma\vdash\Phi$. Meaning if for every truth placement $Z$ in $\Sigma$ we would get $T$, then $\Phi$ also would get $T$. If the previous does indeed exists, then we can prove $\Phi$ using the rules in $\Sigma$.

Soundness is defined as: when given that $\Sigma\vdash\Phi$ then $\Sigma\models\Phi$ , which is the opposite.

Can you please explain the basic difference between the two of them ?

Thanks ,Ron

-

In brief:

Soundness means that you cannot prove anything that's wrong.

Completeness means that you can prove anything that's right.

In both cases, we are talking about a some fixed system of rules for proof (the one used to define the relation $\vdash$ ).

In more detail: Think of $\Sigma$ as a set of hypotheses, and $\Phi$ as a statement we are trying to prove. When we say $\Sigma \models \Phi$, we are saying that $\Sigma$ logically implies $\Phi$, i.e., in every circumstance in which $\Sigma$ is true, then $\Phi$ is true. Informally, $\Phi$ is "right" given $\Sigma$.

When we say $\Sigma \vdash \Phi$, on the other hand, we must have some set of rules of proof (sometimes called "inference rules") in mind. Usually these rules have the form, "if you start with some particular statements, then you can derive these other statements". If you can derive $\Phi$ starting from $\Sigma$, then we say that $\Sigma \vdash \Phi$, or that $\Phi$ is provable from $\Sigma$.

We are thinking of a proof as something used to convince others, so it's important that the rules for $\vdash$ are mechanical enough so that another person or a computer can check a purported proof (this is different from saying that the other person/computer could create the proof, which we do not require).

Soundness states: $\Sigma \vdash \Phi$ implies $\Sigma \models \Phi$. If you can prove $\Phi$ from $\Sigma$, then $\Phi$ is true given $\Sigma$. Put differently, if $\Phi$ is not true (given $\Sigma$), then you can't prove $\Phi$ from $\Sigma$. Informally: "You can't prove anything that's wrong."

Completeness states: $\Sigma \models \Phi$ imples $\Sigma \vdash \Phi$. If $\Phi$ is true given $\Sigma$, then you can prove $\Phi$ from $\Sigma$. Informally: "You can prove anything that's right."

Ideally, a proof system is both sound and complete.

-
What do you mean by saying "prove anything that's wrong" or " prove anything that's right" ? a TRUE/FALSE value for every Phi ? –  ron Feb 4 '12 at 9:22
Think of $\Sigma$ as a set of hypotheses. If $\Sigma \models \Phi$, then $\Phi$ is "right" in the context of $\Sigma$, because whenever $\Sigma$ is True, so is $\Phi$. Otherwise, $\Phi$ is "wrong" in the context of $\Sigma$. A key difference between $\models$ and $\vdash$ is that $\models$ has nothing to do with your rules for proof; $\vdash$, on the other hand, is very much dependent on your rules for proof. –  Ted Feb 4 '12 at 9:27
@ron See my edits for more details. –  Ted Feb 4 '12 at 9:52
@ron: "Anything that's right" is an informal way of saying "anything that's true under all interpretations, in your case every truth placement, in the case of predicate calculus in all $L$-structures for the appropriate language $L$. –  André Nicolas Feb 4 '12 at 10:00
I don't see why you say we're thinking of a proof as something used to convince others in this context. The notion of proof here has a precise definition which goes something like "a sequence of wffs which has the theorem as the last "element" of the sequence such that each wff is either an axiom, or validly infer-able by the rules of inference given." Such a proof might not get used to convince anyone else of the theorem. –  Doug Spoonwood Feb 4 '12 at 23:23
show 1 more comment

From the perspective of trying to write down axioms for first-order logic that satisfy both completeness and soundness, soundness is the easy direction: all you have to do is make sure that all of your axioms are true and that all of your inference rules preserve truth. Completeness is the hard direction: you need to write down strong enough axioms to capture semantic truth, and it's not obvious from the outset that this is even possible in a non-trivial way.

(A trivial way would be to admit all truths as your axioms, but the problem with this logical system is that you can't recognize what counts as a valid proof.)

-
Okay,so what is the use of a FOL (first order logic) that is Complete but not Sound ? and on the other hand , what is the use of a FOL that is Sound but not Complete ? this is a little unclear to me . thanks –  ron Feb 4 '12 at 9:26
@ron: a FOL that is complete but not sound is not useful for proving true things because it can prove false things. A FOL that is sound but not complete can at least prove true things, it just can't prove all true things. –  Qiaochu Yuan Feb 4 '12 at 9:29
So from my understanding , if we have a FOL that is complete and not sound ,it is useful ,since what we cannot prove , must be wrong .Am I wrong ? thanks –  ron Feb 4 '12 at 10:18
@ron "complete and not sound" usually isn't very useful because even once you have "proved" something you still don't know if it's true. –  Ted Feb 4 '12 at 10:58
@Qiaochu Yuan: Okay,but I'm talking about "what I cannot prove" . Is it correct to say that what I cannot prove (using a FOL that is complete & not sound) , must be wrong ? –  ron Feb 4 '12 at 11:08

I cannot write comments so I post is as an answer. Matt in his answer changes meaning of "complete" while saying that group theory is incomplete. The OP asked about semantical completeness, Matt writes about negation completeness, that is:

A theory $T$ is negation complete iff for every formula $A$ of $T$, either $T\vdash A$ or $T\vdash\neg A$.

As such group theory is indeed not complete (see Matt's example). But it is still semantically complete, that is whatever that is true in every group (in every structure which is a model of group axioms) is provable from the axioms for groups.

-

You can have a theory $T$ that is sound but incomplete. As an example consider group theory where $T$ are the three properties of groups. Then you cannot prove or disprove $\forall x,y: xy = yx$ since not all groups are abelian but some are.

-
This is non-standard usage. First-order logic is sound and complete. We don't usually talk about soundness/completeness of first-order theories. –  Zhen Lin Feb 4 '12 at 11:09
@ZhenLin What's nonstandard in Matt N.'s post specifically? You also, of course, mean classical first-order logic. Merrie Bergmann, in her textbook An Introduction to Many-Valued and Fuzzy Logic does talk about the soundness/completeness of three-valued first-order logics in chapter 7 p. 130-143. So, if you would call her use "nonstandard" also and it comes as similar to Matt N's, then Matt N's use is at least not without precedent. –  Doug Spoonwood Feb 4 '12 at 23:40
This is a pointer to the answer by Steve. The concept of "completeness" for a logic, such as first-order logic, is semantic completeness, and this is the notion defined in the question. It is also common to talk about a theory being complete, which means negation complete, but I believe that is not what the question is asking about. –  Carl Mummert Sep 2 '12 at 23:14