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?
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
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.
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.
So a complete theory decides every sentence of its language.
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):