Timeline for What assumptions and methodology do metaproofs of logic theorems use and employ?
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 7, 2019 at 17:32 | comment | added | Ingo Blechschmidt | About the possible mismatch between the object logic and the meta logic: Most of the time this isn't a problem. But sometimes one gets unexpected results. For instance, if we adopt some ultrafinitist meta theory, then we might be in doubt regarding expressions such as $2^{2^{2^{2^2}}}$. However, Peano Arithmetic easily proves that these ultrafinitistic systems verify the existence of these large numbers, essentially by repeating the (ultrafinitistically acceptable) principle "the successor of any number exists" sufficiently (non-ultrafinitistically-acceptably often) often. | |
| Jan 7, 2019 at 17:30 | comment | added | Ingo Blechschmidt | A common base system for proving the basic results of the study of formal systems (such as representability of computable functions, the diagonal lemma, Gödel's incompleteness theorems and so on) is ... informal human reasoning! A common formal such system is PRA, primitive-recursive arithmetic. | |
| Jan 14, 2010 at 8:20 | comment | added | Charles Stewart | Cf. mathoverflow.net/questions/11699/… | |
| Jan 13, 2010 at 13:04 | answer | added | Charles Stewart | timeline score: 1 | |
| Dec 20, 2009 at 2:40 | answer | added | abcdxyz | timeline score: 1 | |
| Dec 14, 2009 at 13:16 | vote | accept | CommunityBot | ||
| Dec 14, 2009 at 9:50 | answer | added | Neel Krishnaswami | timeline score: 8 | |
| Dec 14, 2009 at 7:24 | history | asked | user2529 | CC BY-SA 2.5 |