Timeline for Where are we working when we prove metamathematical theorems?
Current License: CC BY-SA 2.5
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 16 at 19:40 | comment | added | plm | A simple comment: Most metatheorems are proved in the same theory as theorems, only when studying proofs, in order typically to find minimal requirements, does one use weak theories. Thus i would say that the majority of metatheorems are proved and thought about in set theory, possibly with urelements. In fact mathematics is nowadays the foundation, language of science, in particular of metamathematics, and set theory being the standard FOM it is by default also the FOmetaM. Standard logic textbooks, eg Enderton's, are formulated in set theory, with rare remarks on the axioms used or needed. | |
| Apr 12, 2018 at 16:05 | comment | added | user21820 | Historically, Godel was careful to use 'finitistic' and 'constructive' reasoning in proving his incompleteness theorems, so that it would be indisputable that Hilbert's goal was impossible to achieve. It is true that philosophically there are some initial assumptions that must be made otherwise we cannot even get started (as I sketch in the linked post), but practically all modern logicians think that ACA is sound, and ACA is sufficient to prove Godel's incompleteness theorems and completeness theorems. (And note that whether X is meaningful or not is irrelevant to what ACA proves about X.) | |
| Apr 12, 2018 at 15:59 | comment | added | user21820 | See this post on building blocks and then this continuation about the incompleteness theorems. In short, if you accept only string manipulation and induction you are basically stuck at PA, which is insufficient to prove the incompleteness theorem in a form that is 'internally' meaningful, because the sentence Con(S) can be imbued with meaning only if your meta-system can talk about Σ1-sets, at which point you effectively have the halting oracle. | |
| Apr 13, 2017 at 12:58 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
| Jan 15, 2010 at 3:43 | vote | accept | Zev Chonoles | ||
| Jan 14, 2010 at 14:50 | answer | added | François G. Dorais | timeline score: 12 | |
| Jan 14, 2010 at 8:36 | answer | added | Charles Stewart | timeline score: 4 | |
| Jan 13, 2010 at 23:41 | comment | added | François G. Dorais | Perhaps reading the introduction to Gödel's paper would clarify things for that particular case. A nice translation can be found here: research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf | |
| Jan 13, 2010 at 22:49 | comment | added | Andrej Bauer | This question would make more sense, or would at least be easier to answer, if you provided a couple more examples of what you have in mind. Logicians are pretty well aware of what sort of meta-theory is necessary to prove various meta-theorems. | |
| Jan 13, 2010 at 22:04 | history | edited | Zev Chonoles | CC BY-SA 2.5 |
added 2 characters in body
|
| Jan 13, 2010 at 21:59 | history | edited | Zev Chonoles | CC BY-SA 2.5 |
explanation; added 11 characters in body
|
| Jan 13, 2010 at 21:56 | history | undeleted | Zev Chonoles | ||
| Jan 13, 2010 at 21:56 | history | deleted | Zev Chonoles | ||
| Jan 13, 2010 at 21:49 | history | asked | Zev Chonoles | CC BY-SA 2.5 |