On verifying that primitive-recursive functions are provably total in PA

[iblech]

As far as I see, the book doesn't state or prove that primitive-recursive functions are provably total in PA; but most of the ingredients are there! The only thing missing is an explanation that Peano arithmetic proves that one can append elements to lists (coded via the beta function as numbers). I'd like to write a remark sketching that argument. Is there interest in that?

There is, however, a slight problem. The construction given in the proof of the beta function lemma uses the factorial function. I don't know how to verify in a non-circular fashion that the factorial function is total. I'd therefore change j! to lcm(1,...,j). Unlike the factorial function, the function j \mapsto lcm(1,...,j) can be represented and verified to be total without recourse to the beta function. The rest of the proof can be adapted to this change with extremely minimal effort. Am I missing something? Should I go ahead with the change?

[rzach]

I'll think about the change to the beta function lemma. One fundamental principle I like to follow is that proofs remain as simple as possible. I would definitely welcome an explanation of provably total functions -- could be its own chapter! If the change from factorial to lcm makes the beta function lemma harder to understand on a first read, my instinct would be to re-prove it with the change (and perhaps an explanation why the original proof isn't enough). That said, for the typical non-math student the beta function lemma may be a black box anyway. I'll see @avigad on Monday and ask him what he thinks.

[iblech]

Any updates on this? My current (research and teaching) focus is not on these foundational matters, hence there is no need to hurry from my side, but I still believe this issue to be relevant.

In my personal opinion, I don't think that the change to the lcm function will make the proof substantially harder.

[rzach]

Sorry that I spaced on this. I did talk to Jeremy at the time and IIRC he was intrigued. Before making the change in https://github.com/OpenLogicProject/OpenLogic/blob/master/content/incompleteness/representability-in-q/beta-function.tex via pull request, maybe let's see how it'd look with the change. What's there right now is just a sketch and doesn't have enough detail anyway. Eg I never go through the proof, just use the fact. So in other words: go ahead! But let's put the new material (including a changed beta function lemma discussion) into a new chapter -- or just do it offline for now, by email. When it's done I'll either revise the old section.