On verifying that primitive-recursive functions are provably total in PA
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 25/100
- Issue type
- Documentation
- Clarity
- Mostly clear
- Activity status
- Stale
- Tech stack
- tex
- Domain
- content, documentation
Research direction
Start by reviewing the book's beta function lemma and its use of the factorial function. Compare the proposed lcm(1,...,j) replacement and ensure the added remark explains, without circularity, that primitive-recursive functions are provably total in PA; done means the argument is complete and consistent with the existing proof.
Written by the indexing model from the issue text.
Description
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?
- Dominant language
- TeX
- Stars
- 1.4k
- Forks
- 289
- PR merge metrics
- No merged PRs in 30d
Getting set up
This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from OpenLogicProject/OpenLogic
-
Difficulty 1/5 Under an hour Newbie friendliness 65/100
OpenLogicProject/OpenLogic#339 · 1 comment ·
-
Difficulty 4/5 3-5 days Newbie friendliness 50/100
OpenLogicProject/OpenLogic#436 ·
-
Difficulty 3/5 1-2 days Newbie friendliness 68/100
OpenLogicProject/OpenLogic#435 · 1 comment ·
-
Difficulty 5/5 Over a week Newbie friendliness 30/100
OpenLogicProject/OpenLogic#425 · 1 comment ·
-
Improve docsOpen
Difficulty 5/5 Over a week Newbie friendliness 25/100
OpenLogicProject/OpenLogic#390 ·
All issues in OpenLogicProject/OpenLogic
Similar issues
-
Edit:Opencheck:failed streams:edit
Difficulty 2/5 1-3 hours Newbie friendliness 60/100
iptv-org/iptv#54352 · 1 comment ·
Maintainers usually reply within 1 day
-
priority: medium
Difficulty 2/5 1-3 hours Newbie friendliness 65/100
lapanti/lavanti.fi#1565 · 2 comments ·
Maintainers usually reply within 1 day
-
documentation
Difficulty 1/5 Under an hour Newbie friendliness 88/100
Maintainers usually reply within 1 day
-
documentation
Difficulty 1/5 Under an hour Newbie friendliness 88/100
githubnext/gh-aw-workshop#4242 ·
Maintainers usually reply within 1 day
-
Difficulty 1/5 Under an hour Newbie friendliness 72/100
eryajf/learning-weekly#145 ·