Timeline for Tuple machinery in I-Sigma_0
Current License: CC BY-SA 2.5
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2017 at 12:57 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
| Sep 17, 2010 at 1:57 | vote | accept | CommunityBot | ||
| Sep 17, 2010 at 1:54 | comment | added | Kaveh | [continued] The trick is to modify the $\Delta_0$ formula such that we can prove something satisfies it and that the minimum will be the required sequence. Consider the formula which states that $s$ is a sequence of length $n$, the last member of the sequence is at least $n$, and each member is at most one larger that previous one. Let $m$ be largest number of length $len(n)$. Now we can compute the code of the sequence $m,m,...,m$ directly using $Exp$, and show that it satisfies the formula. Then use the bounded minimization to get the least number and show that it should be the sequence. | |
| Sep 17, 2010 at 1:27 | comment | added | Kaveh | @Ricky: First, I should have written "add 2 between them" in place of "add 4 between them". For the proof of totality, lets assume we want to get a sequence that codes numbers from 1 to n. Note that the graph of this functions is easy to check, if we are given a pair of numbers $s$ and $n$ we can easily check whether $s$ is coding the sequence $1,2,...,n$ (it is a $\Delta_0$ property); that we can carry out bounded minimization for $\Delta_0$ formulas; and we can get a bound on the coding of the sequence using $Exp$. | |
| Sep 16, 2010 at 7:16 | comment | added | user5810 | @Kaveh, How would a proof of the totality of the coding go in I-Delta_0 + Exp? | |
| Sep 16, 2010 at 4:47 | comment | added | Kaveh | Another way of coding which is more efficient is using 4 digits, write numbers in the sequence in binary and add 4 between them, and read the resulting number in base 4. | |
| Sep 16, 2010 at 4:45 | comment | added | Kaveh | The problem is not defining a coding of sequences, it is easy to define a coding for sequences (checking if if s is a valid code and computing the i-th member of s, concatenating two sequences, computing the length of the sequence, ...), the problem is proving the totality of the coding, which intuitively should not be possible for reasonable theories as long as they can't prove exponentiation is total, and if you can prove totality of exponentiation then it is easy to prove the totality of the coding. | |
| Sep 15, 2010 at 22:14 | comment | added | user5810 | (I think) You don't even need Sigma_1 induction, you just need Elementary Arithmetic. | |
| Sep 15, 2010 at 20:58 | comment | added | Joel David Hamkins | Ricky, the coding proof I had in mind seems to use more than $\Delta_0$ induction. François, for the Tennenbaum application, you don't actually need totality, but only that the coding overspills into the nonstandard part---it suffices if we have a single nonstandard $d$ for which there is a code of the length $d$ computations. For this, $\Sigma_1$ induction suffices, since the fact that for every $n$ has a code is true in the standard part, and hence overspills. This is also why it suffices to prove as Dave mentions that there is a nonstandard initial segment with PA, or $\Sigma_1$-induction. | |
| Sep 15, 2010 at 19:17 | comment | added | user5810 | I don't see how I_Delta_0 + Exp can prove it, either. (Although I do see how Elementary Arithmetic citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.6509 could prove it.) | |
| Sep 15, 2010 at 18:31 | answer | added | Dave Marker | timeline score: 2 | |
| Sep 15, 2010 at 13:42 | comment | added | François G. Dorais | This seems to need the totality of exp. I don't think you can get by with less than that if you want a reasonable coding. I would suggest working in $I\Delta_0 + Exp$ unless you have a really reason to only work in $I\Delta_0$. | |
| Sep 15, 2010 at 5:26 | history | asked | user5810 | CC BY-SA 2.5 |