Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

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

オープン
  • 何か問題がありますか？
#160 コメント 9 件 リアクション 0 件 担当者 0 名 GitHub で見る

まだ誰も着手していません。

評価

難易度
4/5
見積もり時間
3〜5日
初心者へのやさしさ
25/100
issue の種類
ドキュメント
明瞭さ
おおむね明確
活発さ
停滞
技術スタック
tex
領域
content, documentation

調査の方向性

まず、本のベータ関数補題と、そこでの階乗関数の使用を確認してください。提案されている lcm(1,...,j) への置き換えを比較し、追加された注記が、循環論法なしに、原始再帰関数が PA で証明可能な全域関数であることを説明していることを確認してください。議論が完全で、既存の証明と整合していれば完了です。

索引モデルが issue の本文から書いたものです。

説明

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?

主要言語
TeX
スター
1.4k
フォーク
289
30日以内にマージされた PR はありません

環境構築

このプロジェクトには開発コンテナ、Dockerfile、コントリビューションガイドがありません。まず README を読み、一般的な手順ははじめてのコントリビューションガイドを参照してください。

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

OpenLogicProject/OpenLogic のほかの issue

OpenLogicProject/OpenLogic の issue をすべて見る

似ている issue

Content の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。