Timeline for Notion of Truth and Axioms
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 25, 2011 at 12:13 | comment | added | Emil Jeřábek | Maybe I should also mention that bounded arithmetic is interpretable (on a cut) in Robinson’s Q, so it has as low a proof theoretic strength as it can get. (This is in fact the main reason why Gödel’s second incompleteness theorem applies already to Q and its extensions.) | |
| Aug 25, 2011 at 10:55 | comment | added | Emil Jeřábek | ... PV (originally introduced by Cook as an equational theory) has a language containing function symbols for all polynomial-time functions, and it is axiomatized by basic defining equations for these functions plus induction for open formulas in its language. You can find more on bounded arithmetic in Chapter V of Hájek & Pudlák “Metamathematics of first-order arithmetic”, Buss’s PhD thesis (available on his home page), Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, or Cook & Nguyen “Logical foundations of complexity theory”. | |
| Aug 25, 2011 at 10:46 | comment | added | Emil Jeřábek | Bounded arithmetic is a generic name for fragments of arithmetic that only have induction for (a subset of) bounded formulas (i.e., only with quantifiers $\exists x\le t\,\phi(x)$, $\forall x\le t\,\phi(x)$) in the original arithmetical language or its slight extensions (meaning basically that there should not be any function in the language with exponential growth). The prototypical example is $I\Delta_0$, though it turns out more useful to study theories in an expanded language that allows to prove all polynomial-time computable functions total (Buss’s theories). ... | |
| Aug 24, 2011 at 17:50 | comment | added | user12806 | Thanks, Emil. What are bounded arithmetic and PV ? | |
| Aug 23, 2011 at 11:49 | comment | added | Emil Jeřábek | PRA is an overkill. A weak fragment of bounded arithmetic (such as PV or $S^1_2$) is enough, provided $T$ is presented with a polynomial-time set of axioms (which is not a significant restriction, by Craig’s trick). | |
| Aug 21, 2011 at 16:31 | vote | accept | user12806 | ||
| Aug 21, 2011 at 16:31 | vote | accept | user12806 | ||
| Aug 21, 2011 at 16:31 | |||||
| Aug 21, 2011 at 12:01 | history | answered | Carl Mummert | CC BY-SA 3.0 |