SATySFi インストールチャレンジ in Windows Subsystem for Linux

Windows Subsystem for Linux に SATySFi をインストールをする機会がここ数週間の間になぜか複数回あった．この記事はそれらの経験からわかった Windows Subsystem for Linux に SATySFi をインストールをする方法をまとめたものである．

たぶんこれが一番早いと思います*1．

問題の背景

SATySFi とは組版処理システムの一種で，諏訪敬之しによって，IPA の未踏IT人材発掘・育成事業(2017)の支援の下に開発された．SATySFiは静的型付けにより，組版処理の前段階での詳細でわかりやすいエラー報告を実現しているらしい[要出典]。SATySFi はその高性能さと並んで，インストールがパソコン初心者には難しいことでも知られている[要出典]．

Windows Subsystem for Linux (以下 WSL )とは Windows の中でサーバー版 Linux (に限りなく近いもの)を動かそうという意欲的なシステムで，Micrsoft vs Linux という冷戦の雪解けの象徴である[とても要出典]．ディストリビューションについては Ubuntu や Debian など複数与えられている．

この記事では WSLを使えるようにしてから，SATySFi をインストールするまでの最短経路(たぶん)を紹介する．

Windows Subsystem for Linux を使えるようにする．

WSL を使えるようにする．この工程は大きく分けて２つある．

1. WSL を使用できるように設定を変える．
2. ディストリビューションを決める．

これは基本的には公式ドキュメント Windows Subsystem for Linux (WSL) を Windows 10 にインストールする | Microsoft Docs の「手動インストール」にしたがえば何とかなる*2．

しかし，ここでは公式ドキュメントとは違い GUI で済ませられるところは GUI で済ませる方針で行く*3．

WSL を使用できるように設定を変える．

Windows の機能の有効化または無効化 というところから WSL を使用できるように設定を変えることができる．
方法は

1. 「設定」をスタートメニューなどから開く．
2. Windows の機能の有効化または無効化 を検索窓から検索する．
3. 立ち上がったウィンドウのなかのチェックボックスから「Linux 用 Windows サブシステム」にチェックを入れる．もし，この時点でそもそもそのような項目が見つからなかった場合，Windows のバージョンが足りていない可能性が高い*4．
4. 再起動する．

ディストリビューションを決めてダウンロードする．

ディストリビューションは Microsoft Store から好きなディストリビューションをダウンロードする．

私が試したのは Ubuntu と Debian のみなので，この記事の方法に従う場合は，そのどちらかを選ぶのを推奨する．

ディストリビューションのインストールが完了すると，スタートメニューにそのディストリビューションのアイコンが現れる．そのアイコンをクリックすれば，WSL が立ち上がる．初回はユーザー名とパスワードを求められるので，適当に入力してしまおう．

SATySFi インストールチャレンジ in Windows Subsystem for Linux

WSL が使えるようになったら，いよいよ SATySFi インストールチャレンジの開始である．
本来は WSL 2 を使うことを推奨されているが，WSL 1 でも動くので，この記事では WSL 1 で動かすことを考える．WSL 2 から Windows 側のファイルを編集することが非推奨とされていることを考えると，WSL 1 で動かせる限りは WSL 1 で動かしたほうが良いという発想である．とはいえ，おそらく WSL 2 でもほぼ同じ方法（一か所だけ異なる）でインストールができると考えられるので，WSL 2 を使う人にとって，この記事が全く役に立たないことはないはずである．

以下では，Ubuntu と Debian をインストールしたとして話を進める．

SATySFi のインストールに必要なツールのダウンロード

まず，SATySFi のインストールに必要なツールのダウンロードを行う．次のコマンドを入力する．

sudo apt update
sudo apt install build-essential git m4 unzip curl  make wget opam 

最初のコマンドの実行時にパスワードの入力を求められるはずなので，WSL を最初に立ち上げたときに決めたパスワードを入力する．

公式ドキュメント GitHub - gfngfn/SATySFi: A statically-typed, functional typesetting system だと Opam を違う方法でインストールしているが，現在の Ubuntu や Debian では apt から手に入れたほうが早いのでそうする．

Opam を設定する（鬼門）

ここが最大の鬼門である．

Opam というのは OCaml のパッケージマネージャである．SATySFi は大部分*5 が OCaml によって書かれているために Opam が必要である．

しかし，WSL 勢にはこの Opam の設定が難しい．だって，公式ドキュメント通りにやってもうまくいかないのだもの．しかもエラーを見てもいまいちなぜだめなのかよくわからない．

どうも原因は WSL 1 では bwrap によるサンドボックスが上手く動かないことにあるらしい*6．WSL ２ では解決した問題らしいが，ここではあくまでも WSL 1 で頑張ることにする．

先に述べた理由から，Opam のインストールが終わったらその初期設定を

opam init --comp 4.10.0 --disable-sandboxing

というコマンドによって行う．最後のオプションはサンドボックスを切るためのオプションである*7．SATySFi は 2021 年 2 月 4 日現在，OCaml 4.10.0 を使うことを求められているので，--comp 4.10.0 をつける（これを外すと古いバージョンがインストールされてしまうので必須）．

このコマンドの実行中いくつか入力を求められるがよくわからない場合はすべて y を選択すればよい．

その後

eval $(opam env)

opam repository add satysfi-external https://github.com/gfngfn/satysfi-external-repo.git
opam update

を実行して，SATySFi をインストールできる状態にする．

Opam の設定がうまくいかなかったら

この時点で，

ocaml --version

を実行して

The OCaml toplevel, version 4.10.0

と表示されなかったら，どこかでミスをしている．

この場合はあまり良い方法ではないと思うが，

rm -rf ~/.opam

して opam 関連の諸々を初期化し，この節の最初からやり直しである．

この方法だと，opam 関連のファイルごとすべて吹っ飛ばしているので，他のことに opam を使っている人は使えない方法であるが，この記事に救いを求める人にそういった人はいないと考えられるので気にしないことにする*8．

SATySFi をインストールする

ここから先は一か所を除いて，公式ドキュメント通りに進めれば，上手くいく．

まず，

git clone https://github.com/gfngfn/SATySFi.git

または

git clone git@github.com:gfngfn/SATySFi.git

をして，GitHub に公開されている SATySFi のレポジトリをクローンする．Git を初めて使う人は前者を使えばよい*9．

クローンしてきた SATySFi というディレクトリに

cd SATySFi

して入る．そして，

opam pin add satysfi .
opam install satysfi

をすると，SATySFi が build される．

ここまでで，SATySFi はインストールされているわけだが，使い始める前に

./download-fonts.sh
sudo ./install-libs.sh

をしてほしいそうなのでそうする．ただし，後者のスクリプトは sudo 権限がないと触れないディレクトリを触るので，公式ドキュメントには書いていないが，sudo 権限で実行する*10．

demo が動くか確認する．

ここまで来たらほぼ勝利も同然であるが，勝利したことの確認のため demo を動かしてみる．

cd demo
make
ls 

をして， demo.pdf が生成されていることを確認できれば勝利確定である．

まとめ

WSL 1 勢が気を付けなければならないのは

• opam init するとき， --comp 4.10.0 --disable-sandboxing というオプションを忘れないこと．

である．SATySFi インストールチャレンジ成功者が一人でも多く増えることを望む．

参考にしたもの

1. Windows Subsystem for Linux (WSL) を Windows 10 にインストールする | Microsoft Docs
2. SATySFi の公式ドキュメント GitHub - gfngfn/SATySFi: A statically-typed, functional typesetting system
3. *nix 向け SATySFi インストールバトル手引き 2020年10月版 - Qiita

*1:使うディストリビューションは Ubuntu と Debian を仮定する．

*2:公式ドキュメントが分かりにくいのはある．

*3:画面のスクリーンショットは撮るの忘れた．すいません．

*4:Windows 10 のダウンロード から Update Assistant をダウンロードし，最新版の Windows を手に入れよう．

*5:というか GitHub の言語の割合を見る限り全部 OCaml と考えられる．

*6:ごめんなさい．ここはわからないまましゃべっている．詳しいことは *nix 向け SATySFi インストールバトル手引き 2020年10月版 - Qiita や build ocaml-base-compiler fails on versions 4.02-4.08 (`opam switch create . 4.06.1`) · Issue #12050 · ocaml/opam-repository · GitHub を参照してほしい．

*7: WSL 2 を使っている人にはおそらく必要のないオプション．

*8:居たらごめんなさい．

*9:最近は http を使って Git Hub にアクセスすることは非推奨らしいが

*10:こっちはエラーをよく読むとエラーの理由がすぐわかるので，比較的解決しやすい．

Windows Subsystem for Linux で Texdoc を使いたいというおはなし

Windows Subsystem for Linux (以下WSL)でTexdoc を使うための方法についての記事です．
元々はLaTeX 初心者が知るべきただ一つのコマンド - Sokratesさんの備忘録ないし雑記帳という記事のおまけにしていたのですが，分量的に分けたほうが良いと判断したので，別記事にします．

2022/2/26 追記： Windows 11 ビルド 22000 以上を使っている場合，GUI サポートが始まったため，この記事の前半の方法を使わなくても，WSL から Texdoc によってドキュメントを読めるようになりました．詳しいことは記事の最後に回しますが，「どうしても SumatraPDF などの Windows の pdf viewer で Texdoc のドキュメントを読みたい」などの事情がない限りは GUI サポートを利用した方が楽だと思います．追記終わり．

1. WSL で Texdoc を使えないんだけどォォォォォォ！！！

WSL ユーザーという原罪のため，Texdoc が使えないかわいそうな皆さん．こんばんは．私もそんな人間の一人です．私かわいそう．

WSL でたとえば，

$ texdoc texdoc

を実行すると

texdoc warning: DISPLAY is not set; your viewer will likely have problems.
texdoc warning: Try --list to list results instead of displaying them.

などと表示されブチ切れる羽目になります．これは残念ながら現状 WSL に対して，GUI はサポートされていないからだと考えられます（2022/2/26 追記： Windows 11 ビルド 22000 以上を使っている場合，GUI サポートがあります．そのため，この記事の方法を使わなくても，WSL から Texdoc によってドキュメントを読めるようになりました．追記終わり．）*1．そのため，WSL 側から Windows の pdf viewer などを呼び出すように設定の変更をするしかありません*2．「おっ，なら設定ファイルを書き直せばいいんだな」と思われるかもしれませんが，ある事情から少し工夫をしないと，WSL の Texdoc と Windows の pdf viewer を連携させることができません．ここでは，その方法を紹介します．
基本的には下記のリンク先の方法と同じですが，一部私の工夫が入っています．
"DISPLAY is not set; your viewer will likely have problems" on Windows Subsystem for Linux · Issue #59 · TeX-Live/texdoc · GitHub

私程度が読むようなドキュメントは pdf であることが多いため，pdf を読むための方法しか紹介しませんが，ご了承ください．ただし，ここに書いてあるようなスクリプトをファイルの種類ごとに書いて，viewer として設定すればうまくいくとは思います*3．

おそらく，この方法はディストリビューションなどに依存しないと考えられますが，動作確認は

• エディション Windows 10 Home
• バージョン 20H2
• OS ビルド 19042.685

の中で WSL 2 の ubuntu-20.04 で行っています．
また，TeX Live の バージョンは 2019.20200218-1 です．

2. 方法の紹介の前の注意

あらかじめ申し上げますが，ここで紹介する方法で Texdoc から pdf ファイルを読めるようになっても Texdoc からの

texdoc warning: DISPLAY is not set; your viewer will likely have problems.
texdoc warning: Try --list to list results instead of displaying them.

というメッセージはナント消えません！バカな！そこをご了承の上で下記の方法を試してみてください．
また，わたしが普段使う pdf viewer が Sumatra PDF なので，例として，SumatraPDF を呼び出すように書いています．それ以外の pdf viewer を使いたい人々は適時そこを読み替えてお読みください．

3. WSL から Texdoc を呼び出すそんなに冴えているわけでもないやり方

ステップ 1.

pdf viewer を呼び出すための bash スクリプト*4を書きます（なぜそんな面倒なことをするのかは後で補足します）．
次のような bashスクリプトを openpdf という名前*5で WSL の path が通っている場所に置きます*6．
GitHub - Sokratesnil/wsl-scripts に同じスクリプトを置いてあるので，そちらからダウンロードしても構いません．

#!/bin/sh
for file in "$@"
do
  pathinwsl=`realpath $file`
  pathinwindows=`wslpath -w $pathinwsl`
  SumatraPDF.exe "$pathinwindows" &
done

この bash スクリプトの SumatraPDF.exe を他の好きな pdf viewer の実行ファイルに置き換えれば，その pdf viewer で texdoc が探してきた pdf ドキュメントを読めるはずです．たぶん． 2021/1/6 追記．実際，chrome.exe に置き換えることで Google Chrome で pdf の閲覧ができました．

openpdf を作ったら

$ chmod +x openpdf

とコマンドを実行して，実行者権限を付与してください．

ステップ 2.

Texdoc の設定ファイルを書きます．
Texdoc の設定ファイルを置く場所は

$ texdoc -f

を実行すると分かります．わたしの場合は

/usr/share/texlive/texmf-dist/scripts/texdoc/texdoclib.tlu 3.0
Configuration files are:
    active      /usr/share/texlive/texmf-dist/texdoc/texdoc.cnf
Recommended file(s) for personal settings:
    /home/xxx/texmf/texdoc/texdoc.cnf

などと表示されたので，/home/xxx/texmf/texdoc/ に設定ファイル texdoc.cnf を用意すれば良いことが分かります．もし，存在しないディレクトリなどが途中にあった場合は適時 mkdir texmf などを実行して，ディレクトリを作ってください．

さて，texdoc.cnf に次の一行を書きます．

viewer_pdf=openpdf

これは Texdoc の pdf viewer を指定しています．

ステップ 3. 最後に

$ texdoc texdoc

を実行してみて，エラーが出つつも pdf viewer が立ち上がり，Texdoc の公式ドキュメントを読むことができれば成功です．他のドキュメントも立ち上げてみましょう．

4.なぜこんな回りくどい方法を......

ここで紹介する方法は一見すると回り道に見えるかもしれません．普通に考えると，

viewer_pdf=SumatraPDF.exe

とすればうまくいきそうなのですが，読みたいドキュメントまでの path の指定が wsl と texdoc で食い違いが発生するようで，うまくドキュメントを開くことができません（かなしい）． openpdf はその問題を解決するために path の変換をしてから pdf viewer に pdf ファイルを渡すようにしています．

"DISPLAY is not set; your viewer will likely have problems" on Windows Subsystem for Linux · Issue #59 · TeX-Live/texdoc · GitHub の方法（以下元ネタ）との違いと私の方法の違いも述べておきます（以下の二段落は興味のある方だけお読みください）．
元ネタと私の方法は wsl と texdoc の path の食い違いを補正するという点は共通しています．問題は呼び出すアプリの違いです．元ネタの方法だと powershell.exe を呼び出すようにしています．しかし，これでは動作が重くなります．powershell.exe という重いソフトウェアを呼び出さない分によってわずかですが，動作が軽くなっています．
一方，元ネタのスクリプトだと，texdoc に呼び出されるファイルの拡張子に Windows 側で関連付けられているソフトウェアを呼び出すようになっているという利点があります．そのため，pdf 以外のドキュメントにもバリバリ目を通したい方は，もしかすると元のスクリプトを使ったほうが良いのかもしれません．

5.最後に

 このバグ(?)は WSL の GUI サポートが開始されれば解消されると予想されるため，texdoc 側で対応する予定はまったくないそうです（以下のリンクを参照）．しょうがないね．
https://github.com/TeX-Live/texdoc/issues/59?s=09#issuecomment-720107960

2022/2/26 追記： Windows 11 ビルド 22000 以上を使っている場合，GUI サポートが始まったため，この記事の方法を使わなくても，WSL から Texdoc によってドキュメントを読めるようになりました．「どうしても SumatraPDF などの Windows の pdf viewer で Texdoc のドキュメントを読みたい」などの事情がない限りは GUI サポートを利用した方が楽だと思います．追記終わり．

A. GUI サポートを得た WSL で Texdoc を使う方法（2022/2/26 追記）

Windows 11 ビルド 22000 以上を使っている場合，GUI サポートが始まったため，もっと簡単に Texdoc を利用できるようになりました．ここではその場合の WSL および Texdoc の設定の仕方を軽く説明します．

注意：WSL で使えないような Sumatra PDF などの pdf viewer をどうしても使いたい場合や WSL1 を使いたい場合などは，結局上の GUI サポートに頼らない設定をする必要があります．

WSL の GUI サポートを使う方法について

前提として，Windows 11 ビルド 22000 以上であることが必要です．また，使っているシステムに対応する vGPU 用のドライバーをインストールする必要があります．詳しいことは公式ドキュメントWSL で Linux GUI アプリを実行する | Microsoft Docsの「前提条件」を読んでください．

pdf viewer をインストールする．

WSL のGUI サポートを使えるようになったら，適当な pdf viewer を WSL に入れてください．たとえば，ubuntu ディストリビューションで evince をインストールする場合は，

$sudo apt update
$sudo apt upgrade
$sudo apt install evince

とすれば良いです（debian と Kali linux なら同じコマンドでいけるはず）．

pdf viewer を設定する

pdf viewer をインストールできたら， Texdoc の設定ファイルを書きます．Texdoc の設定ファイルを置く場所は

$ texdoc -f

を実行すると分かります．わたしの場合は

/usr/share/texlive/texmf-dist/scripts/texdoc/texdoclib.tlu 3.0
Configuration files are:
    active      /usr/share/texlive/texmf-dist/texdoc/texdoc.cnf
Recommended file(s) for personal settings:
    /home/xxx/texmf/texdoc/texdoc.cnf

などと表示されたので，/home/xxx/texmf/texdoc/ に設定ファイル texdoc.cnf を用意すれば良いことが分かります．もし，存在しないディレクトリなどが途中にあった場合は適時 mkdir texmf などを実行して，ディレクトリを作ってください．

さて，たとえば，evince で texdoc のドキュメントを読むようにしたい場合は texdoc.cnf に次の一行を書きます．

viewer_pdf=evince

使いたい pdf viewer が他にあるならば，"evince"の部分をその pdf viewer を呼び出すコマンドに置き換えてください．

追記終わり．

*1:WSL の GUI については，サードパーティ製のものが存在するそうですが，私は使ったことありません．もし，そういう製品を使ったらここに書いてあるような問題は起こらないのかもしれないですが，どうなんですかね．よくわからない．2022/2/26 追記： Windows 11 ビルド 22000 以上を使っている場合，GUI サポートがあります．追記終わり．

*2:または，WSL から Texdoc を立ち上げることを諦めて，Windows 側にTeX Live を入れるかです．昔の私のように（わたしかわいそう）．

*3:試してないですが．

*4:実は以前あげていたものと少し変えています．WSL の Texdoc を使う分には以前のもので十分なのですが，たとえば，以前のバージョンの openpdf で Windows 下の pdf ファイルを開こうとすると，開くことができません．これは，以前のバージョンでは SumatraPDF.exe に渡す path の変換を WSL に任せてしまっているためです．汎用性を上げるために SumatraPDF.exe に渡す path を明示的に変換するように変更しました．

*5:名前は他のものでも良いですが，わかりやすい名前にした方が良いと考えます．

*6:ちなみに，動作確認の際は~/bin/openpdf としました．

【備忘録】数学英語文書まとめ

この記事は さいえんSlack Advent Calendar 2020 - Adventar の 25 日目（最終日）の記事です．24 日目は Tomoki UDA さんの担当でした．
さいえんSlackは Slack を中心に活動している科学に興味がある人のためのゆる〜いコミュニティです．詳しいことは以下のリンクを参照してください．
scienslack.github.io

この記事では英語で数学についての文章を書くための How to 文書で役に立ったり有名だったりするものを備忘録を兼ねて紹介する記事です．基本的には修論や博論，投稿論文などを書く際に参考になるものを紹介していきます．参考になれば幸いです．

1. 英語一般

英語一般についての文書で文章を書くときに参考になったものを紹介します．

[1.1.] 徹底例解ロイヤル英文法　改訂新版

徹底例解ロイヤル英文法　改訂新版

高校生にもおなじみの文法書ですね．すこしでも怪しいところがあるたびに開いています．最近，持ち歩くのがしんどくて，電子版を紙版とは別に購入しました．これは正解で，文字列検索できるようになって効率が上がりました．

[1.2.] 【DVD-ROM付】オックスフォード現代英英辞典 第9版

【DVD-ROM付】オックスフォード現代英英辞典 第9版

知り合いに誕生日プレゼントをねだったら買ってもらえました．定評のある英英辞典です．とても役に立っています．語法が怪しかったらまずこの辞書でそのような語法があるかを調べてから使っています（念の為，Google 検索もかけますが）．

2. 科学英語一般

この節では科学英語一般についての How to 本を紹介します．科学英語独特の慣習や科学英語だと許される表現などがあるので，上とは別で使っています．

[2.1.] English for Writing Research Papers (English for Academic Research)

English for Writing Research Papers (English for Academic Research)

最近新版が出たようで，表紙のデザインが変わっていてびっくりしました．私は下のようなバージョンを持っています．

English for Writing Research Papers (English Edition)

また，日本語訳も出ていてそちらも持っています．現題に比べるとタイトルがちょっとアレな感じなのはご愛嬌．

ネイティブが教える 日本人研究者のための論文の書き方・アクセプト術 (KS科学一般書)

医学系の論文からの引用が多いような気がしますが，論文全体の構造などについてはこれがとても参考になりました．最後に科学論文で使える表現集がまとまっているのも使いやすいです．

[2.1.1.]English for Academic Research: Grammar, Usage and Style: Usage, Style, and Grammar

English for Academic Research: Grammar, Usage and Style: Usage, Style, and Grammar

上の姉妹編で主に文法や語法にフォーカスが当てられています．語法に迷ったときなどにたまに参照します．

[2.2.] 理科系のための英文作法―文章をなめらかにつなぐ四つの法則 (中公新書)

理科系のための英文作法―文章をなめらかにつなぐ四つの法則 (中公新書)

いろんなところで取り上げられて有名になっている本と若干タイトルが似ていますが，違う本です．こちらも名著で，特に第一章は接続詞に悩んだときにとても参考になりました．ただ，「"Thus" を頻繁に使うべきではない」など数学英語とは相容れない部分があることに注意して読まなければなりません．

[2.3.] 英語論文 すぐに使える表現集

英語論文 すぐに使える表現集

たまに参照します．日本人が書いているので，「これ英語だとどう表現するんだ？」となったときに助かります．

[2.4.] 理系のための英語論文執筆ガイド―ネイティブとの発想のズレはどこか? (ブルーバックス)

理系のための英語論文執筆ガイド―ネイティブとの発想のズレはどこか? (ブルーバックス)

たまに目を通すと勉強になります．
[2.4.1.] 間違いだらけの英語科学論文　失敗例から学ぶ正しい英文表現 (ブルーバックス)

間違いだらけの英語科学論文　失敗例から学ぶ正しい英文表現 (ブルーバックス)

これも合わせて読むと面白いです．

3. 数学英語

この節では数学英語一般についての How to 本を紹介します．科学英語の中でも数学英語は独特のようで，一般に科学論文だとやめるように言われることが許容されるので，たまに戸惑います*1．

[3.1.] 数学のための英語教本

数学のための英語教本

最近出た本ですが，すでに名著の風格があります．テキスト型の構成の本なので，頭から一節ずつ読むことを推奨します．巻末には数学英語表現早見表もついているので便利です．もっと早く出版してほしかった……

[3.2.] 数理科学論文ハンドブック―英語で書くために

数理科学論文ハンドブック―英語で書くために

図書館で偶然見つけたのですが，辞書的に使うならこっちのほうが良いかもしれません．原著の新版が最近出たようです．

Handbook of Writing for the Mathematical Sciences

[3.3.] Mathematical Writing (Springer Undergraduate Mathematics Series)

Mathematical Writing (Springer Undergraduate Mathematics Series)

用例が多く載っているので，便利です．

[3.4.] A Primer of Mathematical Writing: Being a Disquisition on Having Your Ideas Recorded, Typeset, Published, Read, and Appreciated (Monograph Books)

A Primer of Mathematical Writing: Being a Disquisition on Having Your Ideas Recorded, Typeset, Published, Read, and Appreciated (Monograph Books)

まだきちんと目を通せていませんが名著だそうです．第二版のプレプリントが arXiv にあがっています．
[1612.04888] A Primer of Mathematical Writing, Second Edition

[3.5.] 数学版　これを英語で言えますか？　Ｌｅｔ’ｓ　ｓｐｅａｋ　Ｍａｔｈｅｍａｔｉｃｓ！ (ブルーバックス)

数学版　これを英語で言えますか？　Ｌｅｔ’ｓ　ｓｐｅａｋ　Ｍａｔｈｅｍａｔｉｃｓ！ (ブルーバックス)

数式の読み方が書いてある本です．数式を英語でわざわざ読み上げることが稀なので，ほとんど使ってません．英語で発表するときにもしかしたら使うかも？

4. 組版関連（LaTeX 関連）

この節では数式の出てくる文書独特の組版事情に関連する文書，また数式組版をするためによく使われる LaTeX に関連する文書を上げます．組版というのはざっくり言うと文書にするときの文字や記号の並べ方のことです（ここで詳しい人に刺される）．数式の組版には独特の慣習，規則がありますので，それに従わなくてはなりません．

[4.1.] 小田忠雄，「数学の常識・非常識—由緒正しい TeX 入力法」，数学通信, 第 4 巻第 1 号, 1999 年 5 月, pp.95–112.
ありがたいことに東北大学が無料で公開をしてくれています（合法のはずです）．http://www.math.tohoku.ac.jp/tmj/oda_tex.pdf
必要最低限の組版ルールの解説がされているので，これを読むだけでもだいぶ LaTeX のコードがきれいになります（OHP とか時代に合わない話も載ってしまっていますが）．

[4.2.] Michael Downes, Barbara Beeton,"Short Math Guide for LaTeX"
AMS のパッケージを使うための注意事項が書いてあります．AMS のパッケージを使わずに数学についての文章を書くことはまず考えられないので，読んでおくべきだと考えられます．TeX Live を使っている方は Power Shell やターミナルで

$ texdoc short-math-guide 

とすればいつでも読めます．texdoc というコマンドについては，LaTeX 初心者が知るべきただ一つのコマンド - Sokratesさんの備忘録ないし雑記帳という記事で以前紹介をしました．

[4.3.] [改訂第8版]LaTeX2ε美文書作成入門

[改訂第8版]LaTeX2ε美文書作成入門

かの有名な美文書作成入門です．「LaTeX の入門書で良いものは？」と聞かれたら，ほとんどの人はこれを挙げる気がします（たぶん）．最新版まだ読んでないんですけどね……

[4.4.] 独習 LaTeX2ε

独習 LaTeX2ε

某 W くんから誕生日プレゼントにもらってすごい助かっています．LaTeX 関連の書籍で一番わかりやすい本ではないかと思います（ただし，わたしにとっては）．大概，変なところで詰まったらだいたいこれを見ると解決します（マニアックなことしない限り）．

[4.5.] 数式組版

数式組版

数式組版についての唯一の和書である説……
読んでいるとたまに悪い例と良い例の違いがわからなくて発狂するときがあります．数式組版の深さを感じるための本です．

*1:この関連で最近私の周りで話題になったのが慣用句 "such that" です． "A such that B" で 「B を満たす A」を表現することが数学ではよくあります．しかし，この用法は一般的な辞書・文法書には見られない用法です（少なくとも私の手元にあるもので書いてあるものは確認できなかった）．数学英語独特の表現ではないかと推測されます（確証は持てませんが）．

LaTeX 初心者が知るべきただ一つのコマンド

という煽りタイトルで Texdoc を紹介する記事を書く宣言を何故かしてしまったので，書きたいと思います．後悔も反省もしている．たぶんみんな妖怪かスタンド攻撃のせい．

 この記事は TeX ＆ LaTeX Advent Calendar 2020 - Adventar の 24 日目の記事です．23 日目は munepi さんの Markdown原稿からPandocしてLaTeX組版する本作り - Qiita という記事でした．明日は zr_tex8r さんの 徹底攻略！ pxchfonを使いこなそう - Qiita という記事です．

 多分このアドベントカレンダーの参加者の中で一番の素人です．なんか雪だるまが回転するのを眺めていたら参加してました（なにを言っているのか自分でもわかりません）．なんで僕は TeX に詳しくないのにこのアドベントカレンダーに参加しているんだろう……．

 前置きが長くなりましたが，本題に入りましょう．間違いのないように気をつけて書いていますが，もし間違ったことを書いていたらごめんなさい*1． 

1. Texdoc って何だ？！

 Texdoc とは何かについて，述べましょう．

 Texdoc の公式ドキュメントには

Texdoc is a command line tool which search and view documentations in
TeX Live. 

(Manuel Pégourié-Gonnard, Takuto Asakura, "Texdoc Find & view documentation in TeX Live v3.0",  2018-06-06)

 と書いてあります．私の拙い語学力で訳すと次のような感じでしょうか？

Texdoc とは TeX Live のドキュメントを探して読むためのコマンドラインツールです．

(Manuel Pégourié-Gonnard, Takuto Asakura, "Texdoc Find & view documentation in TeX Live v3.0",  2018-06-06. 日本語訳は筆者)

どういうドキュメントが読めるかはTexdoc の中の人の手による TeX Live ドキュメント案内 - Qiita に詳しいのでそちらを読みましょう．

 はい．そんなわけで．Texdoc すごそうだね．おしまい．

 ってやろうかと思ったんだが，流石によろしくないので，もう少し話を続けます*2．

 現在， TeX Live を使っている TeX ユーザーが大半だと思うのですが，TeX Live ドキュメント案内 - Qiita によるとこの5GB 近い塊*3の4割位はドキュメントだそうです．これだけ容量を占めているドキュメントを読まないのはとてももったいないですね．このドキュメントを探して読むためのツールが Texdoc です．使い方は簡単．TeXLive の入っているパソコンで，単に PowerShell（Windows ユーザー）やターミナル（Linux ユーザー）に

$ texdoc (見たいドキュメントの名前)

を入力するだけです．勝手にビュワーが立ち上がって，ファイルを見せてくれます．

すごい簡単！！！これで明日からTeX Live ドキュメントのマスター(?)だ!!!

 とはならんですね．だって見たいドキュメントの名前わからなかったらどうしようもないわけですから．一応こんな名前のファイルないかなぁというのを探すときのために

$ texdoc -l (expr)

とオプションをつけることで，(expr) が含まれるドキュメントの一覧を出してくれますが，それでも初心者は何を (expr)とすればよいのかわからないでしょう（わかるなら多分初心者じゃないと思う．この記事読まなくて良いのでは）．

 そこで，texdoc を私自身がよく使うタイミングをユースケース*4として紹介したいと思います．皆さんの参考になれば幸いです．参考にならなくても怒らないでね．

 TeX Live を full インストールしていれば，他の環境でも問題なく再現できる話だと思いますが，動作確認は

• エディション Windows 10 Home
• バージョン 20H2
• OS ビルド 19042.685

の中で WSL 2 の ubuntu-20.04 で行っています．また，TeX Live の バージョンは 2019.20200218-1 です*5（私自身が，WSL ユーザーなのでアレですが，実は WSL で Texdoc を使うには工夫が必要です．手前味噌ですが，Windows Subsystem for Linux で Texdoc を使いたいというおはなし - Sokratesさんの備忘録ないし雑記帳 を参照してください）．

2. 初心者のための texdoc ユースケース

texdoc のユースケースを3つほど紹介します．

2.1. あの記号出したいんだけど，コマンドわからんのじゃが……

 ある日のこと，S くんはゼミでの論文紹介のためにスライドを LaTeX で作っていました．紹介したい論文に ¦ という記号が使われているので，自分のスライドにもこの記号を使いたくなりました．残念ながら S くんは頭がよくないので，¦ の出力コマンドをしりません．ここで諦めて別の記号を使うか，と思っていたとき，頭の良い友達の W くんが

$ texdoc symbols

を使ってみたまえ，と勧めてくれました．するとなんということでしょう，たちまち，symbols-a4.pdf *6という PDF ファイルが立ち上がり，LaTeX で使うことのできる記号の一覧が出てきたではありませんか！S くんはこのファイルの中を検索することによって ¦ という記号を出したければ，\usepackage{textcomp} をプリアンブルに書き，\textbrokenbar というコマンドを使えば良いことが分かりました．めでたしめでたし*7．

 また，別の日のこと，S くんは「新しく定義したこの『二項関係』の記号どうしようかな． LaTeX で使えるいい感じの関係記号ないかなぁ」と悩んでいました．悩んでいても仕方ないので，S くんは

$ texdoc symbols

してみました．symbols-a4.pdf は記号を種類ごとにまとめてくれているので，「binary」などと検索をすると，さまざまな二項関係の記号を眺めることができます．

「お，これ良さそう」

S くん，良さそうな関係記号を見つけることができたようです．めでたしめでたし．

2.2. パッケージ特有のコマンドを忘れちまった……

私はよく，bussproofs というパッケージで，証明図を書きます．証明図というのは次のような記号論理学などで使われる図です（Texdoc の使い方と直接関係ないので意味を理解する必要はありません）．

\begin{prooftree} \AxiomC{$A$} \AxiomC{$B$} \BinaryInfC{$A\land B$} \end{prooftree}

しかし，頭がよくないので，普段やらないようなことをやろうとすると，すぐコマンドがわからなくなります．

たとえば，

\begin{prooftree} \AxiomC{$\exists x\varphi$} \AxiomC{$[\varphi\left(t\right)]$} \UnaryInfC{$\vdots$} \UnaryInfC{$C$} \BinaryInfC{$C$} \end{prooftree}

の \(C\) と \(\vdots\) の上の線を消したくなったとします．こういう線を消すためのためのコマンドをよく私は忘れます．

こういうときは公式ドキュメントをみるために次のコマンドを打ち込みます．

$ texdoc bussproofs

すると，bussproofs.sty の公式ドキュメントが立ち上がります．ざっと目を通してみると，\noLine というコマンドで打ち消せることがわかりました（このくらいそろそろ覚えろよ）．

\begin{prooftree} \AxiomC{$\exists x\varphi$} \AxiomC{$[\varphi\left(t\right)]$} \noLine\UnaryInfC{$\vdots$}\noLine \UnaryInfC{$C$} \BinaryInfC{$C$} \end{prooftree} 

 よし一仕事終わり！目的の証明図を出すことができました．

 このように Texdoc でパッケージの公式ドキュメントを呼び出すことができます*8．他にもたとえば

$ texdoc tikz

とすれば，tikz の公式ドキュメント*9が立ち上がるわけですね．

いわゆるパッケージ以外にも KOMA-Script という種類のドキュメントクラスの公式ドキュメントは

$ texdoc KOMA-Script

と打てば，出てきますし，

$ texdoc luatex-ja

 と打てば，LuaLaTeX で使える種類の日本語ドキュメントクラスの公式ドキュメントが立ち上がります．普段使うドキュメントクラスの公式ドキュメントを調べてみると自分の知らないオプション引数など新しい発見があり，おもしろいです．

ところで，Texdoc も TeX Live に含まれるツールの一つなので，

$ texdoc texdoc

とすれば，Texdoc の公式ドキュメントを見ることができます．Texdoc すごい！

2.3. 俺は TeX Master になるって，この前の飲み会で言ったら TeX に詳しい人達に複雑な顔をされた．それはそれとして，人並みには TeX を理解したいなぁ．

 TeX Live に含まれるドキュメントはいわゆるパッケージの公式ドキュメント以外にも色々あります．そういうドキュメントは TeX Live ドキュメント案内 - Qiita に詳しいです．

 その中でも，初心者が読むと嬉しくなりそうなものを二つほど紹介します．

１つ目は

$ texdoc short-math-guide

などとすると立ち上がる short-math-guide.pdf です．AMS のパッケージを使って LaTeX 文書作るときの注意点がまとまっていて，参考になります．AMS のパッケージを使わずに LaTeX 文書を作ることは珍しい時代だと思うので，数学を専門にしていなくても役に立つんじゃないかと思います．英語の文書ですが．

２つ目は

$ texdoc platexsheet

などとすると立ち上がる pLaTeX のチートシートです．基本的なコマンドをど忘れしたときなどに役に立ちます．

3. まとめ

 はい．そんなわけで TeX 初心者にとって役に立ちそうな texdoc のユースケースを3つ紹介しました．

 もしかしたら，「ググった方が早いのでは」と思った人がいるかも知れませんが，LaTeX に対する怪しげな記事*10が散見される現代にあっては，公式ドキュメントに目を通す習慣をつけるという意味でも，Texdoc を使ってみると良いと考えます．

 Texdoc の仕組みや立ち上がる pdf viewer の変更方法などより進んだ情報については，

$ texdoc texdoc

をすると見ることのできる Texdoc の公式ドキュメントを参考にしてください．

 Texdoc の検索ワードを何も思いつかんとき，結局ググるけどね．

*1:もし，間違ったことを書いていても詳しい人からツッコミが入るはずなので，そのうち訂正されるはずだ．たぶん．知らんけど．

*2:TeX Live ドキュメント案内 - Qiita 以上の内容を書ける自信はないですが．

*3:Full でインストールした場合．

*4:あれ，使い方合ってる？

*5:最新版を apt を使わずに引っ張ってくる元気はない．

*6:http://tug.ctan.org/info/symbols/comprehensive/symbols-a4.pdf

*7: このケースの場合， Detexify LaTeX handwritten symbol recognition のような手書きされた記号から TeX Command を推測してくれるサービスを使うという手もあるんですがね……．後で知りましたが．

*8:というか，そのための Texdoc だよなという……

*9:聞いた話による（どこで聞いたかは忘れてしまった）と，tikz の公式ドキュメントには現在非推奨なコードが含まれているそうなので，読む際には注意が必要だそうです．

*10:この記事のように．

ZF が矛盾した日

 Twitter にて「Tychonoff の定理 が選択公理なしで証明された」という主張を見た．

 どのような体系で証明されたのかよくわからないが，もし，その体系が ZF の部分体系(もしくはそれと同等の証明能力を持つ体系)であって，また仮に証明されたのが事実だとすれば，その系として「ZF が矛盾する」ことを示す．以下では選択公理は ACと略記する．

 次の事実を使う．

事実1.

以下の2つは同値

1. ZF が矛盾する
2. ZF + \(\lnot\)AC が矛盾する

事実2.

ZF 上で AC とTychonoff の定理 は同値．

 さて，ZF の部分体系(もしくはそれと同等の証明能力を持つ体系)で「Tychonoff の定理 が選択公理なしで証明された」と仮定しよう．すると，当然 ZF において，Tychonoff の定理 を選択公理なしで証明することができる．これは事実2 から ZF において，AC が証明できることを意味する．よって，ZF + \(\lnot\)AC から AC が証明できる．これはZF + \(\lnot\)AC が矛盾することを意味する．ゆえに事実1 からZF が矛盾することが結論される．

また

事実3.

以下の2つは同値

1. ZF が矛盾する
2. ZFC が矛盾する

から，ZFCも矛盾する．

参考文献

Set Theory (Studies in Logic: Mathematical Logic and Foundations)

集合論―独立性証明への案内

集合・位相入門 (松坂和夫　数学入門シリーズ)

追記(2020/9/18)

 どうも「Tychonoff の定理 が選択公理なしで証明された」と主張された方は「ZFC は矛盾している」という信念をお持ちのようである．仮に「ZFC は矛盾している」と仮定すると「ZF が矛盾すること」は事実3 からすみやかに導かれる．つまり，この記事の内容は件の人にはすべて自明であったようである．なんてこったい．

n回微分可能だがn階導関数が不連続になる関数

 ある日, わたしが

「微分可能だけど導関数が不連続な関数を思いつかないよう(ノдヽ)」*1

と困っていたらある人が

「[1]のページに答えが書いてあるよ」

と教えてくれた.

 そこに書かれている関数を眺めていたら\(n\)回微分可能だが\(n\)階導関数が不連続になる関数を思いついたのでここに記す. 

定義1 (\(n\)回微分可能だが\(n\)階導関数が不連続になる関数)

\(f : \mathbb{R} \to \mathbb{R} , n \in \mathbb{N} \)

\[ \mathop{f}{\left( x \right)} := \begin{cases} x^{2n} \sin \frac{1}{x}, & x \neq 0; \\ 0, & x = 0. \end{cases} \]

\(f\)が\(n\)回微分可能だが\(n\)階導関数が不連続になる関数である証明の概略

命題2 (\(f\)の\(m\)階導関数)

\[ \mathop{f^{\left( m \right)}}{\left( x \right)} := \begin{cases} \sum_{k=0}^{m} a_{\left( m , k \right)} x^{2n-m-k}  \mathop{\mathrm{CS}_{k}} \frac{1}{x}, & x \neq 0; \\ 0, & x = 0; \end{cases} \]

for \( m \in \mathbb{N} , 1 \leq m \leq n - 1\), \( a_{\left( 1 , 0 \right)} = 2n , a_{\left( 1 , 1 \right)} = 1,  \) \(a_{\left( 1 , k \right)} = 0 \quad \left( 1< k \right), \) \( a_{\left( m , 0 \right)} = 2n \cdot \left( 2n - 1\right) \cdot \dots \cdot \left( 2n - m + 1 \right) \quad \left( 1 < m \right), \) \( a_{\left( m+1 , k \right)} = \left( 2n - m - k \right) a_{\left(m , k \right)} + (-1)^{k+1} a_{\left( m , k -1 \right)} \quad \left( 1 < k \right) , \)

\[ \mathop{\mathrm{CS}_{k}} {\left(  x \right)} = \begin{cases} \sin x, & k\text{ is even}; \\ \cos x, & k\text{ is odd}. \end{cases} \] 

 

(命題2の証明の概略)

\(x=0\)での微分可能性と\(\mathop{\mathrm{CS}_{k}}' {\left( x \right)} = \left( -1 \right)^{k} \mathop{\mathrm{CS}_{k+1}} {\left( x \right)}\)に注意して\(m\)についての帰納法. \(\square\)

系3 (\(f\)の\(n\)階導関数)

\[ \mathop{f^{\left( n \right)}}{\left( x \right)} := \begin{cases} \sum_{k=0}^{n} a_{k} x^{n-k}  \mathop{\mathrm{CS}_{k}} \frac{1}{x}, & x \neq 0; \\ 0, & x = 0; \end{cases} \]

where, for \( m \in \mathbb{N} , 1 \leq m \leq n - 1 \) and

\[ \mathop{\mathrm{CS}_{k}} {\left(  x \right)} = \begin{cases} \sin x, & k\text{ is even}; \\ \cos x, & k\text{ is odd}; \end{cases} \]  \( a_k \text{ is const.} \)  

この\(f^{\left(n\right)} \left (x \right)\)は原点で不連続である. なぜなら, \( k < n \) のときは\[a_{k} x^{n-k}  \mathop{\mathrm{CS}_{k}} \frac{1}{x} \to 0 \qquad \text{as } x \to 0\]だが,  \(k = n\) のとき \( a_{k} x^{n-k}  \mathop{\mathrm{CS}_{k}} \frac{1}{x} = a_{k} \mathop{\mathrm{CS}_{k}} \frac{1}{x} \) は \(x\to 0\) で振動するから. \(\blacksquare\)

余談

1. 当たり前だが, この\(f \in C^{n-1}\)だが\(f \not \in C^{n}\)である. 

2. \(f \in C^{n-1}\)だが\(f \not \in C^{n}\)であるような関数はこれ以外にも

\[ \mathop{g}{\left( x \right)} := \begin{cases} x^{n}, & 0 \leq x; \\ -x^{n}, & x < 0; \end{cases} \]

などがある. ただ, この関数の\(n\)階導関数はそもそも存在しない. \((n-1)\)階導関数 \(g^{\left( n-1 \right)} \left( x \right)= n!\left| x\right|\) は連続だが \( x = 0 \) で微分不可能だからである.

参考文献

 [1]  https://mathtrain.jp/c1kyukansu

*1:つまり微分可能だが \(C^1\) 級ではない関数が思いつかないと悩んでいた.

分離論理入門のようなもの

この記事は

https://adventar.org/calendars/4015

の12/21 の記事です．

わたしは分離論理について書きました．

日本語で読める分離論理についてのある程度まとまった文書をわたしは知らないので，需要があるのではないかと思って書きました．

今回は「一階述語論理は知っているけど，分離論理ってなんや」と思っている方を想定読者として書いています。お楽しみいただくか、参考になれば幸いです．

 こちらのリンクから文書はダウンロードできます．

https://sokratesnil.github.io/pdfs/SL.pdf

数学する身体を読んで

数学する身体を読んだ。

内容は次のように表現できる。

マンガ おはなし数学史 : これなら読める！これならわかる！ (ブルーバックス)

異端の数ゼロ――数学・物理学が恐れるもっとも危険な概念 (ハヤカワ文庫NF―数理を愉しむシリーズ)

ゼロから無限へ―数論の世界を訪ねて (ブルーバックス)

虚無

春宵十話 随筆集/数学者が綴る人生1 (光文社文庫)

数学の認知科学

(2020/8/30 追記 この本の「身体化された数学」という単語を借用している可能性あり。元の意味と同じかは『数学する身体』の中で定義されていないため不明。

2021/11/16 追記

『数学する身体』の文庫本を本屋で見かけたので、参考文献リストを確認したところ、この本は載っていなかった。意図的かサーベイ不足かまではわからない) 

これらを百倍に薄めたもの。

おしまい。

それよりも次の本を読んだ方が勉強になるしおもしろい。または薄める前のものを読むと良い。

カッツ 数学の歴史

数学の歴史 (放送大学教材)

数学を哲学する

Zorn の補題は何の補題? ―「補題」と呼ばれる定理たち―

数学の世界には慣例的に「補題」と呼ばれる"定理"がある. 

たとえば, 

• Zorn の補題
• Kőnig の補題
• Tukey の補題
• 握手補題
• Farkasの補題
• 米田の補題

などである(分野に偏りがあるのはご容赦).

 なぜこれらは補題と呼ばれるのか? 

 大学生の頃にMartin Aigner, Günter M. Ziegler, "Proofs from THE BOOK", Springer のChapter 25の冒頭に答えが書いてあるのを見つけた. 有名な事実かと思いきやそうではないらしいので, せっかくなのでこのブログで共有をしたい. 

 以下がそのChapter 25の冒頭の文章である. 

 The essence of mathematics is proving theorems - and so, that is what mathematicians do: They prove theorems. But to tell the truth, what they really want to prove, once in their lifetime, is a Lemma, like the one by Fatou in analysis, the Lemma of Gauss in number theory, or the Burnside-Frobenius Lemma in combinatorics.
 Now what makes a mathematical statement a true Lemma? First, it should be applicable to a wide variety of instances, even seemingly unrelated problems. Secondly, the statement should, once you have seen it, be completely obvious. The reaction of the reader might well be one of faint envy: Why haven't I noticed this before? And thirdly, on an esthetic level, the Lemma - including its proof - should be beautiful! 

(Martin Aigner, Günter M. Ziegler, "Proofs from THE BOOK" , Third edition, Springer, 2004, p.167)

 訳すと次のようになるだろうか?

 数学の本質は定理を証明することである.  ― すなわち, それが数学者のやっていることである. 彼らは定理を証明している. しかし, 本当のことを言えば, 生涯に一度でもいいから彼らが本当に証明したいものは補題なのである. たとえば,  解析学におけるFatou の補題や数論におけるGauss の補題, 組み合わせ数学におけるBurnside-Frobenius の補題のような.
 さて,  何をもって数学的主張は真の補題と言われるのか? まず, その主張は一見して無関係と思えるような問題にさえも応用可能なほど広範囲の応用例を持つべきである*1.  次に, その主張は一見して完璧に明らかであるべきである.  その主張を読んだものはかすかな羨望を覚えるかもしれない. 「なぜ, こんな簡単なことに私は気が付かなかったんだろう?」と*2. 最後に, 美的感覚*3において, その「補題」が―証明も含めて―美しくあるべきである!

(翻訳は筆者自身)

「補題」と呼ばれる"定理"にはこのような事情があったのである. 

 たしかに冒頭に挙げたような「補題」たちはいろんな定理の"補題"になっている(言い換えると, 応用範囲が広い)し, (一度わかれば)主張は明らかである. 最後の「美しさ」の部分については意見が分かれるような気もするが, 見る人が見れば「美しい」のであろう(たぶん). 

 今後の読者の学習の参考になれば幸いである. 

参考文献

Proofs from THE BOOK

この本は日本語訳も出ている.  

天書の証明

*1:訳注:かなり意訳してしまったので, ニュアンスが違うかもしれない.

*2:訳注: 原文では直接話法ではなかったのだが日本語にすると大変おさまりが悪かったのでこうした.

*3:訳注:ここもニュアンスをうまく訳せていない可能性がある. esthetic は「審美的」と訳されることが多いようであるが, あまり一般的な用語ではないように思われ, 意味が伝わらないのではないかと考えた.

自然数の定義

自然数の定義を淡々と述べるものです. 過度な期待はしないでください.

1. 構造としての自然数の定義

1.1. Dedekind による定義

  空でない集合 \( \mathbb{N} \) と単射写像 \( \mathop{s}: \mathbb{N} \to \mathbb{N}\) ,  \( 0 \in \mathbb{N} \) が次のI), II)を満たすとき \( \left(\mathbb{N}, \mathop{s}, 0 \right) \) を自然数と言う:

I) \(  0 \not \in \mathop{s} \left(\mathbb{N}\right) \);

II)  \( X \subset \mathbb{N} \)について, \( 0 \in X \)かつ\( \mathop{s} \left(X\right) \subset X \)ならば, \( X = \mathbb{N}\).

1.2. ペアノの公理（オリジナルとは異なる書き方をしている）

  空でない集合 \( \mathbb{N} \) と単射写像 \( \mathop{s}: \mathbb{N} \to \mathbb{N}\) , ある \( 0 \in \mathbb{N} \) が次のI), II)を満たすとき \( \left(\mathbb{N}, \mathop{s}, 0 \right) \) を自然数と言う:

I) \( \mathop{s}\left( x \right) = 0 \) となるような \( x \in \mathbb{N} \) は存在しない;

II) \( \mathbb{N} \) の元 \(n\) についての(正しいとは限らない)性質 \( P\left( n \right) \) が次のi), ii)の性質を満たすとき, すべての \( \mathbb{N} \) の元 \(n\) について \( P\left( n \right) \) は成り立つ:

i) \( P \left( 0 \right)\) が成立する; 

ii) \( P \left( n \right) \) が成立すると仮定したとき, \( P \left( \mathop{s}\left( n \right) \right) \) が成立することが示せる. 

1.3. 2階述語言語を用いて

 \( \mathcal{L}_2 =\left( 0, s, = \right) \)という2階述語言語に対して以下のような論理式の集合\( T \)を考える.  \[ \forall x \forall y \left( sx = sy \to x = y \right) \] \[ \forall x  \lnot \left( sx = 0 \right) \] \[ \forall X   \left( 0 \in X \land \forall n \left(  n \in X \to sn  \in X \right)  \to \forall n \left( n \in X \right) \right) \]

\( T \)の（標準解釈の下での）モデルを自然数という. 

2. 1の自然数の定義を満たす具体的な自然数

 当たり前ですが, ここから下で定義されるものは1の定義を満たしています. 

1.1.  文字列

 \( 0, s \)を文字とする. 

I) 文字列"\(0\)"は自然数である. 

II) 文字列"\(\mathbf{n}\)"が自然数であるとき, 文字列"\(s\mathbf{n}\)"は自然数である. 

III) I), II)のようにして構成される文字列のみが自然数である. 

1.2. 空集合からの構成 

I) 空集合\(\emptyset\)は自然数である. 

II) 集合\(n\)が自然数であるとき, 集合\(n \cup \left\{ n \right\}\)は自然数である.

III) I), II) のように構成される集合のみが自然数である. 

1.3. 順序数として

 最小の極限順序数を自然数という.  

1.4. 自由モノイド (M 氏に教えてもらった)

 \( \left\{ 1 \right\} \)を生成元とする自由モノイドを自然数と言う. 

参考文献

[1]H.D.エビングハウス他, 『数』, 丸善出版

数 上 (シュプリンガー数学リーディングス)

 [2] 田中一之他, 『ゲーデルと20世紀の論理学3』, 東京大学出版会

ゲーデルと20世紀の論理学 3　不完全性定理と算術の体系

[3] デーデキント，『数について：連続性と数の本質』，岩波書店

数について: 連続性と数の本質 (岩波文庫 青 924)