Timeline for Interesting meta-meta-mathematical theorems?
Current License: CC BY-SA 3.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 2, 2020 at 0:11 | comment | added | Jori | @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) | |
| Apr 13, 2017 at 12:19 | history | edited | CommunityBot |
replaced http://math.stackexchange.com/ with https://math.stackexchange.com/
|
|
| Nov 15, 2016 at 18:41 | comment | added | Robin Saunders | 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. | |
| May 27, 2016 at 22:58 | comment | added | Joel David Hamkins | 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. | |
| Mar 9, 2014 at 13:41 | comment | added | François G. Dorais | @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. | |
| Mar 9, 2014 at 13:08 | comment | added | Carl Mummert | @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). | |
| Mar 8, 2014 at 22:26 | comment | added | Qfwfq | (...) 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$). | |
| Mar 8, 2014 at 22:22 | comment | added | Qfwfq | @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$ (...) | |
| Mar 8, 2014 at 21:10 | comment | added | Emil Jeřábek | 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. | |
| Mar 8, 2014 at 20:48 | comment | added | Qfwfq | (...) 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$. | |
| Mar 8, 2014 at 20:46 | comment | added | Qfwfq | @ 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$. | |
| Mar 8, 2014 at 16:20 | comment | added | François G. Dorais | 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. | |
| Mar 8, 2014 at 16:02 | comment | added | Sebastien Palcoux | @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? | |
| Mar 8, 2014 at 15:51 | comment | added | François G. Dorais | 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. | |
| Mar 8, 2014 at 15:46 | comment | added | Sebastien Palcoux | @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? | |
| Mar 8, 2014 at 15:15 | comment | added | François G. Dorais | 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. | |
| Mar 8, 2014 at 13:55 | history | edited | Sebastien Palcoux | CC BY-SA 3.0 |
Minor edit
|
| Mar 8, 2014 at 13:34 | history | edited | Sebastien Palcoux | CC BY-SA 3.0 |
I've replaced undecidable by independent.
|
| Mar 8, 2014 at 13:22 | history | edited | Sebastien Palcoux | CC BY-SA 3.0 |
added 160 characters in body
|
| Mar 8, 2014 at 13:15 | history | answered | Sebastien Palcoux | CC BY-SA 3.0 |