Understanding importance of Godel's incompleteness theorem I have been reading Chapter 42 of Kleene's "Introduction to Metamathematics" where the following result is proven:
(Rosser's form of Godel's theorem) If the number-theoretic formal system is simply consistent then there is a formula $A$ such that neither $\vdash A$ nor $\vdash \lnot A$.
I know that Godel's theorems are famous for their influence in mathematics. I have trouble understanding what is so influential here.
Consider pure propositional calculus. There, the only provable formulas are those which are identically true (under certain evaluation scheme using truth tables). Consider a formula that is not identically true and not identically false (call it $B$). Then, in pure propositional calculus neither $\vdash B$ nor $\vdash \lnot B$. Somehow, we do not think that this result is influential. What is the reasoning here?
I would appreciate your comments  about this. Sorry if such question has already been asked but I couldn't find it.
 A: It is of course unsurprising that there are incomplete theories. The surprising bit is that every formal number theory is incomplete - or rather:

Every theory which (1) is "strong enough" (= contains a very small set of axioms about basic arithmetic), (2) is consistent, and (3) is "reasonably simple" (= recursively axiomatizable: there is an algorithm for telling what is, and what is not, an axiom of the system) is incomplete.

Each hypothesis is necessary. There are plenty of natural, interesting theories which are complete, consistent, and reasonably simple - they don't let us "interpret arithmetic," though. Similarly, and more seriously, this implies that for example the true theory of arithmetic - that is, the set of all true statements about natural numbers that can be expressed using $+,\times$, Boolean operations, quantifiers, variables, and parentheses - is not computable (it's obviously complete and consistent and contains basic arithmetic). This may not seem as surprising now, but it means that there are "simple number-theoretic claims" which we cannot hope to prove in whatever axiom system we're using. Put another way: no matter what axiom system we decide to use to study arithmetic, there will be some very concrete statements which we'll never be able to prove or disprove.
Now, I do think that the incompleteness theorem is much less surprising in the modern light of computers, where we have a better sense of what "basic arithmetic" can actually do in terms of logical complexity; indeed, I think other basic theorems are far more surprising. But there's no question that it's hugely surprising insofar as we adopt the principle "all mathematical problems can be satisfyingly solved" in too naive a fashion (we have to be very flexible about what "satisfyingly solved" means to not get ruined by Godel), and this was something that many mathematicians were guilty of from time to time (to put it mildly).
