Timeline for Large cardinal axioms and total recursive functions
Current License: CC BY-SA 3.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 8, 2012 at 17:00 | vote | accept | Joerg Zimmermann | ||
| Jun 8, 2012 at 17:01 | |||||
| Jun 8, 2012 at 16:59 | comment | added | Joerg Zimmermann | First of all, thanks a lot for your quick and enlightening answers! Also the discussion about intensional and extensional definitions raises an important point for further contemplation. As Francois has correctly remarked, in my context the intensional view seems to be appropriate, because I deal with programs executed on a universal reference TM. It is fascinating, that these large cardinals, which are directly concerned with unfathomable infinities, have such interesting implications for effective objects. | |
| Jun 8, 2012 at 16:41 | comment | added | Emil Jeřábek | ... In contrast, there is no easy description of the set of all TM provably total in $T$. Generally speaking, one can only guarantee provable totality of TM that run in time $2_k^n$ for some syntactic reason, such as when the TM implements an explicit clock. However, there are also provably total TM that do not follow such an easily recognizable pattern (loosely speaking; the set of all provably total TM is of course r.e.). | |
| Jun 8, 2012 at 16:36 | comment | added | Emil Jeřábek | I forgot to mention that there is also a pragmatic reason: provably total functions of a theory often have a simple description. For example, the provably total recursive functions of $T=I\Delta_0+\mathrm{EXP}$ are exactly the elementary function, i.e., functions computable in time $O(2_k^n)$ for some constant $k$. Every such function is computable by a TM provably total in $T$, but it is not true that every TM running in time $O(2_k^n)$ is provably total in $T$; that a particular TM halts in $2_k^n$ steps on any input is a $\Pi_1$ statement that may or may not be provable in $T$. ... | |
| Jun 8, 2012 at 14:01 | comment | added | Joel David Hamkins | That makes sense. | |
| Jun 8, 2012 at 13:47 | comment | added | Emil Jeřábek | ... There are other ways to study the $\Pi^0_1$ fragment of the theory, such as using consistency statements. | |
| Jun 8, 2012 at 13:47 | comment | added | Emil Jeřábek | You can study provably total algorithms (TM) if you wish, it’s perfectly sensible. I was simply pointing out that the (fairly traditional) definition of a provably total function does not distinguish different algorithms computing the same function. The rationale, I suppose, is that this characteristic of the theory is a set of combinatorial objects (functions), which can be studied with tools unrelated to logic. (The situation is akin to ordinals of a theory, there you also abstract away different definitions of the same ordinal.)... | |
| Jun 8, 2012 at 13:24 | comment | added | Joel David Hamkins | Emil, you are saying that when studying provable totality, one always throws the $\Pi^0_1$-theory of $\mathbb{N}$ into the theory? Why is this? The question seems to be perfectly sensible for theories not containing this extra stuff. | |
| Jun 8, 2012 at 13:21 | comment | added | François G. Dorais | From the last paragraph of the question, it looks like the author may be interested in the $\Pi_2$ fragment of $T$ rather than that of $T+\mathrm{Th}_{\Pi_1}(\mathbb{N})$. In that case Joel's interpretation of provably total would be more appropriate than Emil's (for the purpose of answering the question). Perhaps the Joerg should clarify which he meant... | |
| Jun 8, 2012 at 13:00 | comment | added | Emil Jeřábek | @Joel: Yes, different definitions of the same function may differ in their totality. Consider this as a feature. Essentially, the p.t.r.f. of a theory describe the $\Pi^0_2$ fragment of $T+\operatorname{Th}_{\Pi^0_1}(\mathbb N)$. | |
| Jun 8, 2012 at 12:59 | comment | added | Joel David Hamkins | TM programs and $\Sigma^0_1$ assertions are essentially equivalent. My formula $\phi(x,y)$ is ``$x$ is not the code of a proof of a contradiction and $y=1$'', which has the same intentional content of the program. The stronger theory proves $\forall n\exists!m\ \phi(n,m)$, but ZFC does not. | |
| Jun 8, 2012 at 12:33 | comment | added | Jacques Carette | The gap here is indeed that the TM program and the formula are not essentially equivalent -- the TM program has some intensional content not present in the formula $f(n)=1$, as the 'proviso' on $n$ is externally invisible. If denotational semantics was that easy, the whole theory would not exist... | |
| Jun 8, 2012 at 11:31 | comment | added | Joel David Hamkins | Emil, you are the expert on this topic, so I defer to you. I consider using the TM program or the formula $\phi$ to be essentially equivalent. It seems that we should refer to the function by a particular $\phi$, though, since it may be the case that we can prove that one $\phi$ gives rise to a total function, but we can't prove it for another, even when the functions happen to be the same (in the standard model or with respect to a stronger theory). That is the situation of my first example, where the function happens to be the constant $1$ function, but ZFC does not prove it. | |
| Jun 8, 2012 at 11:05 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 853 characters in body
|
| Jun 8, 2012 at 11:00 | comment | added | Emil Jeřábek | The standard definition of a provably total recursive function is as follows: an $f\colon\omega\to\omega$ is a p.t.r.f. of a theory $T$ if there exists a $\Sigma^0_1$-formula $\phi(x,y)$ such that $T\vdash\forall x\,\exists!y\,\phi(x,y)$ and for every $n\in\omega$, $\mathbb N\models\phi(n,f(n))$. As you can see, the definition is purely extensional, it does not refer to particular TM. | |
| Jun 8, 2012 at 10:54 | comment | added | Joel David Hamkins | But the assertion that $f$ is like that is not provable in ZFC. We are refering to the functions by their TM programs. | |
| Jun 8, 2012 at 10:39 | comment | added | Emil Jeřábek | $f$ is the constant $1$ function, hence provably total in ZFC. | |
| Jun 8, 2012 at 10:29 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |