Sequent calculus and first incompletness theorem

Wikipedia says that sequent calculus is sound and complete (http://en.wikipedia.org/wiki/Sequent_calculus#Properties_of_the_system_LK). Godel first incompleteness theorem says that system capable of doing arithmetics may not be complete and consistent. Does it mean that Sequent Calculus is not capable of doing arithmetics or is incomplete or I miss some subtle point of incompleteness theorem?

-

There is an unfortunate clash of terminology when talking about completeness in logic (compounded by the fact that there is a Gödel's completeness theorem as well as a Gödel's incompleteness theorem).

A formal system (like the sequent calculus or the more familiar natural deduction or Hilbert-style proof systems, possibly with proper axioms etc.) is called complete if semantic truth implies syntactic truth. That is, if a statement is true in all models of the system (it is semantically true) then it is in fact provable in the system (it is syntactically valid). This notion of completeness is what is meant in the wiki article on the sequent calculus. It is also the content of Gödel's completeness theorem: any Hilbert or natural deduction style system in first order logic is complete. The converse of this property, that whatever is provable is always true, is known as soundness.

On the other hand, a formal system is (also) called complete if it is consistent and for any sentence $\varphi$ either $\varphi$ or $\lnot\varphi$ is provable in the theory. This notion of completeness is what is discussed in Gödel's incompleteness theorems.

These two meanings of completeness are independent of one another; most systems of interest are complete in the former sense, but they may or may not be complete in the latter sense.

-
That makes things clear. But you said that system is (Godel) complete if it's consistent and for any sentence $\varphi$ or $\lnot\varphi$. On the other hand Godel completeness theorem says about consistency and completeness as two distinct notions. So I suspect that completenes means only that for every sentence $\varphi$ either $\varphi$ or $\lnot\varphi$. – Trismegistos Jan 17 '13 at 11:13
@Trismegistos It is a matter of convention whether you take your complete theories to be consistent or not. An inconsistent theory is trivially complete, so this case isn't really meaningful. Also, I like to think of complete theories as being the maximal consistent sets of sentences. – Miha Habič Jan 17 '13 at 11:17

Miha Habič's answer is exactly right, so this is just by way of amplification and a comment on the double use of "complete".

Putting it symbolically may help.

A theory $T$ with the set of axioms $\Sigma$ is negation-complete iff, for any sentence $\varphi$ of its language, $\Sigma \vdash \varphi$ or $\Sigma \vdash \neg\varphi$.

So a complete theory decides every sentence of its language.

A logical system [like the sequent calculus] is semantically complete iff for any set of wffs $\Sigma$ and any sentence $\varphi$, if $\Sigma \vDash \varphi$ then $\Sigma \vdash \varphi$

where as usual '$\vdash$' signifies the relation of formal deducibility in the logical proof system, and '$\vDash$' signifies the relevant relation of semantic consequence. So a complete deductive logic enables us to give formal derivations of everything that is semantically entailed by given premisses.

These notions of completeness are plainly different. As it happens, the first proof of the semantic completeness of a proof system for quantificational logic was also due to Gödel, and the result is often referred to as Gödel's 'Completeness Theorem'. The topic of that theorem is therefore evidently not to be confused with the topic of Gödel's (First) 'Incompleteness Theorem': the semantic completeness of a proof system for quantificational logic is one thing, the negation incompleteness of certain theories including enough arithmetic quite a different thing.

OK, there is here a potentially dangerous double use of the term 'complete'. But this double use isn't a case of terminological perversity -- even though logicians can be guilty of that! For there's the following parallel worth noting (and which explains why "complete" is the apt term in both cases):

A negation-complete theory is one such that, if you add as a new axiom some proposition that can't already be derived in the theory, then the theory becomes useless by virtue of becoming inconsistent. Likewise a semantically complete deductive system is one such that, if you add a new logical axiom that can't already be derived (or a new rule of inference that can't be established as a derived rule of the system) then the logic becomes useless by virtue of warranting arguments that aren't semantically valid.

-
Thanks putting it down in logical symbols is often very clarifying. – Trismegistos Jan 22 '13 at 21:32