Metamathematics and Godel's Theorems

semioticghost

From what I've read, Godel's Theorems are able to make definite statements about mathematics because they are in fact metamathematical proofs, and thus not self-referentially subject to the incompleteness of mathematics or any rigorously logical system that they demonstrate.

What exactly frees metamathematics of the same logical pitfalls as normal mathematics, though? In attempting to answer foundation problems, it still relies on the axioms present in proof and model theory to get anywhere, and thus is still particularly subject to the second incompleteness theorem, yes? Or have I misread things somewhere/ is my interpretation or impression of Godel's work misguided?

I'd appreciate any clarification. Thanks in advance.

Hurkyl

Gödel's theorems are perfectly rigorous proofs in formal logic. e.g. the first incompleteness theorem proves that a certain class of theories must be incomplete.

The metamathematical part is the supposition that mathematics is a model of the sorts of things studied in formal logic.

Or, you could (metamathematically) assert that the hypotheses of Gödel's theorems are true about mathematics, and then the rest of the proof would be a rigorous metamathematical proof. (I think)


Incidentally, I do not know of a theorem that says a formal system is incapable of proving itself incomplete, so I'm not sure upon what your first paragraph was based. In fact, I'm pretty sure ZF is quite capable of proving itself incomplete.

semioticghost

Well, if mathematics is incomplete, then how can a MATHEMATICAL proof of incompleteness be considered definitive? Thus was, I thought, the rationale for making the proof metamathematical.

Hurkyl

Saying that a theory is incomplete simply means that there exists a statement P such that:
(1) P cannot be proven by the theory.
(2) The negation of P cannot be proven by the theory.


The reason to make it metamathematical is so that it can speak about mathematics, as opposed to the things that are studied by formal logic.

semioticghost

Why isn't metamathematics studied by formal logic, then? What makes it fundamentally different from formal logic? I guess that's my question.

Hurkyl

IMHO, metamathematics is nothing more than the hypothesis that you can use formal logic to talk about mathematics.

I don't know if the philosophers would agree with me.

MathematicalPhysicist

according to wikipedia, metmathematics is based on 4 theories:
recursion theory, mathematical logic, set theory and proof theory.
so i think if this definition is acceptable by the philosopher, then they will not object to your assertion, hurkyl.

semioticghost

But doesn't Godel's work demonstrate that formal logic is incomplete? You can't use formal logic to prove that formal logic is incomplete, because your proof will be vulnerable to the incompleteness.

From what I understand, Godel's metamathematical Incompleteness Theorems establish that mathematics and all other rigorously logical systems powerful enough to be of interest are intrinsically incomplete. But is not metamathematics just such a system, and thus is it not also incomplete--subject to its own conclusions and thus not definitive? Or is there a crucial distinction to be made between metamathematics and the types of systems that Godel's Incompleteness Theorems render incomplete? If so, what is that difference?

Or am I being to big picture here, and do the focus of Godel's theorems have a scope narrow enough to avoid this issue, and if so, how do they do it?

Hurkyl

Actually, Gödel's incompleteness theorems do not apply to several rigorously logical systems of interest.

For example, the theory of real closed fields is very interesting -- but it's not powerful enough to define the word "integer".

On the other hand, the theories constructed for the purposes of nonstandard analysis are powerful enough to talk about the integers... but they are far too `powerful' for Gödel's theorems to apply.


I still think that you are misinterpreting the word "incomplete".


A theory is incomplete if and only if there exists a statement P that can neither be proven nor disproven.

That's it. That's all it says. The only inadequacy the word "incomplete" implies is the fact the theory cannot answer every question asked of it.

In particular, "incompleteness" says absolutely nothing about the quality of the proofs and theorems that the theory is capable of providing.

semioticghost

So then a metamathematical proof would be devoid of such statements P that can be neither proven nor disproven, and thus not subject to its own theorems, I assume. But you can't really used the specific breed of metamathematics to write MATHEMATICAL proofs, and the majority of logical axiomatic systems powerful enough to make statements of interest in mathematics DO contain such statements P.

That said, how is Godel's metamathematical proof not such "a formal system P" (the term Godel uses in his proof), with regards to his second Incompleteness Theorem in particular (which I thought concerned self-referentiality)? I'm confused as to how such a system is defined and why Godel's metamathematical statements don't fit the definition.

Hurkyl

Yep -- a (formal) proof consists of a sequence of statements, where each step is either an axiom, or is logically deduced from the previous steps.

Thus, no statement in a proof can be undecidable by the theory!

I'm not really sure what you're asking in the rest of your post, so I'll just try explaining stuff and hope I get lucky. :)

Gödel's second incompleteness theorem (which can be cast as a mathematical theorem in formal logic) relies on a notion similar to that of a model. Using the theory of integer arithmetic, Gödel constructs a way to interpret certain numbers as logical statements (which I'll call number-statements), and if I recall correctly, the theory of integer arithmetic is powerful enough to develop a formal logic of number-statements.

As external "observers", we are able to translate any proof made about these number-statements into honest to goodness proofs. In particular, we can use the theory of integer arithmetic to prove things from the number-statements that correspond to the axioms of the theory of integer arithmetic: such proofs would be translated into honest to goodness proofs about the theory integer arithmetic.

To say it differently, in the theory of integer arithmetic, we can develop a theory of formal logic. As external "observers", we can translate between this theory of formal logic and honest to goodness mathematical proofs.

(Or, if we want to phrase everything mathematically, we have the formal system of integer arithmetic, and in that system, we can construct another formal system of integer arithmetic, and we can map back and forth between the "outer" and "inner" theories)

If the theory of integer arithmetic was capable of proving its model of integer arithmetic was consistent, then Gödel's second theorem would then proclaim that the axioms of integer arithmetic are inconsistent.

semioticghost

Where does the notion of self-referentiality come into play in all of this, then?

matt grime

No.

I don't see why a proof is at all 'vulnerable' to the incompleteness theorem

you do not understand correctly.

It applies to *finitely axiomatized* system *strong enough to define integer arithmetic*.

In particular it does not apply to geometry (see the work of Tarski).

CrankFan

I think you mean recursive here, instead of finite.

For example, consider the first order induction schema (of first order PA).

matt grime

My mistake; my only experience of this stuff is on this website where it occupies far more time than it is worth.

semioticghost

I would hope that you've experienced it somewhere else; it'd be a bit of a shame for you to declare how much time it's "worth" (a dubious assignation in its own right) based solely on your forum experiences.

Anyway (just clarifying here), metamathematics is used to parse mathematics, and thus can view it externally as a discrete system. Meanwhile, metamathematics avoids being incomplete by virtue of the fact that by definition it is never used in an attempt to parse itself, and thus avoids the entire can of worms. Yes?

However (correct me if I'm wrong here), if one wished to parse metamathematics the way that Godel parsed certain mathematical systems, it would prove impossible without the development of a "metametamathematics," and then metametamathematics with metametametamathematics, all the way to meta^infinity-mathematics, into a spiralling series of academic and increasingly esoteric proofs with no color and no end. Assuming that development of a metametamathematics is even possible; is it?