4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Godel's statement is actually much stronger, it is the claim that there is a statement $A$ such that $\models A$ but not $\vdash A$. That's what makes it so frustrating, it creates a clear formal example of a distinguishable case of "true" and "provable". $\endgroup$ – DanielV Oct 14 '18 at 0:26
  • 2
    $\begingroup$ @DanielV That notation is highly misleading, since there it uses "$\models$" with respect to a fixed structure and "$\vdash$" with respect to a theory, and this makes it look like it contradicts the completeness theorem. It should instead read something like "For any (reasonable) theory $T$ there is some $A$ such that $\mathbb{N}\models A$ but $T\not\vdash A$." $\endgroup$ – Noah Schweber Oct 14 '18 at 0:33
  • 1
    $\begingroup$ See the post How is the Gödel's Completeness Theorem not a tautology ? for the link between the "obvious" completeness of the calculus (e.g. of predicate logic) and the unexpected incompleteness of first-order arithmetic. $\endgroup$ – Mauro ALLEGRANZA Oct 14 '18 at 9:36
6
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ "The surprising bit is that every theory is incomplete .." - is a very compelling argument, thank you. $\endgroup$ – Daniels Krimans Oct 13 '18 at 23:41
  • $\begingroup$ Yes, I keep hypotheses in mind, thank you. $\endgroup$ – Daniels Krimans Oct 13 '18 at 23:42
  • 1
    $\begingroup$ @DanielsKrimans Cool, sorry - I just felt really guilty for writing that particular phrase. As soon as I posted my answer I realized that if someone stopped there they'd get exactly the wrong idea. I've deleted my previous comment. $\endgroup$ – Noah Schweber Oct 13 '18 at 23:44

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.