Timeline for Is there any current development of a first order formalization of metamathematics?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 15, 2014 at 7:47 | answer | added | Ioachim Drugus | timeline score: -2 | |
| Aug 7, 2014 at 23:47 | comment | added | François G. Dorais | You might also find this interesting - r6.ca/Goedel/goedel1.html | |
| Aug 7, 2014 at 23:22 | comment | added | dezakin | Thanks, I'll check it. I was mostly motivated in asking questions about satisfiability, decidability, and provability about questions inside an automated theorem proving system, so I need to be able to formalize all definitions if I want to ask a question about a particular well formed formula like "Is this a decidable statement?" or "Is this a satisfiable statement?" or "Do statements that have this form fall in the set of decidable statements?" | |
| Aug 7, 2014 at 23:02 | comment | added | François G. Dorais | You can do nearly 100% of it in PRA and 97% in much less... See the article by Craig Smorynski in the Handbook of Mathematical Logic for a detailed exposition. | |
| Aug 7, 2014 at 22:50 | comment | added | dezakin | The definition of a Gödel numbering is done in the metatheory, along with other definitions for making informal proofs. I'm looking for formal first order definitions, including of Gödel numberings. Arithmetic is embedded in set theory, but without the appropriate definitions its hard to ask questions about arithmetic in raw set theory, and without the appropriate definitions in arithmetic, its hard to ask questions about Gödel numbering of formula in arithmetic. | |
| Aug 7, 2014 at 22:35 | comment | added | Noah Schweber | I'm confused: in light of Goedel coding, how isn't first-order arithmetic already a "logic of proofs" (and other things besides)? My understanding was that weaker systems, like modal logics of proofs, are fragments of first-order arithmetic, although I could be wrong (theories axiomatizing notions of truth are really really strong, but these aren't quite theories of provability). | |
| Aug 7, 2014 at 22:32 | history | edited | dezakin | CC BY-SA 3.0 |
formatting, comma usage.
|
| Aug 7, 2014 at 22:08 | history | asked | dezakin | CC BY-SA 3.0 |