# Is metatheory, providing proof of the incompleteness theorem, consistent?

Is metatheory, considered as a formal system, that used to prove the First Incompleteness Theorem, consistent?

-
Which metatheory? –  Zhen Lin Jan 17 '13 at 9:22
one consistent suffice –  Max Jan 17 '13 at 9:37
How do you expect anyone to prove absolute consistency of a metatheory without relying on an even stronger metametatheory? You seem to be asking for something impossible. –  S. Carnahan Jan 17 '13 at 12:45
consistency is a subject matter of Incompleteness theorem –  Max Jan 17 '13 at 13:46

Peano Arithmetic suffices to prove Godel's Theorem, and Peano Arithmetic is consistent, so yes.

If you don't believe Peano Arithmetic is consistent, then the question becomes: What do you believe is consistent? As you can see in the accepted answer to this question, you can prove Godel's Theorem in Primitive Recursive Arithmetic, or even a bit less. If you doubt that PRA is consistent, you'll be forced to doubt so much that any skepticism you might have about Godel's Theorem is probably among the least of your worries.

-
I think that PA or PRA do not suffices And I do not sure that they are consistent –  Max Jan 17 '13 at 11:33
That both these theories prove the incompleteness theorem is a standard fact. I’m afraid you should learn at least something about the subject before asking question. –  Emil Jeřábek Jan 17 '13 at 12:46
my objections: every sentence or statement form defines class of his own proofs(statement form for every individual for wich he provable) and even classes of proofs between proofs an so on... after Godelization we obtain function that defines the Godel number of sentence(statement form) for sets/classes of Godel numbers of proofs and so on... quantification over sets higher order stuff Thus we have higher-order metatheory obtained from first-order arithmetics after Godelization of sintax –  Max Jan 17 '13 at 13:30
The only objects manipulated in the proof of the incompleteness theorem are various finite strings, like formulas and proofs, which are easily encoded as numbers. There is nothing stopping you from thinking about sets of proofs and suchlike, but nothing of this sort is needed to prove Gödel’s theorem. –  Emil Jeřábek Jan 17 '13 at 15:35
Gödelization is a representation of finite objects by numbers, it does not involve any infinite sets (which is what higher-order arithmetic is for). If you are worried that the statement of Gödel’s incompleteness theorem involves these finite objects rather than numbers, and therefore strictly speaking cannot be literally expressed in first-order arithmetic, you can take a reformulation of any of the theories mentioned employing finite sets instead of numbers as its basic objects. This is only a notational variant of the original theory, so it does not change its consistency strength. –  Emil Jeřábek Jan 17 '13 at 16:41
As already pointed out by Steven Landsburg, there are plenty of such theories if you stick to conventional mathematics. If you are some sort of an ultrafinitist, the incompleteness theorem is provable in weak fragments of bounded arithmetic, such as $PV$ or $S^1_2$. These theories are interpretable in Robinson’s arithmetic $Q$, so as long as you accept that $Q$ is consistent, there is such a theory. Do you believe that for every natural numbers $n,m$, the number $\underbrace{2^{2^{\cdot^{\cdot^{\cdot^{2^m}}}}}}_n$ exists? Then $Q$ is consistent.
We may live on volcanos waiting for counterexample to the consistency of ZFC, but the situation here is quite different, as the theory in question is much weaker. What is true is that you cannot get something out of nothing. Max, can you tell us what is true in the metametatheory where you want the consistency of the metatheory to be shown? As I wrote, the consistency of, say, $S^1_2$, can be shown in an elementary metametatheory whose most strongest assumption is the totality of the iterated exponential. Are you stipulating that that is false? Then good luck. –  Emil Jeřábek Jan 17 '13 at 15:12