使う言葉：
- 述語 → (述語関数 | 述語記号)
- 命題〈単純命題〉
- 構造化命題〈structured proposition〉
- 導出〈derivation | デリベーション〉
- シーケント
- リーズニング
- 背景指標
- 導出可能〈derivable | デライバブル〉
使わない言葉：
- 判断
- 証明
- 推論
- 推論規則
- 公理 アノテーション @axiom としては使うかも
- 定理 アノテーション @theorem としては使うかも
曖昧性：
- 判断 → 構造化命題 | 導出 | 導出可能メタ命題
- 証明 → 導出射 | 導出定義 | 導出表現〈導出コンビネーション〉
- 推論 → 基本導出 | 基本リーズニング | 導出 | リーズニング
- 推論規則 → 基本導出 | 基本リーズニング
- 公理 → 基本導出射 | 基本導出宣言
- 定理 → 導出射 | 導出宣言 | 導出の宣言と定義のペア
使う記号：$`\newcommand{\rimp}{\multimap}
\newcommand{\limp}{ \style{display: inline-block; transform: rotate(180deg)}{\multimap} }
\newcommand{\reason}{\rightsquigarrow}
`$
- $`\rimp, \limp`$ ： 含意演算子記号
- $`\to`$ ： シーケント〈導出プロファイル〉区切り記号
- $`\reason`$ ： リーズニングプロファイル区切り記号、変更の可能性あり
- $`\mid\vdash`$ ： 導出可能メタ記号
- $`\vdash`$ ： 自然演繹導出可能メタ記号
