24
$\begingroup$

The Goedel incompleteness theorems can be considered meta-mathematical theorems, as they are "written" in a meta-theory and "talk" about properties of a class of formal theories.

The following may be a naive question, but...

Are there any "interesting" results at the next level, i.e. so to speak, that take place in a meta-meta-theory and talk about meta-theories and properties thereof and the theories they describe/codify?

Improve this question
$\endgroup$
4
  • 35
    $\begingroup$ And, if so, do we need a meta.meta.mathoverflow? $\endgroup$
    – Gerry Myerson
    Commented Mar 8, 2014 at 22:05
  • 4
    $\begingroup$ I read somewhere that meta.meta.mathoverflow questions should go to meta.stackoverflow.com, so again we have collapse to the first level. $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Mar 8, 2014 at 22:55
  • 13
    $\begingroup$ @Bjørn: I have an issue with that. Where do I take it? $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 9, 2014 at 19:27
  • 2
    $\begingroup$ @AsafKaragila now you can use meta.stackexchange.com $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Apr 17, 2014 at 21:14

6 Answers 6

Reset to default
33
$\begingroup$

In Reverse Mathematics, we can study what happens if we use weak systems of second-arithmetic as metatheories. For example, we can study the strength of the completeness theorem and prove results such as "Gödel’s completeness theorem is equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$." That can be seen as a meta-meta-theorem: we are investigating which axioms are required in the metatheory for the completeness theorem to hold.

This is not as trivial as it may sound; some results are genuinely unexpected. For example, one interesting fact is that every countable $\omega$-model $M$ of $\mathsf{WKL}_0$ contains a real $C$ that codes a countable $\omega$-model of $\mathsf{WKL}_0$. Due to other weaknesses of $\mathsf{WKL}_0$, this does not cause $\mathsf{WKL}_0$ to be inconsistent! We identify the coded $\omega$-model $C$ not within $M$, but at a level one step above $M$; the model $M$ will not, in general, recognize that $C$ satisfies $\mathsf{WKL}_0$. So we are viewing $\mathsf{WKL}_0$ as our metatheory and our object theory, but not as our meta-meta-theory - we cannot prove the desired result in $\mathsf{WKL}_0$ because of incompleteness phenomena.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ This is indeed the kind of answer I expected when I wrote the question! $\endgroup$
    – Qfwfq
    Commented Mar 9, 2014 at 13:27
18
$\begingroup$

This answer is intended to clarify my comments to Sébastien's answer and also to propose a properly meta-meta-fact.

There is an intrinsic problem with the idea of meta-meta-theorems because theorems are mathematical ideas and therefore talking about them belongs in the meta-theory and hence cannot be properly meta-meta-theoretical. It's true that statements like "the meta-theory is incomplete" are, as stated, meta-meta-theoretical but once you sit down to formalize (I wish I could say "mathematicize") what that statement means, it suddenly loses its meta-meta-theoretical flavor and it becomes simply meta-mathematical or even plainly mathematical.

That doesn't mean that meta-meta-facts don't exist, they just need to involve ideas that are impossible to formalize in a mathematical sense. One such idea is the following variant of the sorites paradox. The understandable numbers have the following two properties:

  • $0$, $1$, $2$ are understandable and if $n$ is understandable then so is $n+1$.
  • The Ackermann number $A(5,5)$ is not understandable.

There is no mathematical concept that corresponds to understandable numbers since mathematical concepts obey mathematical induction and that contradicts the two properties above. However, the concept of understandable numbers still makes sense. That fact — understandable numbers make sense — is properly meta-meta-mathematical, though I would hardly call this a meta-meta-theorem since I can't imagine how I could prove this.

You don't have to go that far beyond mathematics to come across a meta-meta-mathematical statement. The statement "the meta-theory is incomplete" that I mentioned earlier is meta-meta-theoretical in intent. The similar statement "any meta-theory is incomplete" is even more clearly meta-meta-theoretical. This last statement is true in a practical sense since any practical meta-theory should interpret arithmetic and should be computably axiomatizable, but such theories are incomplete by Gödel's theorem. However, it is not really true that "any meta-theory is incomplete" since, for example, the theory of true arithmetic is complete and perfectly usable as a meta-theory, but the drawback is that we don't understand what the axioms of this theory actually are. As I just illustrated, depending on how you choose to formalize "any meta-theory is incomplete", you may get different answers. Each such answer is a meta-theorem but not a meta-meta-theorem because of the formalization process which involves a mathematical interpretation of the statements. To avoid this meta-collapse, you must resist the temptation to give the meta-meta-statement any concrete mathematical sense. The catch is that you can't really prove such meta-meta-statements without first transforming them into mathematical statements, so there is little hope in finding a meta-meta-theorem in any proper sense.

To further illustrate the issue, note that Gödel's Incompleteness Theorems were originally meta-meta-theorems: Gödel proved that the formal system of Principia Mathematica (PM) was incomplete and PM was intended by Russell and Whitehead as the foundation of all mathematics, i.e., the ultimate meta-theory. Today, we understand Gödel's results as meta-theorems that apply to any computably axiomatizable theory that can interpret enough arithmetic, regardless of whether such theories are thought of as meta-theories.

This collapse of meta-levels is systematic. A meta-meta-theorem is just a meta-theorem applied in the context of a meta-theory, and any meta-theorem applied in the context of a meta-theory is a meta-meta-theorem. Since the difference between a theory and a meta-theory is only one of intent, there is no concrete distinction between meta-theorems and meta-meta-theorems.

Improve this answer
$\endgroup$
13
  • $\begingroup$ So meta - meta - mathematical in intent is a little bit like physical in intent or financial in intent... that makes sense. $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Mar 9, 2014 at 4:04
  • 1
    $\begingroup$ I'm not sure to understand what meta-meta-theorem means for you, but compared to the content of your answer, it's normal because if there is a perfectly understandable definition, then it's a mathematical concept and then it's no more meta-meta but meta. So meta-meta theorems are statements that can't (yet?) make sense mathematically, but still make sense for the human mind, right? Then "the Riemann hypothesis is interesting" or "A. Grothendieck is a good mathematician", or ..., are meta-meta theorems: the non mathematically conceptualizable part of philosophy and history of mathematics. $\endgroup$
    – Sebastien Palcoux
    Commented Mar 9, 2014 at 12:36
  • $\begingroup$ One difficulty seems to be that, as some point, the $\text{(meta-)}^n\text{theory}$ has a strong chance of being inconsistent. So that may be the obstacle that prevents meta-meta-theorems from being just meta-theorems, if the meta-meta-theory is inconsistent. This seems to be the heart of the "understandable numbers" example. $\endgroup$
    – Carl Mummert
    Commented Mar 9, 2014 at 12:44
  • $\begingroup$ This answer seems to have nothing to do with my question... In particular, I really can't make sense of the phrase "There is an intrinsic problem with the idea of meta-meta-theorems because theorems are mathematical ideas and therefore talking about them belongs in the meta-theory and therefore cannot be properly meta-meta-theoretical" and of the entire second paragraph... $\endgroup$
    – Qfwfq
    Commented Mar 9, 2014 at 13:32
  • 4
    $\begingroup$ @Qfwfq: A "meta-theorem" is a theorem about a theory as opposed to a theorem in the theory. A "meta-meta-theorem" would be a theorem about the meta-theory. That's a fine idea but if you want to prove something about the meta-theory you first need to formalize it so that it is a theory you can prove something about. But then your meta-meta-theorem is just a meta-theorem, isn't it? This collapse of "metaness" systematically happens if you sit down to formalize and prove a meta-meta-statement. So every meta-meta-theorem is just a meta-theorem... $\endgroup$
    – François G. Dorais
    Commented Mar 9, 2014 at 13:56
13
$\begingroup$

You could let $\alpha_0$ be the statement Con(ZFC), and $\alpha_{n+1}$ be ZFC $\not\vdash\alpha_n$, and at limit ordinals $\alpha_\lambda$ is $(\forall \beta<\lambda)($ZFC $\not\vdash \alpha_\beta)$. Then for each computable ordinal $\lambda$, $\alpha_\lambda$ is true assuming $\alpha_0$ is. Which is a theorem of meta$^{\omega_1^{\text{CK}}}$-mathematics. :)

But we can view theoretical computer science, theoretical physics, mathematical finance, and in general the discipline studying mathematical descriptions of any phenomenon, as subsets of mathematics.

In which case metamathematics, being the mathematical description of mathematics, is also a subset of mathematics (and therefore meta$^\lambda$-mathematics is a subset of meta-mathematics).

(Acknowledgments: This answer is indebted to answer and comments of Sébastien and François.)

Improve this answer
$\endgroup$
4
  • $\begingroup$ Does ${\sf ZFC}\not\vdash\alpha_n$ represent “${\sf ZFC}$ cannot prove $\alpha_n$”? If so, then $\alpha_1$ represents “${\sf ZFC}$ cannot prove $\operatorname{Con}\left({\sf ZFC}\right)$”, right? Isn’t this statement logically equivalent in ${\sf ZFC}$ (or even ${\sf PA}$) to just $\operatorname{Con}\left({\sf ZFC}\right)$, i.e. $\alpha_0$? And, hence, all $\alpha_\beta$ are equivalent to $\alpha_0$ as well, no? $\endgroup$
    – Vladimir Reshetnikov
    Commented Apr 21, 2021 at 18:35
  • 1
    $\begingroup$ Ah... I guess I meant something like T_1= ZFC+Con ZFC, then T_2 = T_1+Con T_1 ... $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Apr 21, 2021 at 19:17
  • 2
    $\begingroup$ Yes, that version makes sense. But there are subtle issues with those definitions: the outcome depends on which exact representation for each recursive ordinal you choose at each step. See mathoverflow.net/q/67214/9550, mathoverflow.net/a/171723/9550. $\endgroup$
    – Vladimir Reshetnikov
    Commented Apr 21, 2021 at 19:28
  • $\begingroup$ OK, sure $\, \, \, \, \, $ $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Apr 21, 2021 at 19:38
12
$\begingroup$

There are statements which are independent but not provably independent

If the independence of a statement is a meta-mathematical theorem, then the existence of statements which are independent but not provably independent is a meta-meta-mathematical theorem.
See the post: Are there statements that are undecidable but not provably undecidable (undecidable is here synonymous of independent) and the positive answer (under ZFC, assuming its consistence).

Improve this answer
$\endgroup$
15
  • 3
    $\begingroup$ It's hard to imagine what "meta-meta" means. The meta theory is a theory like any other (e.g. PRA, PA, ZFC, depending on taste). Provability in such a theory is at the first "meta level," so the meaning of "independent but not provably independent" is just a conjunction of two statements at the first "meta level"; the apparent compounding of "metaness" is just an illusion. $\endgroup$
    – François G. Dorais
    Commented Mar 8, 2014 at 15:15
  • 1
    $\begingroup$ @FrançoisG.Dorais: "meta" is not an absolute notion, it is relative to a given theory. So, as a meta theory $T_1$ of a theory $T_0$ is also a theory, the meta-meta theory $T_2$ of a theory $T_0$ is also the meta theory of $T_1$, and also a theory. So if I understand well your comment, you think it's not relevant to call $T_2$ the meta-meta theory of $T_0$, right? $\endgroup$
    – Sebastien Palcoux
    Commented Mar 8, 2014 at 15:46
  • 3
    $\begingroup$ The problem lies in what happens when you formalize the meta-theory. Once you do that, the meta-theory becomes a plain theory. You can think of things like "the meta-theory is incomplete" as a meta-meta-statement but as soon as you formalize what this means it drops to a meta-statement because the act of formalizing happens in the meta-theory since that's what formalizing means. $\endgroup$
    – François G. Dorais
    Commented Mar 8, 2014 at 16:20
  • 3
    $\begingroup$ @CarlMummert: Yes, I think the only way to make sense of meta-meta-mathematics is with intent. There is no issue with a formal metatheory but the catch is that this is then a mathematical theory, so talking about it is meta-mathematics and not really meta-meta-mathematics (except for intent). There are indeed plenty of philosophical issues here as well as plenty of confusion. $\endgroup$
    – François G. Dorais
    Commented Mar 9, 2014 at 13:41
  • 2
    $\begingroup$ Regarding the answer: every statement that is independent of a theory like PA or ZFC will not be provably independent in that theory, since to prove that a statement is independent of a theory is to prove that the theory is consistent, and no such theory proves its own consistency by the second incompleteness theorem. $\endgroup$
    – Joel David Hamkins
    Commented May 27, 2016 at 22:58
1
$\begingroup$

If the question can be phrased like this “Is it possible to obtain a result in meta theory of a theory, which cannot be obtained in that theory”, then I believe the answer is “No”, and this can be proved in strict terms of mathematical logic. I did not look into detail, but I believe it is easy to prove the following

Theorem. For any theory T in language L and a metatheory T’ of T in language L’, such that L and L’ do not have symbols in common, there exists a common conservative extension of T and T'.

This theorem shows that whenever we obtain an interesting result in a meta theory T’ of a theory T, we can obtain same result in a conservative extension of T. In order to apply the theorem and get to this, we first rename all symbols in the axioms of T (and in the language of T’) so that the languages of T and T' do not have symbols in common, then apply the theorem.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ This is not strictly true because $T$ might have only finite models of a fixed size and $T'$ might have only infinite models. If we exclude that case, then any two theories, in disjoint languages, that both have infinite models have a common conservative extension, namely their disjoint union (and its consequences if you require theories to be closed under deduction). So this has nothing to do with "meta". Also, because you made the languages disjoint, $T'$ won't be able to prove anything nontrivial in the language of $T$. $\endgroup$
    – Andreas Blass
    Commented Jul 27, 2014 at 4:38
  • $\begingroup$ Good points. I was aware of more general statement with arbitrary T and T', but I phrased my statement so that the correlation "meta" between T and T' helps resolve the difficulties you discribed. A metatheory is said to be a theory "about" a theory. I treat this aboutness as a provision that both theories can be replaced by equivalent theories, such that difficulty with cardinality does not occur. Also, T' must encrypt the "knowledge" in T, and to avoid the difficulty in your last sentence, we add the missing correlations between symbols of two theories after taking their union. $\endgroup$
    – Ioachim Drugus
    Commented Jul 27, 2014 at 5:57
1
$\begingroup$

There has been a lot of discussion here about meta-meta-mathematics really not being a concrete notion, and the meta-meta-level collapsing to the meta-level because a meta-theory is of course, a theory.

However, I think the mistake many have implicitly made in the discussion is to assume that a meta-theory is "just" a theory. If $T_0$ is a theory (Which I will identify with its consequence relation $\vdash_{T_0}$ with a language $L_0$ of formulas, then a meta-theory $T_1$ is simply another consequence relation $\vdash_{T_1}$ whose language of formulas $L_1$ includes sentences of the form $"\Gamma \vdash_{T_0} \phi"$ for contexts $\Gamma$ and formulas $\phi$ in the base language $L_0$, such that: $$ \vdash_{T_1} "\Gamma \vdash_{T_0} \phi" \iff \Gamma \vdash_{T_0} \phi $$

So under this definition (which I think matches up with the intuitive idea of what a "metatheory" is, at least in my conception of it), a metatheory is a theory, but not just a theory -- it is a theory with additional structure.

Thus, in this sense we can meaningfully talk about meta-meta-theories by treating a meta-theory $T_1$ as a theory, and finding a metatheory $T_2$ for $T_1$ (treated as a theory). This alone would simply be a meta-theory again, but if we keep the structure of the metatheory $T_1$ (instead of throwing it away and simply treating it like a theory), we obtain an honest-to-goodness metametatheory, which would have something like the structure:

$$ ((\vdash_{T_2},L_2),(\vdash_{T_1},L_1),(\vdash_{T_0},L_0)) $$

together with two "quoting operations" as I have described above, letting the metametatheory talk about the consequence relation of the metatheory, and the metatheory talk about the consequence relation of the base theory.

Godel's incompleteness theorem, though as mentioned in François G. Dorais' answer was originally formulated to talk about the "metatheory" PM, did not meaningfully make use of the metatheoretical structure in PM, and thus is not an honest-to-goodness metametatheorem, which would make meaningful use of the structure I have described above.

Whether or not such mathematics has been done, I'm not sure. Possibly Carl Mummert's answer gives an example of such of a study which cannot meaningfully be reduced to simply metamathematics, but I'm afraid without knowing the details it is difficult for me to comment definitively.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .