数学基礎論アドベントカレンダー2022投稿用

数学基礎論アドベントカレンダー2022投稿用の記事です。命題の証明などを紹介している人が多い中で申し訳ありませんが、Alweさんがyukicoderの宣伝でも良いと言っていたのでyukicoderの宣伝をします。

結論から言うと、プログラミングができる人向けに「yukicoderは基礎論学習のために便利かもしれない」という話をするのですが、そのために色々と準備をします。

数学の学習方法

まず数学の学習方法には色々あり、メジャーなのは

• 教科書や論文を読む
• 演習問題を解いたり解説を読んだりする
• セミナーを行う

辺りだと思います。

一方であまりメジャーな学習方法ではありませんが今回おすすめしたいのが、

• 演習問題を不備なくちょうどいい難易度で作り丁寧で行間のない解説を作ったりすること

です。行間のない解説を作ること自体は数学基礎論アドベントカレンダー参加者の多くの人たちが慣れていると思いますが、演習問題を作成することに慣れている人はあまり多くないかもしれませんね。

何故演習問題を作ると良いのでしょう？　まず演習問題を作る際に重要であることは

1. 問題文の意図が第三者に明確に伝わること
   1. 条件の書き漏らしは絶対にしないこと
   2. 複雑な定義もぼかさず厳密に説明すること）
2. 演習問題が第三者に有限の時間で解けること
   1. 解き方が有名でなく自分の思いつきや難しい事実に激しく依存する場合、適切な誘導をつけること
      1. 出典がある場合はきちんと引用すること
      2. 演習問題の対象をある程度明確に意識し、それに合わせた誘導をすること
   2. 解き方が分かった人が実際に解くのに掛かる時間の見積もりができること
      1. 想定した解き方で解くのに\(10^100\)日掛かる、というのではダメ
      2. 時間は計算機をフルに動かせば\(1\)日で解けそうでもメモリが\(1\)TB必要、というのでは非現実的
3. 解いた人の回答が正解か否かを判定する方法があること
   1. 詳しい人に確かめてもらう、という方法が通用する簡単な問題ならここは自動的
   2. そうでない場合は、提供する類題のうち少なくとも１問は解答や解説があることが望ましい
   3. もし可能であれば、自動で採点できるシステムがあるととても嬉しい
4. 色々な人が問題にアクセスできること
   1. どうせなら多くの人に解いてもらえた方が意欲も上がるし、好きな概念の布教にもなる
   2. 問題に不備があった場合にフィードバックを貰えれば、自分の間違いを正せる
   3. 想定していなかった素晴らしい解法に出会えれば、自分も新たに学ぶことができる

などです。

特に1や2-1を意識して問題を作成すれば、その問題を解くために必要な知識や議論の流れを自分でまとめ直すことができ、2-2を意識することで複数の解き方の長所や短所への理解が深まります。

今回yukicoderをおすすめする上で大事な要素は3-2や3-3と4で、yukicoderを使うことでオンラインで自動採点できる問題を解説つきで広く共有することが可能になります。

yukicoderとは？

yukicoderは競技プログラミングの作問と回答を行うことができるサイトです。競技プログラミングとは、プログラミングを用いて数学の問題を解く競技です。

基礎論においては様々な手続きの計算可能性が知られており、ものによっては計算可能性を証明すること自体が非自明な問題だったりします。

そのため基礎論は競技プログラミングと相性がよく、プログラミングで解ける問題を作成することにより基礎論で学んだ計算可能な手続きを厳密に理解していることを確認することができます。

また証明論ではしばしばテトレーションオーダーの計算量が要求される手続きもあり、どのような手続きをどのような問題設定で問うか、も考えることで各手続きへの理解も深まります。

そこで数ある競技プログラミングのサイトのうち、yukicoderは問題を解くだけでなく作問を自由に行えるのでおすすめです。登録も不要で、twitterなりgithubなりと連携をすれば問題を作成したり回答を提出したりすることができます。

問題例

いくら基礎論が競技プログラミングと相性が良いと主張しても、実際に手軽に問題が作れるのかどうか気になると思いますので例を挙げます。

2022/12/20時点でyukicoderで自分で作問した問題は56件で、そのうち基礎論に直接関係するものが12問、そのうち現時点で公開しているものが4問です。基礎論に直接関係する問題以外にも、基礎的な集合の問題やペアノ算術で数列を定式化する際に重要な中国剰余定理に関する問題など、基礎論に間接的に関係する問題もいくつか作成しています。

No.2090 否定論理積と充足可能性

問題へのリンクはこちらです。

問題文要約

ここでは \(P\) に非負整数である添字を付けた記号で命題変数を表します。例えば \(P_0\) や \(P_3\) は命題変数ですが、\(P\) や \(Q\) や \(Q_0\) は命題変数ではありません。

\((\mid)\) はシェファーの棒記号であり、否定論理積（NAND）を表します。

非負整数 \(A_0, A_1, A_2, A_3, A_4, A_5\) を入力すると命題論理の論理式 \begin{eqnarray*} (((P_{A_0} \mid P_{A_1}) \mid P_{A_2}) \mid ((P_{A_3} \mid P_{A_4}) \mid P_{A_5})) \end{eqnarray*} が充足可能か否かを出力するソースコードを提出してください。

以下、命題論理について詳しくない人に向けた用語の補足説明をします。（クリックで開く）

命題変数の真理値割り当てとは、大雑把には各非負整数 \(i\) に対し \(P_i\) が真であるか偽であるかを決める対応のことです。

より形式的には非負整数全体の集合 \(\mathbb{N}\) から\(\{0,1\}\) への写像のことですが、その定式化に納得できる人はこの補足が不要なので大雑把な説明に留めます。

命題論理の論理式 \(F\) が充足可能であるとは、\(F\) が真になるような命題変数の真理値割り当てが存在するということです。例えば論理式 \begin{eqnarray*} P_0 \land (P_1 \lor P_0) \end{eqnarray*} は全ての命題変数（といっても \(P_2\) 以降は関係ありませんが）を真とすると論理式全体が真となるので、充足可能です。一方で論理式 \begin{eqnarray*} P_0 \land (\neg P_0) \end{eqnarray*} は充足可能ではありません。実際、\(P_0\) が真である場合は \(\land\) の右側にある部分論理式 \(\neg P_0\) が偽となってしまうため論理式全体が偽となり、\(P_0\) が偽である場合も \(\land\) の左側にある部分論理式 \(P_0\) が偽となってしまうので論理式全体が偽となり、どう命題変数の真理値割り当てを取っても論理式全体が偽となってしまいます。

このように、問題文には用語を知らない人向けに補足説明を書くことも出来ますし推奨されています。

備考

2022/12/20時点での挑戦者は102人で、うち正解者は101人（正答率 \(99.02\%\)）です。何度不正解を出しても再提出できますので、プログラミングが分かる人は是非挑戦してみてください。

以下ネタバレを含むので、クリックしたら開くようにしてあります。

充足可能性は意味論の概念であり、真理値割当を全探索するのがもっとも自然な解法ですね。しかし基礎論に詳しい皆さんは、意味論と統語論の関係にも詳しいと思います。今回は統語論的に同値変形をしてしまって否定がトートロジーであるか否かを判定する方法で解くことも可能で、その場合は真理値割当の全探索より遥かに高速に計算を実行することが出来ます。

No.2118 遺伝的有限集合の数え上げ

問題へのリンクはこちらです。

問題文要約

各非負整数\(n\)に対し集合 \(S_n\) を次の条件を満たす集合 \(T\) 全体の集合と定めます：

• 以下の \(3\) 条件を全て満たす 非負整数 \(i\) が存在する：
  • \(2^i \leq n\) である。（従って \(n\) の二進法表記における \(2^i\) の位が意味を持つ）
  • \(n\) の二進法表記における \(2^i\) の位（\(1+i\) 桁目）が \(1\) である。
  • \(T = S_i\) である。

非負整数\(N\)を入力すると集合 \(S_N\) を出力するソースコードを提出してください。ただし集合を出力する際は以下の形式に従ってください：

1. まず、半角左波カッコ{を出力する。
2. 次に、その全ての要素を好きな順に半角コンマ,区切りで重複なく出力する。
3. その後、半角右波カッコ}を出力する。

例えば空集合 \(\{\}\) を出力するには、まず{を出力し、次に要素はないので何も出力せず、その後}を出力することになります。従って結局{}を出力することになります。

備考

2022/12/20時点での挑戦者は84人で、うち正解者は79人（正答率 \(94.05\%\)）です。

以下ネタバレを含むので、クリックしたら開くようにしてあります。

\(\textrsf{ZFC} - \textsf{Infty}\) のモデルでおなじみの、遺伝的有限集合を題材にした問題です。

問題文そのものには遺伝的有限集合という用語が現れませんが、問題文で与えられた \(S_n\) はペアノ算術で遺伝的有限集合のグラフを形式化する時に使われる写像そのものです。

正解となるソースコードを書くためには \(S_n\) の再帰的定義を正しく理解して実装できる必要があります。

また提出したソースコードが正解か否かは自動で判定できるようにしていますが、自分でも証明したい場合は（出力に「重複なく」という制約があることから）２つの遺伝的有限集合が一致する条件（外延性公理）をその出力の統語的情報に翻訳して理解する必要があります。そこでは数学的帰納法を使って厳密に議論する必要があるので、ただ提出するだけでなく自分で証明をする訓練にもお使いいただけます。

No.2121 帰属関係と充足可能性

問題へのリンクはこちらです。

問題文要約

ここでは \(x\) に非負整数である添字を付けた記号で集合変数を表すことにします。

例えば \(x_0\) や \(x_3\) は集合変数ですが、 \(x\) や \(y\) や \(y_0\) は集合変数ではありません。

まずは記法の確認です。各非負整数 \(n\) に対し、有限集合 \(V_n\) は以下のように再帰的に定義されます：

• \(n = 0\) ならば、\(V_n\) は空集合である。
• \(n > 0\) ならば、\(V_n\) は \(V_{n-1}\) の冪集合、つまり \(V_{n-1}\) の部分集合全体の集合である。

例えば定義から \(V_0 = \{\}\) となります。\(\{\}\) の部分集合は \(\{\}\) 自身に限るので、\(V_1\) は \(\{\}\) のみを要素に持つ集合 \(\{\{\}\}\) となります。\(\{\{\}\}\) の部分集合は \(\{\}\) と \(\{\{\}\}\) 自身の２つがあるので、\(V_2\) は \(\{\}\) と \(\{\{\}\}\) のみを要素に持つ集合 \(\{\{\},\{\{\}\}\}\) となります。

\(5\) 以下の非負整数 \(N\) と \(2\) 以下の非負整数 \(A_0, A_1, A_2, A_3, A_4, A_5\) を入力すると集合論の論理式 \begin{eqnarray*} ((((\forall x_3((x_3 \in x_{A_0}) \to (x_3 \in x_{A_1}))) \land (x_{A_1} \in x_{A_2})) \land (x_{A_3} \in x_{A_2})) \land (x_{A_4} \in x_{A_2})) \land (x_{A_5} \in x_{A_0}) \end{eqnarray*} が \(V_N\) で充足可能か否か、つまり論理式 \begin{eqnarray*} ((((\forall x_3 \in V_N((x_3 \in m_{A_0}) \to (x_3 \in m_{A_1}))) \land (m_{A_1} \in m_{A_2})) \land (m_{A_3} \in m_{A_2})) \land (m_{A_4} \in m_{A_2})) \land (m_{A_5} \in m_{A_0}) \end{eqnarray*} が真であるような \(V_N\) の要素 \(m_0, m_1, m_2\) の組み合わせ \((m_0,m_1,m_2)\) が存在するか否かを出力するソースコードを提出してください。

ただし \(m_3\) と \(m_{A_3}\) を混同しないように気をつけてください。

以下、\(\forall\) について詳しくない人向けの解説をします。（クリックで開く）

何らかの論理式 \(P\) が与えられた時、論理式 \(\forall x_3(P)\) は日本語では

• 任意の \(x_3\) に対し、\(P\) である。
• いかなる \(x_3\) に対しても、\(P\) である。

などのように読まれます。つまりどのように \(x_3\) を選んだとしても \(P\) が常に成り立つということですね。例えば \(\forall x_3(x_3 = x_3)\) は

• 任意の \(x_3\) に対し、\(x_3 = x_3\) である。
• いかなる \(x_3\) に対しても、\(x_3 = x_3\) である。

などのように読まれます。 更に何らかの集合 \(M\) が与えられた時、\(x_3\) の動く範囲を \(M\) に制限したい場合は、\(\forall x_3 \in M(P)\) のように書きます。これは日本語だと

• \(M\) の任意の要素 \(x_3\) に対し、\(P\) である。
• \(M\) に属す任意の \(x_3\) に対し、\(P\) である。
• \(M\) のいかなる要素 \(x_3\) に対しても、\(P\) である。
• \(M\) に属すいかなる \(x_3\) に対しても、\(P\) である。

などのように読まれます。なお \(\forall x_3 \in M(P)\) という表記は実際には \(\forall x_3(x_3 \in M \to P)\) の糖衣構文ですので、その定義に則って

• 任意の要素 \(x_3\) に対し、\(x \in M\) ならば \(P\) である。
• いかなる \(x_3\) に対しても、\(x \in M\) ならば \(P\) である。

などのように読んでも構いません。今回は \(M\) として \(V_N\) を考えており、\(\forall x_3 \in V_N(P)\) という形の論理式を扱っています。

備考

2022/12/20時点での挑戦者は29人で、うち正解者は29人（正答率 \(100.00\%\)）です。やや読解難易度の高い問題であるため挑戦者が少ないですが、その分正答率は高いですね。

以下ネタバレを含むので、クリックしたら開くようにしてあります。

各種集合論のモデルでおなじみの、フォン・ノイマン階層を題材にした問題です。

問題文そのものにはフォン・ノイマン階層という用語が現れませんが、問題文で与えられた \(V_n\) はフォン・ノイマン階層そのものです。

正解となるソースコードを書くためには \(V_n\) の再帰的定義を正しく理解して実装できる必要がありますが、集合の集合の集合の…と入れ子になった集合を実装するのはプログラミングに慣れていなければあまり簡単ではありません。しかも、単純に充足可能性を判定しようとして集合変数の付値割当を全探索すると、これはテトレーションオーダーの計算量となってしまい実はうまくいきません。きちんと論理式の意味を理解して、効率的な探索を実行する必要があります。

もちろん今回も、意味論ではなく統語論からのアプローチで解くことが可能です。論理式を統語的に同値変形をしてしまい、否定が証明可能であるか否かを判定すればいいですね。こちらは意味論的な解法と違ってとても高速な実行速度となります。

No.2168 停止性問題（双頭ヒドラゲーム）

問題へのリンクはこちらです。

問題文要約

この問題は要約しても曖昧であまり役に立たないと思いますので、厳密な問題文を上のリンクからご確認ください。

備考

yukicoderのアドベントカレンダーコンテスト2022に投稿し2022/12/20/0:00に公開したばかりなので、2022/12/21/00:00時点での挑戦者は8人で、うち正解者は4人（正答率 \(50.00\%\)）です。なお挑戦者のうち1人は自分で、もう1人は後述する「tester」という役割の人なので、実質的な挑戦者は6人、うち正解者は2人（正答率 \(33.33\%\)）と考えてください。これから多くの方々が挑戦してくだされば幸いです。

以下ネタバレを含むので、クリックしたら開くようにしてあります。

証明論でおなじみの、ヒドラゲームの亜種を題材にした問題です。証明論では無限集合に関する複雑な命題も有限な文字列などに関するシンプルな問題に翻訳することが多く、ヒドラゲームもそのような問題の１つですね。今回も無限集合の命題を翻訳したヒドラゲームになっています。解説にも証明を詳しく書いたので、集合論に自信のある人は是非挑戦してみてください。

作問から公開まで

ところで先程、

yukicoderで自分で作問した問題は56件で、そのうち基礎論に直接関係するものが12問、そのうち現時点で公開しているものが4問です。

と述べました。作問をした問題を全て公開しているわけではないのにはきちんと理由がありまして、それを最後に説明して終わろうと思います。

まずyukicoderは誰でも自由に作問ができるサイトなので、当然あまり作問に慣れていない人が問題を作成することもあります。また僕自身もそうですが、数学の作問自体には慣れていても競技プログラミングの人たちを対象にした作問（特に、競技プログラミングであまり前提知識とされない用語を断りなく用いないこと）には慣れていないという人も多いと思います。

また、第三者のチェックが入っていない問題は不備があったり自動採点に間違いがあったり、解説が間違っていたりすることもあると思います。

そういった懸念事項を解決するために、yukicoderでは作問時に基本的には第三者（testerと呼びます）に問題のチェックをしてもらうことが要請されています。つまり問題のチェックを通って初めて、その問題（および自動採点と解説）が公開されるわけです。

やはりtester作業より作問作業のほうが人気であるため、twitterでちょくちょくtester不足に言及している人がいるようです。というわけで、基礎論関係の問題を12個作ってtesterさんを募集したとは言っても、実際にtesterさんが見つかったのが今のところ4問であった、というのが作問数と公開問題数の差の答えです。

僕も積極的にtesterを行っていますが、もし皆さんがyukicoderで作問を行うようになった際はぜひ他の方々の作問のtesterも積極的に引き受けてくださると幸いです。

この数学基礎論アドベントカレンダー参加者の中からもし何人か基礎論の作問者が出てくださってお互いにtesterを引き受けられるようになれば、基礎論の問題をどんどん公開できるようになって世界中の基礎論erが幸せになれると思うので、この機会にyukicoderの活用をご一考ください！

ちなみに基礎論で作問をした場合、twitterで僕に声をかけてくださればもちろん（あまりに難易度が高すぎて僕の手におえなさそうなものでなければ）testerは引き受けると思いますので、testerを見つけられない場合も難易度をご連絡の上で遠慮なくご相談ください。基礎論以外でももちろん構いませんが、競技プログラミングそのものはそこまで知識がないので、競技プログラミングの知識をあまり仮定しない数学の問題でなるべくよろしくお願いいたします。

それでは、yukicoderを用いた基礎論演習問題作成に興味のある人は、公式のヘルプページをご確認ください。

作問した問題はただ１問だけで公開するだけでなく、何問かまとめて（作問者は複数人でも可）特定の時間に公開をする「コンテスト形式」を選択することも可能なので、いつか皆さんの「基礎論コンテスト」に参加できる日を楽しみにしております。