23

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?

Qfwfq
  • 22,715

6 Answers6

34

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.

Carl Mummert
  • 9,593
19

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.

François G. Dorais
  • 43,723
  • So meta - meta - mathematical in intent is a little bit like physical in intent or financial in intent... that makes sense. – Bjørn Kjos-Hanssen Mar 09 '14 at 04:04
  • 1
    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. – Sebastien Palcoux Mar 09 '14 at 12:36
  • 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. – Carl Mummert Mar 09 '14 at 12:44
  • 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... – Qfwfq Mar 09 '14 at 13:32
  • Also, the phrase " 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" doesn't make any sense to me. Perhaps I'm just missing something (after all, I'm absolutely no expert in Logic!), but my impression is that you understand the "meta-" word as indicating something philosophical and not entirely within the reach of formal mathematics, which is not the intended meaning in my question. – Qfwfq Mar 09 '14 at 13:36
  • 4
    @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... – François G. Dorais Mar 09 '14 at 13:56
  • @SébastienPalcoux: I don't think meta-meta-theorems make sense since the theorems are mathematical ideas so talking about them is always simply meta-mathematics. As I tried to explain in my answer, this doesn't apply to all concepts. You can have meta-meta-statements, some of which are meta-meta-facts, but you can't prove such things unless you collapse them to meta-theorems. – François G. Dorais Mar 09 '14 at 14:02
  • @Qfwfq: True arithmetic is the theory of the standard model of arithmetic. This is a complete theory since every arithmetic statement is either true or false in the standard model. Unfortunately, this theory is not computably axiomatizable which makes it difficult to understand. – François G. Dorais Mar 09 '14 at 14:09
  • @FrançoisG.Dorais: I agree. Now, are you willing to go further, by saying that the non mathematically conceptualizable part of philosophy of mathematics, is meta-meta-mathematics. Next, as "Theories do not have associated meta-theories" (you said), meta-theories do not have associated meta-meta-theories, and so, meta-meta-mathematics would be non mathematically conceptualizable theories about mathematics, meta-mathematics, but also meta-physics, meta-biology... and so meta-meta-mathematics would be exactly the non mathematically conceptualizable part of Philosophy in general. – Sebastien Palcoux Mar 09 '14 at 14:26
  • @SébastienPalcoux: That's a fair assessment. – François G. Dorais Mar 09 '14 at 14:44
  • This answer is the best thing I read all day today! – Vincent Sep 29 '16 at 20:51
  • @FrançoisG.Dorais: You write "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." Do you really think that Russell and Whitehead intended PM to be a meta theory. I guess Gödel was the first one who realized that theories of arithmetic (and thus also PM) can speak about logical systems (including themselves) through Gödel numbering. Did Russell and White realize –  Nov 15 '16 at 19:27
  • that in PM one can express statements like "PM is incomplete"? –  Nov 15 '16 at 19:28
14

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

Bjørn Kjos-Hanssen
  • 24,629
  • 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? – Vladimir Reshetnikov Apr 21 '21 at 18:35
  • 1
    Ah... I guess I meant something like T_1= ZFC+Con ZFC, then T_2 = T_1+Con T_1 ... – Bjørn Kjos-Hanssen Apr 21 '21 at 19:17
  • 1
    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 https://mathoverflow.net/q/67214/9550, https://mathoverflow.net/a/171723/9550. – Vladimir Reshetnikov Apr 21 '21 at 19:28
  • OK, sure $, , , , , $ – Bjørn Kjos-Hanssen Apr 21 '21 at 19:38
12

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

Community
  • 1
Sebastien Palcoux
  • 25,922
  • 3
    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. – François G. Dorais Mar 08 '14 at 15:15
  • 1
    @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? – Sebastien Palcoux Mar 08 '14 at 15:46
  • 1
    Theories do not have "associated meta-theories". In the meta-theory, you can formalize first-order syntax and talk about any theory (PRA, PA, ZFC, etc.); you don't change meta-theory every time you talk about a different theory. – François G. Dorais Mar 08 '14 at 15:51
  • 1
    @FrançoisG.Dorais: I see, thank you. So in some sense "meta" is an absolute notion, and "meta-meta" is not well-defined, or, as you said, an illusion, and then exists just as a misnomer, right? – Sebastien Palcoux Mar 08 '14 at 16:02
  • 3
    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. – François G. Dorais Mar 08 '14 at 16:20
  • @ the above commenters: Let me try to clarify a bit what I mean by "meta-theory". Suppose we start with your favourite (say "set theoretical") theory $T_2$; then assume another theory $T_1$ can be codified inside $T_2$: the formulas of $T_1$ are really particular kinds of sets. We say that $T_2$, together with the choice of way in which $T_1$ is codified within $T_2$, is a meta-theory for $T_1$, and some statements in the language of $T_2$ about those sets are meta-theoretical statements about $T_1$. – Qfwfq Mar 08 '14 at 20:46
  • (...) We also say that $T_2$ is a meta-meta-theory for a theory $T_0$ if we specify a choice of $T_1$ and a codification of $T_0$ in $T_1$ and of $T_1$ in $T_2$, so that $T_2$ is a meta-theory for $T_1$ and $T_1$ is a meta-theory for $T_0$. – Qfwfq Mar 08 '14 at 20:48
  • 1
    Consider Löb’s theorem: if $T$ proves that the provability of $A$ in $T$ implies $A$, then $T$ proves $A$. Note that $A$ appears on two different levels in this statement, so is $T$ here a theory, meta-theory, or what? In other words, I think the distinction between theorems, meta-theorems, and so on is ill-defined. – Emil Jeřábek Mar 08 '14 at 21:10
  • @Emil Jeřábek: Well, I would informally say that in this case there are two copies of $T$: one serving as a metatheory (call it $T_2$) for the other (call it $T_1$). More formally: $T_1$ is somehow codified inside $T_2$; assuming for simplicity $T_2$ were some kind of set theory (whatever it means): then $T_1$ itself would be a family of sets (described formally by sentences of $T_2$), as well as the sentences expressible within $T_1$. So, if I understand correctly, Loeb's theorem states: if $T_2$ proves the sentence $(T_1 \vdash A_1)\to A_2$, then $T_2$ proves $A_2$ (...) – Qfwfq Mar 08 '14 at 22:22
  • (...) where $A_1$ is a set codifying a sentence of $T_1$, and $A_2$ is a sentence of $T_2$ (which happens to have exactly the same heuristic meaning as $A_1$, like $T_1$ and $T_2$ are just two formalizations in two different levels of abstraction of the "same" heuristic "theory" $T$). – Qfwfq Mar 08 '14 at 22:26
  • 1
    @François: perhaps the distinction between the object theory and the metatheory is not one of formalization, but is about intent instead? I don't see any issue with a formal metatheory still being used as a metatheory. There are several philosophical issues with the concept of "metatheory", as used in contemporary practice, that I would love to see someone write about. One source of confusion seems to be a lingering association of "metatheory" with weak syntactical theories such as PRA useful for Hilbert's program (these metatheories are almost always formal). – Carl Mummert Mar 09 '14 at 13:08
  • 3
    @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. – François G. Dorais Mar 09 '14 at 13:41
  • 2
    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. – Joel David Hamkins May 27 '16 at 22:58
  • On the other hand, a strong enough theory T can certainly prove that, given Con(T), certain statements are independent of T (for example, the second incompleteness theorem says this is true of the statement Con(T) itself). It might then be interesting to consider whether T + Con(T) cannot prove certain statements to be independent of T. – Robin Saunders Nov 15 '16 at 18:41
  • @JoelDavidHamkins But isn't the linked answer about something different? Namely we are interested in a statement $\varphi$ such that 1) $\text{ZFC} \nvdash \varphi$, 2) $\text{ZFC} \nvdash \neg\varphi$, and 3) $\text{ZFC} \nvdash \text{Con(ZFC)} \to (\neg\text{Prov}(\varphi) \land \neg\text{Prov}(\neg\varphi))$. The answer proves (in ZFC, assuming $\Sigma_1$ soundness) that such statements should exist. But do we actually concretely know such statements? (Or maybe I misunderstood you or that answer) – Jori Jul 02 '20 at 00:11
1

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.

Ioachim Drugus
  • 829
  • 1
    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$. – Andreas Blass Jul 27 '14 at 04:38
  • 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. – Ioachim Drugus Jul 27 '14 at 05:57
1

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.

Nathan BeDell
  • 111