0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@etale_cohomology(Etale Cohomology)

【Arend連載６回目補足】宇宙レベルに束縛されない型が新規導入された件 ── Arend 1.12.0 の告知を、第６回の記述と照合する

0
Last updated at Posted at 2026-09-05

thumbnail_picture.jpg

本記事の結論（Executive Summary）

2026年８月４日に、Arend version 1.12.0の公開が事前告知されました。

しかし、2026年9月5日現在、公式GitHubには1.12.0について、実機で動かすことのできるコード資材は未だに公開されていないままです。

そこで今回、実機検証はできないものの、version 1.12.0について、予告情報として公開されている公式ブログ記事や公式ドキュメント、論文の内容を確認した限りにおいて、本Arend連載全７回シリーズの初回～６回目までの記事で皆様にお届けしてきた記述の内容のうち、version 1.12.0で内容が古くなった部分はあるのか、あるとしたら、情報更新後の記載内容はどうなるのかを、整理してお届けします。

調査した結果、前回（第６回目記事）で論じてきた「宇宙」の基本規則と、本連載シリーズで述べてきた内容は訂正する必要がなく、内容は維持される一方で、「宇宙」に関するコードの記法と、「レベル多相」の扱いには（ver 1.12.0への移行に伴い）変更が必要そうだ（version 1.12.0の予告編関連公式資料を確認した限りでの判断）というものです。

変更の必要がない箇所

第６回で扱った次の中核的な事項は、1.12.0 の公式ドキュメントと論文を確認した結果、引き続き成立します。

  • \Type0 : \Type1 : \Type2 という宇宙の階層
  • \Prop : \Set0
  • 集合 A : \Set p の要素の等しさ x = y が \Prop に属すること
  • 宇宙の累積性
  • $\Pi$ 型・$\Sigma$ 型の宇宙レベルが max で決まること
  • 非可述性と、「証明を持ち回らずに済む」設計の根拠

従って、本連載シリーズで取り上げてきたArendの定理証明支援処理系としての設計思想の特徴と、他の言語と比較したときの Arend の強み・弱みについての説明は書き直す必要はないと判断しました。（前述のとおり、version 1.12.0については実機検証することで言語仕様を確認することがまだできませんので、検証作業には限りがあります）

出典：

変更が必要な箇所

「宇宙」（Universe）に関するArendの記法と、「レベル多相」の扱いについては、version 1.10.0と、version 1.12.0とで顕著な変更点があります。

論点 Arend 1.10 1.12.0 ドキュメントの説明
レベルなしの \Type 型検査器が状況に応じて有限レベルを推論する 最大の「無限の可述的レベル」を表す
\oo ホモトピーレベルの無限大を表す 廃止。 切断されていない宇宙は \Type p
\lh ホモトピーレベル用の暗黙の径数 廃止。 ホモトピーレベルは多相の軸ではない
レベル多相 \lp と \lh を暗黙に利用 .{l} で可述的レベルを明示的に宣言する
\Set のレベル省略 受理される エラー。 \Set0 や \Set l が必要

とくに、レベルなしの \Type の意味が変わりました。
version 1.10 では \func bad : \Type => \Type が通ります。

しかし、version 1.12.0 のドキュメントでは、無限レベルの \Type はどの有限宇宙にも属さず、自分自身にも属さないため、この種の定義は許されない と説明されています。*

変更が必要 なのは、第６回の記事で掲載した「記号一覧表」のうち \Type、\oo、\lh の３項目と、\lp \lh を使ったレベル多相の書き方です。**

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

「宇宙レベルに束縛されない型」とは

version 1.12.0 で導入された「宇宙レベルに束縛されない型」 について、本記事執筆者は、次のように解釈します。

  • \Type0、\Type1、\Type2 などは、有限の可述的レベルを持つ宇宙である
     
  • レベルを省略した新しい \Type は、それらの「どれか」ではなく、無限レベルの宇宙を表す
     
  • この \Type はどの \Type n にも属さず、とくに自分自身を含まない
     
  • そのため、Type : Type のような矛盾につながりうる循環を防ぐ
     
  • 有限レベルの \Type0 や \Set0 などは引き続き使用できる

つまり、version 1.12.0は、「有限レベルの宇宙を廃止して無限宇宙だけにした」のではありません。

  • レベルを意識しなくてよい径数には、無限の \Type を用いる
  • 有限レベルが重要な箇所では従来どおりレベルを明示する、

という 使い分けが、version 1.12.0では想定されている、というのが筆者の解釈 です。

出典：

比較したリリース・バージョン

本連載シリーズは、（version 1.11系が未公開のため）version 1.10を実機検証することで執筆・公開してきました。

今回行ったのは、version 1.11.0と1.12.0（動かせるコードが未公開のため予告関連公式資料のみ）を比較する作業です。

リリースバージョン 状態
1.10 本連載で実機検証に使用。GitHub の最新リリース
1.11.0 2025年12月11日にブログで告知。**GitHub には公開されていない。**告知に宇宙系の変更はない
1.12.0 2026年8月4日にブログで告知。GitHub には公開されていないが、IntelliJ プラグインとして2026年7月30日に配布されている

出典：

検証上の制約

1.12.0 をめぐる公式情報には、３種類の不整合があります。

不整合 内容
配布 公式ブログは 1.12.0 を「released」と告知しているが、GitHub の最新タグ・最新リリースは 1.10 のまま
記述 ドキュメントは新記法（無限 \Type、.{l}、\lh 廃止）を説明するが、論文は従来の暗黙のレベル径数や \lp \lh の説明を残す
論文内部 論文の CLI の節は 1.12.0 の新機能を説明する一方、宇宙の節は従来の記述を含む

筆者は、IntelliJ 用 Arend プラグインに base-1.12.0.jar が含まれており、型検査器自体は配布されていることを確認しました。

しかし上記の「1.12.0」からダウンロード可能なzipファイルを解凍したところ、CLI 本体は同梱されておらず、1.10 の CLI と組み合わせても API の不整合で実行できませんでした。

そのため、1.12.0 で実際にコードを型検査する直接検証はできず、1.12.0については公式ブログ記事や公式ドキュメント、論文の記述に頼らざるをえませんでした。

なお、本記事の実機検証はすべて Arend 1.10 によるものです。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、Arend Plugin Versions, JetBrains Marketplace

本記事の最終的な立場

  • 型検査器の内部実装は大幅に刷新された、と公式ブログは告知している。ただし、内部実装の詳細は公開されていない
     
  • 型がどの宇宙に置かれるかを定める規則は、公式ドキュメントと論文を読む限りで、version 1.10 と 1.12.0とで変更点は存在しない
     
  • 宇宙を書き表す記法（\Type、\oo、\lh）と、レベル多相の書き方（\lp \lh から .{l} へ）は、1.10 と 1.12.0 で大きく異なる
     
  • 結論として、前回第６回目の記事で述べた「宇宙」に関する理論的な主張は保たれる一方で、Arendの記法に関して、\lp \lh \oo を使ったコードと、第６回の記号一覧表には一部変更が生じている
  • version 1.12.0 について、 CLI 等で直接実行できる実行ファイルが公式にリリースされた時点で、コード実機検証を含めた再検証が必要と考えられる

なお、宇宙系以外にも、1.12.0 では CLI のバイナリキャッシュ、JSON 出力、証明探索、使用箇所検索、クラス階層検索、REPL の改善、IntelliJ 2026.2 対応、arend-lib への代数幾何・解析・代数の追加が告知されています。これらは本連載シリーズの第７回目の記事で扱います。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

本記事で参照する公式資料

本記事では、「ブログ」「ドキュメント」「論文」という語を繰り返し使います。それぞれが何を指すかを、先に明示しておきます。

略称 書誌情報 URL
ブログ Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日 https://arend-lang.github.io/2026/08/04/Arend-1.12.0-released.html
ドキュメント Universes, Arend Documentation（リリースバージョン 1.12.0） https://arend-lang.github.io/documentation/language-reference/expressions/universes
論文 Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"（2026年8月10日、公式ブログで完成を告知） https://arend-lang.github.io/assets/lang-paper.pdf

このほかに、1.12.0 に関連して筆者が確認した公式資料は、次のとおりです。

# 資料 URL 本記事での扱い
④ Arend 1.11.0 released, Arend Theorem Prover, 2025年12月11日 https://arend-lang.github.io/2025/12/11/Arend-1.11.0-released.html 宇宙系の変更がないことの確認に使用
⑤ Paper on Arend, Arend Theorem Prover, 2026年8月10日 https://arend-lang.github.io/2026/08/10/Arend-paper.html 論文の完成告知。目次のみ
⑥ Level, Arend Documentation https://arend-lang.github.io/documentation/language-reference/definitions/level \use \level の仕組みと、.{l} 構文の用例
⑦ Functions, Arend Documentation https://arend-lang.github.io/documentation/language-reference/definitions/functions 関数定義の構文。.{l} への言及なし
⑧ Downloading Arend, Arend Documentation https://arend-lang.github.io/documentation/getting-started/download jar の取得先
⑨ JetBrains/Arend, GitHub https://github.com/JetBrains/Arend 最新タグと master の確認
⑩ JetBrains/arend-lib, GitHub https://github.com/JetBrains/arend-lib 同上
⑪ Arend Plugin for JetBrains IDEs, JetBrains Marketplace https://plugins.jetbrains.com/plugin/11162-arend 2025年12月22日更新。「Bug fixes」のみ

確認できなかった資料

# 資料 状態
⑫ arend-lib v1.12.0 のドキュメント（https://arend-lang.github.io/arend-lib/v1.12.0/） 403。アクセスできない
⑬ GitHub の v1.12.0 リリースページ **存在しない。**最新タグは v1.10

筆者は、①〜⑪をすべて読みました。①②③⑥⑦は全文、④は冒頭、⑤⑧〜⑪は該当箇所です。

ここまでが、本記事の結論を先取りしてお伝えしたものです。

ここから先は、お時間のある方だけ、お読みいただく形で差し支えございません。

なぜ補足記事を書くのか

第６回目の記事は、Arend 1.10 で執筆・検証しました。

2026年8月4日に、Arend 1.12.0 が告知されたものの、1.12.0はまだ、公式GitHub上に公開されておらず、実機検証ができませんでした。

そこで、公開告知文や関連するドキュメントやブログ記事、論文を読んで把握できた範囲内で、本連載シリーズの初回～６回目までに述べてきた内容について、事後的に修正したり訂正すべき点があるかどうかを調べました。

本稿は、そのチェック結果を読者の皆様にお伝えするものです。

告知文に、次の一文があります。

（原文引用）

This release includes a major internal overhaul of the universe/level system

（筆者による日本語訳）

このリリースは、宇宙／レベル系の大幅な内部刷新を含む。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

第６回目の記事の主題は、まさに宇宙の設計でした。

したがって、1.12.0 の変更が第６回の記述に影響するかどうかを、読者にお示しする必要があります。

本記事の主題

本記事のテーマは、「1.12.0 について、公式資料は宇宙の規則では一致し、記法では不整合がある。第６回の論旨は保たれる」ということです。

そのことを、ドキュメント・論文・1.10 の実機の三者を照合することで示します。

読者の皆様が、まず抱かれるであろう疑問

タロウくん：
Arendがバージョン1.12.0で、宇宙の言語仕様を含めて大きく変わったということですか？

ということは、この連載シリーズの初回から６回目まで、Arendについて解説してきたことと、他の言語と比較したときの大きな相違点と強み・弱みも、連続シリーズをすべて書き直さないといけない(すでに公開済みの記事はArendバージョン1.11.0でしか成立しない古い内容になった)ということですか？

ここまで書いてきた記事と、先生との対話が全て内容が古くなったという理解でよろしいですか？

専任講師：
いいえ。すべて書き直す必要はありません。

告知文には「宇宙／レベル系の大幅な内部刷新」とあります。しかし、本記事の第２部で照合したとおり、宇宙の規則そのものは変わっていません。変わったのは記法です。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日、Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・記法だけ、ですか？

専任講師：
第１回目から第６回目までの記事で解説した、Arend の設計判断と、他の言語との相違点・強み・弱み。これらは 1.12.0 でも成り立ちます。

具体的に何が変わり、何が変わらないのかを、本記事の第５部で表にして示します。

タロウくん：
・・・公開済みの記事は、1.11.0 でしか成立しない古い内容になったのではないのですか。

専任講師：
まず、本連載で実機検証に使ったのは 1.10 です。1.11.0 ではありません。

そして、1.10 と 1.12.0 のあいだで変わったのは、記号一覧表の４項目です。
\Type の意味、\oo、\lh、レベル多相の記法。

それ以外は、そのまま成り立ちます。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・では、先生との対話も、古くなっていない。

専任講師：
対話で扱った内容のうち、宇宙の規則、証明を持ち回らない仕組み、非可述性、累積性は、1.12.0 のドキュメントが明文化した規則と一致しています。古くなっていません。

記法に関わる箇所だけ、本記事で補足します。

検証の範囲について

ブログは 1.12.0 を告知していますが、GitHub の master と最新リリースは 1.10 のままです。そのため、2026年9月時点で実施可能な範囲内でコード検証を行いました。

本記事に掲載したコードは、すべて Arend 1.10 で検証したものです。1.12.0 の jar が入手できた時点で、改めて検証します。

本記事の議論の流れと読み方

本記事を読むと、何が分かるのか

本連載で実機検証に使った Arend 1.10 と、2026年8月に告知された Arend 1.12.0 とで、何が変わり、何が変わらなかったのか。それを表で示します。

なぜ 1.11.0 を扱わないのか

1.10 と 1.12.0 のあいだに、1.11.0（2025年12月11日）があります。

しかし、1.11.0 は、実機で動かせるコードが GitHub に公開されていません。

さらに、1.11.0 の告知には、宇宙系の変更は書かれていません。

告知は「安定性の向上」と「Arend server の導入」を主な内容としています。

したがって、本記事では 1.10 と 1.12.0 を直接比べます。

出典：
Arend 1.11.0 released, Arend Theorem Prover, 2025年12月11日

変わらなかったもの

第６回の記述 1.10 1.12.0
\Type0 : \Type1 : \Type2 の階層 ○ ○
\Prop : \Set0 ○ ○
\Set0 の等しさの型が \Prop に属する ○ ○
累積性 ○ ○
$\Pi$ 型のレベルは max ○ ○
非可述性 ○ ○

第６回で実機検証した宇宙の規則は、すべて 1.12.0 のドキュメントに明文化された規則と一致しています。

宇宙が２つの数で指定される理由、証明を持ち回らずに済む仕組み。第６回の論旨は、1.12.0 でも成り立ちます。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

変わったもの ── ドキュメントを読む限りでの確認結果

次の表は、ドキュメント（Universes・Level）の記述に基づきます。論文はこれと異なる記述をしています（第４部で扱います）。

第６回の記述 1.10 1.12.0（ドキュメント）
記号一覧表の \Type レベルを推論する 無限のレベルを表す
記号一覧表の \oo ホモトピーレベルの無限大 廃止
記号一覧表の \lh ホモトピーレベルの径数 廃止
レベル多相の書き方 \lp \lh を暗黙に使う .{l} で明示的に宣言する

ドキュメントによれば、変わったのは記法です。設計思想は変わっていません。

ただし、論文は従来の記法（\lp \lh）を記述しており、ドキュメントと論文のあいだに不整合があります。

どちらが 1.12.0 の実装を反映しているかについては、第４部で述べるとおり、開発者本人が書いたと推定される arend-skills がドキュメント側と一致しており、ドキュメント側と解釈する根拠が強いと筆者は考えます。

ただし、1.12.0 を実機で動かして確かめるまで、確定的な判断ではありません。

出典：

\Type の意味の変化について

表の１行目を、少し補います。

第６回で、\Type0、\Type1、\Type2 と、数字を付けて宇宙の階層を説明しました。

数字を付けない \Type と書いたとき、それが何を指すかが、1.10 と 1.12.0 で違います。

数字なしの \Type は何を指すか
1.10 型検査器が、文脈に合う数字を自動で補う。\Type0 になったり \Type1 になったりする
1.12.0 どの数字よりも上の、無限のレベルを指す。どの \Type n にも属さない

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

1.12.0 の jar ── GitHub からは入手できない

ブログは 1.12.0 を告知していますが、GitHub の最新リリースは 1.10 のままです。本記事の実機検証は、すべて 1.10 で行いました。

出典：
Downloading Arend, Arend Documentation、JetBrains/Arend, GitHub

本記事の議論の流れ

青い枠が、出発点です。 1.12.0 の告知文から始めます。

金色の枠が、本記事の中心です。 規則の照合、新しい概念の解説、検証結果。

赤い枠が、制約です。 1.12.0 の jar が入手できないこと、そしてドキュメントと論文のあいだに不整合があること。

緑の枠が、到達点です。 入手できた時点で再検証する、という約束。

本記事の読み方

関心 どこから読むか
1.12.0 で何が変わったのかを、まず知りたい 第１部
第６回の記述が正しいままかどうかを知りたい 第２部
「宇宙レベルに束縛されない型」とは何かを知りたい 第３部
なぜ 1.12.0 を実機で試せないのか、ドキュメントと論文がなぜ食い違うのかを知りたい 第４部
1.10 でどこまで確かめられたのかを知りたい 第５部

第１部 ── 1.12.0 の告知内容

pic_1.jpg

告知文の全体

専任講師：
2026年8月4日、Arend の公式ブログに 1.12.0 のリリースノートが掲載されました。

（原文引用）

This release includes a major internal overhaul of the universe/level system, an opt-in binary caching mode for the CLI, and substantial additions to arend-lib, most notably in algebraic geometry and analysis.

（筆者による日本語訳）

このリリースは、宇宙／レベル系の大幅な内部刷新、CLI のオプトインのバイナリキャッシュモード、そして arend-lib への大幅な追加、とくに代数幾何と解析における追加を含む。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

タロウくん：
・・・３つの項目がありますね。

専任講師：
本記事で扱うのは、最初の「宇宙／レベル系の刷新」のみ です。

CLI と arend-lib の追加は、本連載シリーズの第７回目の記事で取り上げます。

宇宙系に関する２つの項目

専任講師：
告知文の “Language updates” に、宇宙系 に関する項目が２つあります。

（原文引用）

  • Introduce types not bounded by universe levels.
  • Introduce classes not bounded by universe levels, with a local override available when a definition needs to be pinned to a finite level.

（筆者による日本語訳）

- 宇宙レベルに束縛されない型を導入する。
- 宇宙レベルに束縛されないクラスを導入する。定義を有限レベルに固定する必要がある場合には、局所的な上書きが利用できる。

出典：Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

タロウくん：
・・・「宇宙レベルに束縛されない」というのが分かりません。

専任講師：
第３部で扱います。その前に、第６回の記述が 1.12.0 のドキュメントとどう対応するかを、第２部で確かめておきます。

第２部 ── Universe placement rules と、第６回の記述の照合

pic_2.jpg

第６回目の記事の記載内容は、ver1.12.0では古くなったか

タロウくん：
Arendがバージョン1.12.0で、宇宙の言語仕様を含めて大きく変わったということですか？

ということは、この連載シリーズの初回から６回目まで、Arendについて解説してきたことと、他の言語と比較したときの大きな相違点と強み・弱みも、連続シリーズをすべて書き直さないといけない(すでに公開済みの記事はArendバージョン1.11.0でしか成立しない古い内容になった)ということですか？

ここまで書いてきた記事と、先生との対話が全て内容が古くなったという理解でよろしいですか？

専任講師：
その疑問に答えるために、この第２部があります。

「大きく変わった」かどうかは、告知文の言葉だけでは判断できません。

1.12.0 のドキュメントに明文化された規則と、第６回で実機検証した内容を、１つずつ照合する必要があります。

タロウくん：
・・・照合して、一致すれば古くなっていない。

専任講師：
そうです。
一致すれば、これまでの連載記事での記述内容は、1.12.0でもそのまま有効です。

しかし、もし一致しなければ、その箇所は補足が要ります。

まず、照合を行います。

その結果を踏まえて、第５部で「変わるもの・変わらないもの」を表にします。
そして、強み・弱みがどう変わりそうかにも、第５部の末尾で答えます。

なお、質問文に「1.11.0」とありますが、本連載で実機検証に使ったのは 1.10 です。1.11.0 の告知には宇宙系の変更は書かれていません。

出典：
Arend 1.11.0 released, Arend Theorem Prover, 2025年12月11日

新設された節

専任講師：
1.12.0 のドキュメントの Universes のページに、「Universe placement rules」という節が新設されました。

型がどの宇宙に置かれるかの規則を、明示的に列挙しています。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・第６回では、その規則を実機で確かめていましたね。

専任講師：
そのとおりです。第６回では、規則が明文化されていなかったため、実機で１つずつ確かめました。

1.12.0 のドキュメントで明文化された規則と、第６回の検証結果を照合します。

照合① ── \Prop : \Set 0

（原文引用）

\Prop : \Set 0, which is the same as \Prop : \0-Type 0.

（筆者による日本語訳）

\Prop : \Set 0 であり、これは \Prop : \0-Type 0 と同じである。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

第６回の第２部で、実機で確かめました。

$ java -jar Arend.jar PRED3.ard

[ERROR] src.PRED3:1:20: Type mismatch
  Expected type: \Prop
    Actual type: \Set0
  In: \Prop

\Prop の型は \Set0。一致しています。

照合② ── $\Pi$ 型のレベル

（原文引用）

If A : \h_1-Type p_1 and B : \h_2-Type p_2, then \Pi (x:A) -> B : \h_2-Type max(p_1,p_2).

（筆者による日本語訳）

A : \h_1-Type p_1 かつ B : \h_2-Type p_2 ならば、\Pi (x:A) -> B : \h_2-Type max(p_1,p_2) である。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

第６回の第２部で、「$\Pi$ 型の大きさは、定義域と値域の大きいほう」と述べました。

$$\text{大きさ}\bigl(\Pi(x : A)., B\bigr) = \max\bigl(\text{大きさ}(A),\ \text{大きさ}(B)\bigr)$$

可述的レベル p について、max(p_1,p_2)。一致しています。

タロウくん：
・・・ホモトピーレベルは h_2 だけですね。

専任講師：
そこは、第６回では扱いませんでした。

$\Pi$ 型のホモトピーレベルは、値域 B のホモトピーレベルで決まります。定義域は関係しません。

そして、B : \Prop なら \Pi (x:A) -> B : \Prop です。第６回で扱った非可述性が、この規則から導かれます。

照合③ ── 集合の等しさの型は命題

（原文引用）

If A : I -> \h-Type p, then Path A a a' : \max(-1,h-1)-Type p. In particular, if A : \Set p, then a = a' : \Prop.

（筆者による日本語訳）

A : I -> \h-Type p ならば、Path A a a' : \max(-1,h-1)-Type p である。とくに、A : \Set p ならば a = a' : \Prop である。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

第６回の第４部で、実機で確かめました。

\func eqIsProp (A : \Set0) (x y : A) : \Prop => x = y

--- Done (89ms) ---

一致しています。

タロウくん：
・・・この規則が、「証明を持ち回らずに済む」仕組みの根拠でしたね。

専任講師：
そのとおりです。そして、1.12.0 でも同じ規則です。

照合④ ── 宇宙自身の宇宙

（原文引用）

If 0 ≤ h < ∞, then \h-Type p : (h+1)-Type (p+1).

（筆者による日本語訳）

$0 \leq h < \infty$ ならば、\h-Type p : \(h+1)-Type (p+1) である。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

本連載シリーズの第４回目の記事で、\Set0 : \1-Type1 を実機で確かめました。

$h = 0$、$p = 0$ を代入すると \Set0 : \1-Type1。一致しています。

照合⑤ ── 累積性

（原文引用）

Note that the hierarchy of universes in Arend is cumulative, that is every expression of type \Type n has also type \Type (n+1).

（筆者による日本語訳）

Arend の宇宙の階層は累積的である。すなわち、型 \Type n を持つすべての式は、型 \Type (n+1) も持つ。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

第６回の第５部で、実機で確かめました。

\func a : \Set0 => Nat
\func d : \Set1 => Nat
\func e : \Type1 => Nat

--- Done (87ms) ---

一致しています。

照合⑥ ── $\Sigma$ 型のレベル

（原文引用）

If A : \h_1-Type p_1 and B : \h_2-Type p_2, then \Sigma A B : \max(h_1,h_2)-Type max(p_1,p_2).

（筆者による日本語訳）

A : \h_1-Type p_1 かつ B : \h_2-Type p_2 ならば、\Sigma A B : \max(h_1,h_2)-Type max(p_1,p_2) である。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

第６回の第５部で、標準の HoTT が $\Sigma$ 型で hProp を作ると、ひとつ上の宇宙へ上がることを述べました。

この規則の max(p_1,p_2) が、その理由です。一致しています。

照合の結果

# 規則 第６回での対応 一致
① \Prop : \Set 0 第２部で実機確認 ○
② $\Pi$ 型は max(p_1,p_2) 第２部「定義域と値域の大きいほう」 ○
③ A : \Set p なら a = a' : \Prop 第４部で実機確認 ○
④ \h-Type p : \(h+1)-Type (p+1) 第４回の \Set0 : \1-Type1 ○
⑤ 累積的 第５部で実機確認 ○
⑥ $\Sigma$ 型は max 第５部で $\Sigma$ 型を扱った ○

タロウくん：
・・・６つとも、一致している。

専任講師：
第６回で実機検証した宇宙の規則は、すべて 1.12.0 のドキュメントと一致しています。

そして、論文の第2.2節も同じ規則を述べています。

（原文引用）

Prop ⊆ Set 0 and Prop : Set 0. [...] For X : Set n and x, y : X the type x = y lies in Prop. In particular, sets satisfy uniqueness of identity proofs. [...] Set n ⊂ Set (n + 1), Set n : Set (n + 1)

（筆者による日本語訳）

Prop ⊆ Set 0 かつ Prop : Set 0。［中略］X : Set n と x, y : X について、型 x = y は Prop に属する。とくに、集合は等しさの証明の一意性を満たす。［中略］Set n ⊂ Set (n + 1)、Set n : Set (n + 1)。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、第2.2節

1.10 の実機、1.12.0 のドキュメント、論文。三者が一致しています。

第６回の論旨は、この三者一致によって保たれます。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

なお、$\Pi$ 型のホモトピーレベルが値域だけで決まる理由については、本稿末尾のコラム欄（$\Pi$ 型のホモトピーレベルは、なぜ値域だけで決まるのか）をご参照ください。

第３部 ── 宇宙レベルに束縛されない型とは何か

pic_3.jpg

レベルなしの \Type

専任講師：
1.12.0 のドキュメントに、次の記述があります。

（原文引用）

Writing \Type without a level denotes the universe with the largest, infinite, predicative level. It is convenient for parameters whose predicative level does not matter. Note, however, that the infinite \Type is not itself a small type, so it is not a member of any \Type n (in particular, not of itself). This is what rules out contradictory circular definitions; for the same reason a definition such as \func bad : \Type => \Type is not allowed.

（筆者による日本語訳）

レベルなしで \Type と書くと、最大の、無限の可述的レベルを持つ宇宙を表す。可述的レベルが問題にならない径数に便利である。ただし、無限の \Type はそれ自体が小さな型ではないため、どの \Type n にも属さない（とくに、自分自身には属さない）。これが、矛盾を導く循環的な定義を排除する。同じ理由で、\func bad : \Type => \Type のような定義は許されない。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
先生、第６回で \Type0、\Type1 と数字が上がっていく話を伺いました。

数字のない \Type は、何段目なのですか。

専任講師：
どの段にも属さない、と定めています。

タロウくん：
・・・段の外にある。

専任講師：
第６回で、\Type0 の型は \Type1、\Type1 の型は \Type2 と、限りなく続くことを見ました。

1.12.0 では、その「限りなく続く」先を、ひとつの名前で指せるようにしました。それが、レベルなしの \Type です。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・無限のレベル。

専任講師：
そして、無限のレベルの \Type は、どの \Type n にも属しません。

タロウくん：
・・・自分自身にも属さない。

専任講師：
そうです。

本連載シリーズの第６回目の記事で、\Type0 : \Type0 を許すと矛盾すると述べました。無限のレベルの \Type についても、同じ制約が保たれています。

ドキュメントが「\func bad : \Type => \Type のような定義は許されない」と述べているのは、そのためです。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

なお、「宇宙レベルに束縛されない」という表現の厳密な意味については、本稿末尾のコラム欄（「宇宙レベルに束縛されない」の厳密な意味）をご参照ください。

1.10 では、どうだったか

タロウくん：
・・・1.10 では、レベルなしの \Type はどうなっていたのですか。

専任講師：
実機で確かめました。

＜Arend 1.10 のコード＞

\func bad : \Type => \Type

＜Arend 1.10 の型検査結果＞

$ java -jar Arend.jar SUP1.ard

--- Done (84ms) ---

通ります。

タロウくん：
・・・1.12.0 のドキュメントが「許されない」と述べている定義が、1.10 では通る。

専任講師：
1.10 では、レベルなしの \Type は「レベルを推論する」という意味でした。

型検査器が、\Type を \Type \lp \lh と読み替え、返り値の側を \Type (\suc \lp) として補います。そのため、bad が通ります。

1.12.0 では、レベルなしの \Type は「無限のレベル」を表します。無限のレベルは、どの宇宙にも属しません。そのため、同じコードが弾かれます。

1.10 1.12.0（告知）
レベルなしの \Type の意味 レベルを推論する 無限のレベル
\func bad : \Type => \Type 通る 弾かれる

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・意味が変わっている。

専任講師：
これは、記法だけでなく意味の変更です。

ただし、第６回では \Type0、\Type1 のようにレベルを付けた形を使っていました。レベルを付けた形の意味は、1.12.0 でも変わっていません。

なお、1.10 で \Type => \Type が通る仕組みについては、本稿末尾のコラム欄（1.10 で \func bad : \Type => \Type が通る理由）をご参照ください。

両方使えるのか

タロウくん：
1.12.0では1.11.0にあった宇宙レベルに束縛される型と、束縛されない型の両方を使えるのか？それとも後者しかつかえないのか？

専任講師：
両方使えます。

告知文に、次の記述があります。

（原文引用）

Introduce classes not bounded by universe levels, with a local override available when a definition needs to be pinned to a finite level.

（筆者による日本語訳）

宇宙レベルに束縛されないクラスを導入する。定義を有限レベルに固定する必要がある場合には、局所的な上書きが利用できる。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

タロウくん：
・・・「局所的な上書きが利用できる」。

専任講師：
有限レベルに固定する書き方が残っている、ということです。

そして、ドキュメントに次の記述があります。

（原文引用）

Every truncated universe must be given a (finite) predicative level. Writing \Set or \66-Type with the level omitted is an error ("Infinite level is not allowed here"). Supply a concrete level, as in \Set 0, or a level parameter.

（筆者による日本語訳）

すべての切断された宇宙には、（有限の）可述的レベルを与えなければならない。\Set や \66-Type をレベルなしで書くとエラーになる（「ここでは無限のレベルは許されない」）。\Set 0 のように具体的なレベルを与えるか、レベル径数を与えること。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・「切断された宇宙」というのは、何ですか？＿

専任講師：
\Set0 や \1-Type1 のように、ホモトピーレベルを指定した宇宙のことです。第６回で「h-型の宇宙」と呼んだものです。

タロウくん：
・・・それらは、有限レベルを付けなければならない。

専任講師：
そのとおりです。整理します。

書き方 意味 1.12.0 での扱い
\Type（レベルなし） 束縛されない型。無限レベル 使える
\Type0、\Type1 束縛される型。有限レベル 使える
\Set0、\1-Type1 束縛される型。有限レベル 使える。レベルは必須
\Set（レベルなし） ── エラー

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・では、どちらを使えばよいのですか。

専任講師：
ドキュメントは、レベルなしの \Type を「可述的レベルが問題にならない径数に便利」と述べています。

レベルを気にしなくてよい場面ではレベルなしの \Type を使い、レベルが問題になる場面では有限レベルを付ける、という使い分けです。

pic_4.jpg

タロウくん：
・・・第６回で見た \Set0 や \1-Type1 は？

専任講師：
従来どおりです。

変わったのは、切断されていない \Type の扱いだけ です。

なお、質問文に「1.11.0にあった」とありますが、1.11.0 の告知には宇宙系の変更は書かれていません。1.10 と 1.11.0 のあいだで、宇宙系は変わっていないと筆者は理解しています。

出典：
Arend 1.11.0 released, Arend Theorem Prover, 2025年12月11日

注意：
「両方使える」は、告知文とドキュメントに対する筆者の解釈です。

1.12.0 の jar で実機検証できていません。
また、既定がどちらなのかは、告知文からは分かりません。

さらに、第４部で述べるとおり、論文はドキュメントと異なる記法を述べています。論文の記法（\lp \lh \plevels）も 1.12.0 で使えるかどうかは、確認できていません。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

第４部 ── GitHub とブログの不整合

pic_5.jpg

確認した事実

専任講師：
2026年9月5日に、次を確認しました。

項目 状態
公式ブログ 1.11.0（2025年12月11日）、1.12.0（2026年8月4日）を告知
公式ドキュメント 1.12.0 の内容に更新されている
JetBrains/Arend の最新タグ v1.10
JetBrains/Arend の master の build.gradle.kts version = "1.10.0"
JetBrains/arend-lib の最新タグ v1.10.0
GitHub releases/latest の Arend.jar 1.10。本連載で使用したものと MD5 が一致
IntelliJ Arend プラグイン 2025年12月22日に更新

出典

タロウくん：
・・・ブログは 1.12.0 を告知しているのに、GitHub には 1.10 しかない。

専任講師：
そのとおりです。

公式ドキュメントの Downloading Arend のページは、GitHub の releases/latest から jar を取得するよう案内しています。そこから取得できるのは 1.10 です。

タロウくん：
・・・なぜですか。

専任講師：
筆者には分かりません。推測を書くことはしません。

事実として、2026年9月5日時点で、1.12.0 の jar は GitHub から取得できませんでした。

タロウくん：
・・・8月4日から１か月経ちましたが、1.12.0 はまだリリースが完了していないのですか。

専任講師：
分かりません。

ブログの題名は「Arend 1.12.0 released」です。「予告」ではなく、「リリースした」と述べています。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

しかし、配布物が見つかりません。

確認先 状態（2026年9月5日）
GitHub releases/latest 1.10
GitHub tags v1.10 が最新
GitHub master version = "1.10.0"
IntelliJ プラグイン（JetBrains Marketplace） 1.12.0 が 2026年7月30日に公開されている（次の節で扱います）

出典：JetBrains/Arend, GitHub、Arend Plugin for JetBrains IDEs, JetBrains Marketplace

タロウくん：
・・・「リリースした」と述べているのに、配布物がない。

専任講師：
考えられる可能性を、４つ挙げます。

# 可能性 確認結果
① IntelliJ プラグインに同梱されている 確認済み。次の節で述べる
② JetBrains の内部リポジトリで配布されている ①により不要。配布は Marketplace という公開の場所で行われている
③ GitHub へのタグ付けが遅れている 未確認。Marketplace に7月30日からあるのに GitHub にない理由は分からない
④ ブログの投稿が、配布物の公開より先行した 否定された。プラグインは7月30日、ブログは8月4日で、配布物のほうが先

①は、以下から確認しました。

①について、IntelliJ Arend プラグインは、Arend の型検査器を同梱しています。
本記事執筆者は JetBrains Marketplace（https://plugins.jetbrains.com/plugin/11162-arend/versions/stable ）から 1.12.0 のプラグインの zip を取得し、解凍して確認しました。

確認の結果は、次の節で述べます。

可能性①の確認 ── IntelliJ プラグインに同梱されている

専任講師：
本記事の執筆中に、可能性①を確認した。

JetBrains Marketplace の Arend プラグインのページに、次の表示があります。

Plugin Versions
Compatibility: IntelliJ IDEA
Channels: Stable

Version   Compatibility Range   Update Date
1.12.0    2026.2+               Jul 30, 2026

出典：
Arend Plugin Versions, JetBrains Marketplace

タロウくん：
・・・7月30日。ブログの 8月4日より前ですね。

専任講師：
そうです。プラグインは、ブログの投稿より５日早く公開されていました。

本記事執筆者は、このページから 1.12.0 の zip ファイル（intellij-arend-1_12_0.zip）をダウンロードし、解凍しました。*

解凍後の lib/ ディレクトリに、次の jar がありました。

jar 内容
base-1.12.0.jar 型検査器の中核
api-1.12.0.jar 拡張機能の API
proto-1.12.0.jar バイナリ形式の定義
intellij-1.12.0.jar IntelliJ プラグイン本体

base-1.12.0.jar の中の GeneratedVersion.class に、1.12.0 という文字列がありました。

つまり、1.12.0 の型検査器は、IntelliJ プラグインとして配布されています。

タロウくん：
・・・では、それを CLI として動かせば、検証５件を 1.12.0 で試せるということですね？

専任講師：
試みましたが、動きませんでした。

その理由ですが、CLI の本体である org.arend.frontend.ConsoleMain が、プラグインのどの jar にも含まれていませんでした。

プラグインは IntelliJ の中で動く前提で作られており、CLI は同梱されていないのです。

1.10 の Arend.jar の CLI と、1.12.0 の base-1.12.0.jar を組み合わせることも試しましたが、NoSuchMethodError が出ました。API が変わっています。

確認したこと 結果
1.12.0 の型検査器がプラグインに同梱されているか 同梱されている
CLI として動かせるか 動かせない。ConsoleMain が同梱されていない
1.10 の CLI と組み合わせられるか **組み合わせられない。**API が変わっている

タロウくん：
・・・型検査器はあるが、動かす手段がない。

専任講師：
筆者の環境には IntelliJ がないため、そうなります。
IntelliJ をお持ちの読者は、プラグインを入れれば 1.12.0 を試せます。

手がかり ── \lp \lh \oo の文字列が、1.12.0 の jar にない

専任講師：
動かせなくても、jar の中身は調べられます。クラスファイルに含まれる文字列を検索しました。

文字列 1.10 の Arend.jar 1.12.0 の base・intellij・api
\lp １回 ０回
\lh １回 ０回
\oo １回 ０回
\func、\Type、\Prop、\Set、\Sigma、\use、\level あり あり

タロウくん：
・・・\lp、\lh、\oo が、1.12.0 にはない。

専任講師：
確実に存在するキーワード（\func 等）は 1.12.0 の jar からも見つかります。

したがって、\lp \lh \oo が見つからないのは、検索の失敗ではない可能性が高いです。

これは、ドキュメントの記述（\lh と \oo の廃止）と整合します。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・では、ドキュメントが正しく、論文が古い。

専任講師：
そう解釈できます。しかし、決定的ではありません。

\Pi、\suc、\max も 1.12.0 の jar から見つかりませんでした。これらは 1.12.0 のドキュメントに存在する文言です。したがって、この検索方法には漏れがあります。

「\lp \lh \oo の不在は、ドキュメント側の記述と整合する」というのは、筆者の解釈です。実機で動かして確かめるまで、確定とは言えません。

この確認で、決着したこと・しなかったこと

問い 決着
1.12.0 は配布されているか **決着。**IntelliJ プラグインとして、2026年7月30日に配布されている
ドキュメントと論文のどちらが実装を反映しているか 未決着。ただし、jar の文字列と arend-skills の記述はドキュメント側と整合する（次の節）
検証５件が 1.12.0 でどうなるか **未決着。**CLI がなく、型検査器を動かせない

タロウくん：
・・・本記事では「告知」と呼んできましたが。

専任講師：
正確には「リリースを告知した」です。ブログは「released」と述べています。そして、プラグインとしては実際に配布されています。

GitHub から取得できないため、本記事の実機検証は 1.10 で行いました。本記事で「告知」と書いているのは、「ブログで述べられている」という意味であり、「配布されていない」という意味ではありません。

もうひとつの不整合 ── ドキュメントと論文

専任講師：
配布の不整合に加えて、記述の不整合があります。

論文の第3.1節は、宇宙系を次のように述べています。

（原文引用）

Universe polymorphism. Definitions are made polymorphic on universe levels: there are implicit level parameters associated with each definition.

（筆者による日本語訳）

宇宙多相。定義は宇宙レベルについて多相にされる。各定義には暗黙のレベル径数が結びつけられている。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、第3.1節

タロウくん：
・・・「暗黙のレベル径数」。ドキュメントは「存在しない」と述べていました。

専任講師：
そうです。矛盾しています。

論点 論文 ドキュメント 1.10 の実機
暗黙のレベル径数 ある（第3.1節） ない ある
\Type n k の記法 使う（第3.1.1節「\Prop is \Type n -1」） 「２つのレベルは書けない」 通る
ホモトピーレベルの多相 ある（第１節） 「多相の軸ではない」 ある
レベル多相の構文 \plevels \levels（第6.1.1節） .{l} \lp \lh

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・論文は、1.10 の宇宙系を述べている。

専任講師：
ただし、論文の第５節は 1.12.0 の CLI（-ss、-ps 等）を記述しています。同じ論文のなかで、CLI の節は 1.12.0 の内容を、宇宙系の節は従来の内容を記述しているのです。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、第５節

整理します。不整合は３つあります。

# 不整合 内容
① 配布 ブログは 1.12.0 を告知。GitHub は 1.10 のまま
② 記述 ドキュメントは新しい記法。論文は従来の記法
③ 論文内部 CLI の節は 1.12.0。宇宙の節は従来

タロウくん：
・・・どちらが正しいのですか？

専任講師：
判断の手がかりはあります。

論文の脚注14 で紹介されている arend-skills というリポジトリの中に、次の記述があります。

（原文引用）

\Type \lp \lh / \Type p h no longer exist (and \lp, \lh, \oo, \oo-Type are gone). [...] No implicit \lp/\lh: a definition is polymorphic only if it declares named level parameters after its name: \func id.{l} (A : \Type l) (a : A) => a.

（筆者による日本語訳）

\Type \lp \lh と \Type p h は、もう存在しない（\lp、\lh、\oo、\oo-Type はなくなった）。［中略］暗黙の \lp \lh はない。定義が多相になるのは、名前の直後に名前付きのレベル径数を宣言したときだけである：\func id.{l} (A : \Type l) (a : A) => a。

出典：
sxhya/arend-skills, arend-quirks/SKILL.md, 第５節

タロウくん：
・・・ドキュメントと同じことを述べていますね。

専任講師：
このファイルは、Claude Code が 1.12.0 の型検査器と組んで使うための実務ファイルです。

最終コミットは2026年8月10日で、論文完成の告知と同日です。

ファイル内の絶対パスが /home/sergey/Documents/Arend/ であることから、著者は論文の著者のひとり Sergey Sinchuk と推定されます。

資料 宇宙系の記述
ドキュメント 新記法
arend-skills 新記法。「gone」と明記
論文 第3.1節 1.10 の記法

タロウくん：
・・・論文だけが違う。

専任講師：
ドキュメントと arend-skills が一致し、論文の宇宙系の節だけが異なります。

arend-skills は実装と一緒に使う実務ファイルです。

したがって、「ドキュメントが実装を反映しており、論文の宇宙系の節は 1.12.0 に合わせて更新されていない」と解釈する根拠が強いと筆者は考えます。

先ほど述べた、1.12.0 のプラグインの jar に \lp \lh \oo の文字列がなかったことも、この解釈と整合します。

ただし、これは筆者の解釈です。

1.12.0 を実機で動かして確かめるまで、確定とは言えません。

本記事の検証の範囲

専任講師：
本記事の実機検証は、すべて Arend 1.10 で行いました。（version 1.11.0と1.12.0は動かせる資源ファイルが公開されていないため）

確かめられること

# 内容
① 1.10 で、1.12.0 のドキュメントが「許されない」と述べる定義が通るかどうか
② 1.10 で、1.12.0 のドキュメントが「存在しない」と述べる記号が使えるかどうか
③ 1.10 で、1.12.0 の新しい構文が弾かれるかどうか

確かめられないこと

# 内容
① 1.12.0 で、それらがドキュメントのとおりに振る舞うかどうか
② 1.12.0 で、第６回の検証コードが同じ結果になるかどうか

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・片側だけの検証になる。

専任講師：
そうです。1.10 の挙動を確かめ、1.12.0 のドキュメントの記述と比べることで、「何が変わったか」を示します。

「1.12.0 で実際にどうなるか」は、jar が入手できた時点で確かめます。

なお、この不整合を確認した経緯については、本稿末尾のコラム欄（ブログと GitHub の不整合を、どう確認したか）をご参照ください。

第５部 ── 検証結果

pic_6.jpg

検証した５件

専任講師：
1.12.0 のドキュメントの記述のうち、1.10 で確かめられるものを５件選びました。

# 検証 1.12.0 ドキュメントの記述
① \func bad : \Type => \Type 「is not allowed」
② \func t : \oo-Type0 => Nat 「There is no \oo-Type」
③ \func t (A : \Type \lp \lh) : \Type \lp \lh => A 「Homotopy levels are not a polymorphic axis」
④ \func t : \Set => Nat 「Writing \Set with the level omitted is an error」
⑤ \func id.{l} (A : \Type l) (a : A) => a 「using the syntax .{...}」

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

結果

＜Arend 1.10 の型検査結果＞

# 1.10 の結果 1.12.0 ドキュメントの記述 差
① 通る（Done (84ms)） 許されない あり
② 通る（Done (93ms)） 存在しない あり
③ 通る（Done (74ms)） 多相の軸ではない あり
④ 通る（Done (76ms)） エラー あり
⑤ 弾かれる（no viable alternative at input '.'） この構文で書く あり

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・５件すべてで、差がある。

専任講師：
そうです。そして、５件すべてで、1.10 の挙動は論文の記述と一致します。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、第3.1節

順に見ていきます。

① ── 第３部で扱った

レベルなしの \Type の意味が変わったことの証拠です。

② \oo ── 1.12.0 のドキュメントに存在しない

専任講師：
1.10 では、\oo はホモトピーレベルの無限大を表す記号として使えます。

1.12.0 のドキュメントは、次のように述べています。

（原文引用）

The untruncated universe (homotopy level ∞) is simply \Type p. [...] There is no \oo-Type, and it is not possible to write two levels after \Type.

（筆者による日本語訳）

切断されていない宇宙（ホモトピーレベル ∞）は、単に \Type p である。［中略］\oo-Type は存在せず、\Type のあとに２つのレベルを書くことはできない。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・第６回の記号一覧表に \oo がありました。

専任講師：
1.10 では正しく、1.12.0 では該当しません。

1.12.0 では、\oo-Type0 と書いていたものを \Type0 と書きます。

③ \lh ── 1.12.0 のドキュメントに存在しない

専任講師：
1.10 では、\lp と \lh がすべての定義の暗黙の径数として存在します。

1.12.0 のドキュメントは、次のように述べています。

（原文引用）

Homotopy levels are not a polymorphic axis; only predicative levels can be abstracted this way.

（筆者による日本語訳）

ホモトピーレベルは多相の軸ではない。可述的レベルのみが、この方法で抽象化できる。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・第６回の記号一覧表に \lh もありました。

専任講師：
同じく、1.10 では正しく、1.12.0 では該当しません。

タロウくん：
・・・ホモトピーレベルについて、多相にできなくなった。

専任講師：
そのとおりです。1.12.0 では、可述的レベルだけが多相の対象です。

④ レベルなしの \Set ── 1.12.0 ではエラー

専任講師：
第３部で述べたとおりです。

第６回で引用した公式チュートリアルのコードに、isSet \Set という形がありました。1.10 では通り、1.12.0 では通らない可能性があります。

ただし、第６回で実機検証した Set-isNotSet は \Set0 を使っており、影響を受けません。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

⑤ .{l} 構文 ── 1.12.0 の記法

専任講師：
1.10 では、.{l} は構文エラーになります。

1.12.0 のドキュメントは、次のように述べています。

（原文引用）

A definition can be made polymorphic in the predicative level by declaring one or more level parameters right after its name, using the syntax .{...}, and referring to them in universes such as \Type l: \func id.{l} (A : \Type l) (a : A) => a. There is no implicit level parameter: a definition that mentions only the bare (infinite) \Type is not level-polymorphic.

（筆者による日本語訳）

定義は、名前の直後に .{...} という構文で１つ以上のレベル径数を宣言し、\Type l のような宇宙でそれを参照することで、可述的レベルについて多相にできる：\func id.{l} (A : \Type l) (a : A) => a。暗黙のレベル径数は存在しない。無限の \Type だけに言及する定義は、レベル多相ではない。

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・1.10 の \lp が、1.12.0 では .{l} になった。

専任講師：
そして、「暗黙のレベル径数は存在しない」とあります。1.10 では暗黙だったものが、1.12.0 では明示的に書くことになりました。

1.10 1.12.0（告知）
レベル多相の書き方 \lp \lh を暗黙に使う .{l} で明示的に宣言する
例 \func id (A : \Type \lp \lh) (a : A) => a \func id.{l} (A : \Type l) (a : A) => a

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

第６回の記述で、変わるもの・変わらないもの

第６回の記述 1.10 1.12.0（告知） 扱い
\Type0 : \Type1 : \Type2 の階層 ○ ○ 変わらない
\Prop : \Set0 ○ ○ 変わらない
\Set0 の等しさの型が \Prop に属する ○ ○ 変わらない
累積性 ○ ○ 変わらない
$\Pi$ 型のレベルは max ○ ○ 変わらない
非可述性 ○ ○ 変わらない
記号一覧表の \Type「宇宙」 ○ 意味が変わる（無限レベル） 説明が要る
記号一覧表の \oo ○ 存在しない 説明が要る
記号一覧表の \lh ○ 存在しない 説明が要る
\lp の暗黙の径数 ○ .{l} 構文に変更 説明が要る

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・上の６行は変わらず、下の４行が変わる。

専任講師：
上の６行が、第６回の論旨です。下の４行が、記法です。

第６回の論旨は、1.12.0 でも成り立ちます。変わったのは記法であって、設計思想ではありません。

本当に、記法だけなのか

タロウくん：
1.12.0になって変わるのは、記法だけですか？
また、宇宙についてmajorな変更が予告されているにもかかわらず、記法だけしか変わらないのは違和感がありますね。

ちなみに、Arend開発運用チームはなぜ、記法を変えることにしたんでしょうか？v1.10.0ではなにか困りごとがあって、それを解消したかったとか、困りごとはなかったが、Arendをさらに良いものにしたかったから、でしょうか。

公開されている情報から窺い知ることができることがあれば、教えてください。

専任講師：
３つの問いに、順に答えます。

記法だけか

専任講師：
「記法だけ」という言い方は、正確ではありませんでした。訂正します。

告知文は「宇宙／レベル系の大幅な内部刷新」と述べています。

（原文引用）

a major internal overhaul of the universe/level system

（筆者による日本語訳）

宇宙／レベル系の大幅な内部刷新

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

「内部」とあります。型検査器の内部で、宇宙とレベルをどう扱うかが刷新された、ということです。

タロウくん：
・・・内部が変わった。

専任講師：
しかし、その内部の詳細は、告知文にもドキュメントにも書かれていません。筆者が確認できるのは、外から見える変化だけです。

何が 変わったか 根拠
型検査器の内部 変わった（告知による） 告知文の「internal overhaul」
宇宙の規則（どの型がどの宇宙に置かれるか） 変わっていない 第２部で照合した６規則
記法（\oo、\lh、.{l}、数字なしの \Type） 変わった 第５部で検証した５件

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日、Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・「記法だけ」ではなく、「外から見える変化は記法だけ」。

専任講師：
そのとおりです。内部で何が変わったかは、本記事では分かりません。

しかし、外から見える規則が変わっていないことは、第２部で確かめました。第６回の論旨が保たれるのは、そのためです。

タロウくん：
では、外から見えない部分で、v1.12.0で変わった点はあるのですか？

また、宇宙以外の部分で、v1.12.0で変わったことは？

専任講師：
２つの問いについて、ひとつひとつ答えていきます。

まず、外から見えない部分について。

告知文は「internal overhaul」と述べるだけで、内部の何がどう変わったかは書いていません。ドキュメントにも、内部の実装についての記述はありません。

したがって、筆者には分かりません。

GitHub の master ブランチのソースコードを 1.10 のものと比べれば、内部の変更を追えるかもしれません。

しかし、第４部で述べたとおり、master は 1.10.0 のままです。比べる対象がありません。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

次に、宇宙以外の部分について。

告知文には、宇宙系以外にも多くの変更が書かれています。
本記事では扱いませんが、一覧にします。

分類 変更
言語 中置演算子の前置適用を禁止。単一引数への適用は右セクションとして解釈
プラグイン IntelliJ platform 2025.3 および 2026.2 に対応。JetBrains Educational plugin に対応（コース作成、プロジェクト生成、課題検査）。Find Usages のフリーズ、フォーマッタの性能問題を修正
CLI --serialize によるバイナリキャッシュ。-ss（記号検索）、-ps（証明探索。従来は IDE 限定）、-fu（使用箇所検索）、-ch（クラス階層）、-sc（スコープ）。すべて --json 出力に対応。REPL の改善。個別定義の型検査
arend-lib 代数幾何（scheme site、affine scheme、Spec、Proj、局所環付きロケール）。解析（冪級数の Cauchy 積、exp、log、sin、cos、cos π = -1、複素数の Banach 代数）。Noether 環、Hilbert の基底定理、テンソル積。bar 帰納法、扇定理。natarith・intarith メタ

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

タロウくん：
・・・宇宙以外にも、こんなに変わっている。

専任講師：
そうです。1.12.0 は、宇宙系だけの更新ではありません。

とくに、CLI の --json 出力と -ps 証明探索は、AI との連携に直結します。本連載シリーズの第７回目の記事で扱います。

arend-lib の代数幾何と解析の追加は、本連載シリーズの第４回目の記事で「弱み」とした Mathlib との差を、縮める方向の変化です。

本記事は、宇宙系の変更が第６回の記述に影響するかどうかに絞っています。

タロウくん：
ということは、v1.12.0に関する公式情報から判明した変更点は、先生が教えてくれたことだけ、ということですか？

専任講師：
公式情報として筆者が確認したのは、次の３つです。

# 公式情報 内容
① 告知文（2026年8月4日） 変更点の一覧。先ほどの表は、この告知文の内容をすべて含んでいます
② ドキュメント（Universes のページ） 宇宙の規則の明文化。本記事の第２部・第３部・第５部で引用しました
③ 論文の公開（2026年8月10日） 「The paper Theorem prover Arend is now finished」という告知

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日、Universes, Arend Documentation（リリースバージョン 1.12.0）、Paper on Arend, Arend Theorem Prover, 2026年8月10日

タロウくん：
・・・③の論文は、まだ読んでいないのですか。

専任講師：
論文は全文読みました。

**論文の第５節は、1.12.0 の CLI（--serialize、-ss、-ps 等）を記述しています。つまり、論文は 1.12.0 の内容を含んでいます。

しかし、論文の第３節は、暗黙のレベル径数、\Type n k、ホモトピーレベルの多相を述べています。

これはドキュメントと矛盾します。第４部で扱ったとおりです。

論文は、CLI については新しく、宇宙系については従来のままです。

出典：

タロウくん：
・・・では、告知文の一覧が、変更点のすべてですか。

専任講師：
告知文に書かれた変更点は、すべて先ほどの表に含めました。

しかし、告知文がすべての変更を網羅しているとは限りません。

告知文は「主な変更」を列挙するものであり、細かい修正は省かれることがあります。

タロウくん：
・・・網羅しているかどうかは、分からない。

専任講師：
分かりません。

すべての変更を知るには、ソースコードの差分を見る必要があります。

しかし、第４部で述べたとおり、GitHub の master は 1.10.0 のままで、1.12.0 のソースコードは公開されていません。

したがって、筆者に言えるのは次のとおりです。

問い 答え
公式情報で判明した変更点は、本記事で示したものだけか 告知文とドキュメントから分かる範囲では、そうです
それが変更点のすべてか **分かりません。**ソースコードが公開されていないため

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

違和感について

タロウくん：
・・・内部が大きく変わったのに、規則が変わらないというのは、ありうるのですか。

専任講師：
ありえます。むしろ、そうあるべきです。

型検査器の内部の実装を変えても、型が置かれる宇宙の規則が変わらないなら、既存のコードは同じ結果を出します。

内部を刷新しつつ、外から見える規則を保つ。それは、処理系の改修として自然な方針です。

ただし、記法が変わった４点については、既存のコードの書き換える必要が出てきます。そこは「互換性が切れた」箇所です。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

なぜ記法を変えたのか

タロウくん：
・・・では、なぜ記法を変えたのですか。

専任講師：
公開されている情報に対する筆者の解釈を、３点、挙げてみます。

（１点目）
ドキュメントに、数字なしの \Type についての説明があります。

（原文引用）

It is convenient for parameters whose predicative level does not matter.

（筆者による日本語訳）

可述的レベルが問題にならない径数に便利である。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

多くの定義では、可述的レベルがいくつであるかは問題になりません。

そのような場面で、レベルを気にせずに \Type と書けるようにした、というのが筆者の解釈です。

（２点目）
ホモトピーレベルの多相を外したことです。

（原文引用）

Homotopy levels are not a polymorphic axis; only predicative levels can be abstracted this way.

（筆者による日本語訳）

ホモトピーレベルは多相の軸ではない。可述的レベルのみが、この方法で抽象化できる。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

version 1.10 では、\lp と \lh の２つの軸で多相を扱っていました。
それが、version 1.12.0になると、可述的レベルの１軸だけになるようです。

多相の軸が減れば、型検査器が推論すべきものも減ります。

第６回で扱った Kraus の「型検査は決定可能か」という問いを思い出してください。軸を減らすことは、その方向の単純化です。

（３点目）
「暗黙のレベル径数は存在しない」としたことです。

（原文引用）

There is no implicit level parameter

（筆者による日本語訳）

暗黙のレベル径数は存在しない。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

1.10 では、すべての定義が暗黙に \lp \lh を持っていました。

書かれていないものが背後で働いている状態です。
1.12.0 では、レベル多相が要る定義だけが .{l} で明示します。

書かれていないものを減らし、書かれているものだけで意味が決まるようにする。これも、単純化の方向です。

タロウくん：
・・・困りごとがあったのか、さらに良くしたかったのか。

専任講師：
公開情報には、「困りごと」を明示した記述はありません。

GitHub の Issues を見れば、1.10 の宇宙系についての不具合報告や要望が分かるかもしれません。

問い 答え
困りごとがあったのか 公開情報からは分からない
何を目指したのか **単純化。**ドキュメントの記述から、「レベルを気にせず書ける」「多相の軸を減らす」「暗黙のものを減らす」の３つが筆者の解釈として導ける

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

タロウくん：
・・・「単純化を目指した」は、先生の解釈ですね。

専任講師：
そうです。本記事執筆者の解釈です。

開発チームが「単純化のため」と述べた文書は、筆者が調べた範囲では見つかっていません。ドキュメントの記述を、本記事執筆者がそう解釈した、ということです。

第６回のコラムの訂正

専任講師：
論文を読んで、第６回のコラムに訂正すべき箇所が見つかりました。

第６回のコラム「Arend の \Prop は、なぜ証明無関係でないのか」で、「筆者が調べた範囲では、公式資料に明示的な理由を確認できませんでした」と書きました。

論文に、理由が書かれていました。

（原文引用）

Moreover propositional proof irrelevance for P : Prop cannot be strengthened to the computational one p ≡ q, p, q ∈ P. Although it is probably consistent, it causes some issues in a type theory with h-prop elimination.

（筆者による日本語訳）

さらに、P : Prop についての命題的証明無関係を、計算的なもの p ≡ q に強めることはできない。おそらく無矛盾ではあるが、h-prop 消去を持つ型理論において、いくつかの問題を引き起こす。

出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"、第2.2節(2)(e)

タロウくん：
・・・理由は「h-prop 消去との整合」。

専任講師：
そうです。

第６回のコラムの「確認できなかった」は、筆者が論文を最後まで読んでいなかったためです。訂正します。

強みと弱みは、どう変わりそうか

タロウくん：
６回目記事まで論じてきたArendの特徴と、他の言語と比較した強みと弱みは、1.12.0の予告を読む限り、どう変わりそうなのか？

専任講師：
まず、第６回までで論じた特徴を、表にまとめます。

回 Arend の特徴 強み 弱み
第２回 区間を型の中に置いた 仕様が単純 計算しきる力がない
第３回 等しさを型として扱う 根拠を区別できる ──
第４回 階層を土台で支える 包摂的部分型付け 土台が大きい。Mathlib がない
第５回 data に道の構成子を並べる 円周が２行で書ける ──
第６回 宇宙に２つ目の軸を足した 証明を持ち回らない 宇宙の仕様が複雑

変わらないものと、変わりそうなものを分けます。

まず、変わらないものです。

第２回、第３回、第５回で論じた特徴は、1.12.0 の告知に変更がありません。

第６回目の記事で論じた「証明を持ち回らない」仕組みも、第２部で照合したとおり、宇宙の規則が変わっていないので、そのままです。

タロウくん：
・・・変わりそうなものは？

専任講師：
３つあります。

第１に、第６回で「弱み」とした「宇宙の仕様が複雑」について。

記法が整理されました。

\oo と \lh がなくなり、レベル多相は .{l} で書きます。
ただし、複雑さそのものが減ったかどうかは、実機で確かめないと分かりません。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

第２に、第４回で「弱み」とした「Mathlib がない」について。

arend-lib に代数幾何と解析が加わりました。
弱みは縮小しましたが、Mathlib との差は依然として大きいままです。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

第３に、CLI に --json 出力と証明探索が加わりました。

これは第６回までに論じていない、新しい強みです。

AI との連携の基盤になります。
本連載シリーズの第７回目の記事で扱います。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

特徴 1.12.0 での変化 強み・弱みへの影響
宇宙の仕様が複雑（第６回の弱み） 記法の整理 記法は整理された。複雑さが減ったかは未確認
証明を持ち回らない（第６回の強み） 変更なし 変わらない
Mathlib がない（第４回の弱み） arend-lib に代数幾何・解析を追加 弱みが縮小。差は依然大きい
円周が２行で書ける（第５回の強み） 変更の告知なし 変わらない
計算しきる力がない（第２回の弱み） 変更の告知なし 変わらない
CLI が型検査のみ --json、-ps を追加 新しい強み

タロウくん：
・・・強みが増えて、弱みが減った。

専任講師：
告知を読む限りは、そう見えます。

ただし、筆者は 1.12.0 を実機で試せていません。実際にどうなのかは、jar が入手できた時点で確かめます。

本記事の結論

第６回で実機検証した宇宙の規則は、すべて 1.12.0 のドキュメントと一致しています。

ドキュメントによれば、1.12.0 で変わったのは記法です。

\oo と \lh は廃止され、レベル多相は .{l} 構文で書きます。数字なしの \Type は、無限のレベルを指すようになりました。

しかし、論文は 1.10 の記法を述べています。
ドキュメントと論文のあいだに不整合があります。

開発者本人が書いたと推定される arend-skills がドキュメント側と一致しており、ドキュメント側と解釈する根拠が強いと筆者は考えますが、1.12.0 を実機で動かして確かめるまで、確定的な判断ではありません。

第６回の論旨は、1.12.0 でも成り立ちます。

宇宙の規則は、1.10 の実機、ドキュメント、論文の３者で一致しています。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）、Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

1.12.0 の jar は、2026年9月時点で GitHub から取得できませんでした。
入手できた時点で、改めて検証します。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）、Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日

次回について

本連載シリーズの第７回目（最終回）の記事では、AI による数学定理証明と Arend の親和性を扱います。

７回目の記事では、1.12.0 より前の Arend（本連載で実機検証した 1.10）と、1.12.0 の Arend（本記事で扱ったもの）を分けて論じる予定 です。

1.12.0 の CLI に加わった --json 出力と証明探索が、AI 連携にどう効くか。そこが、第７回の論点のひとつになります。

連載リンク

Appendix ── 本記事で実機検証したコード

A-1. 検証環境

処理系 バージョン 導入方法
Arend 1.10（Java 21） GitHub releases/latest から Arend.jar を取得

OS：Ubuntu 24.04

注意：
1.12.0 の jar は、2026年9月5日時点で GitHub から取得できませんでした。

A-2. Arend 1.10 で確認したこと

# ファイル コード 結果
① SUP1.ard \func bad : \Type => \Type Done (84ms)
② SUP2.ard \func t : \oo-Type0 => Nat Done (93ms)
③ SUP3.ard \func t (A : \Type \lp \lh) : \Type \lp \lh => A Done (74ms)
④ SUP4.ard \func t : \Set => Nat Done (76ms)
⑤ SUP5.ard \func id.{l} (A : \Type l) (a : A) => a no viable alternative at input '.'

A-3. 第６回で検証したコード

第６回目の記事の Appendix に掲載した14件は、すべて Arend 1.10 で検証済みです。本記事では再実行していません。

1.12.0 の jar が入手できた時点で、1.12.0 で再実行します。

A-4. 再現の手順

1. https://github.com/JetBrains/Arend/releases/latest/download/Arend.jar を取得する
2. 作業ディレクトリに arend.yaml を置く（sourcesDir: src）
3. src/ に .ard ファイルを置く
4. java -jar Arend.jar src/ファイル名.ard

【発展篇】中上級者向けのコラム

📌 中上級者向け：$\Pi$ 型のホモトピーレベルは、なぜ値域だけで決まるのか

本文の第２部で、$\Pi$ 型のホモトピーレベルが値域 B のホモトピーレベルで決まり、定義域は関係しないことを述べました。

その理由を補います。

$\Pi$ 型 \Pi (x:A) -> B の要素は、関数です。２つの関数 f、g が等しいとは、すべての x について f x = g x が成り立つことです（関数の外延性）。

したがって、f = g の型は \Pi (x:A) -> (f x = g x) と対応します。この型のホモトピーレベルは、f x = g x のホモトピーレベル、つまり B の等しさのホモトピーレベルで決まります。

定義域 A がどれほど複雑でも、関数の等しさは値域の等しさで決まるのです。

**とくに、B : \Prop なら、f x = g x は自明であり、\Pi (x:A) -> B も命題になります。**これが、本連載シリーズの第６回目の記事で扱った非可述性の根拠です。

出典：Universes, Arend Documentation（リリースバージョン 1.12.0）

📌 中上級者向け：1.10 で `\func bad : \Type => \Type` が通る理由

本文の第３部で、1.10 では \func bad : \Type => \Type が通ることを示しました。

その仕組みを補います。

1.10 では、レベルなしの \Type は \Type \lp \lh の略記です。\lp と \lh は、すべての定義が暗黙に持つレベル径数です。

したがって、\func bad : \Type => \Type は、次のように読まれます。

\func bad : \Type \lp \lh => \Type \lp' \lh'

型検査器は、\Type \lp' \lh' : \Type \lp \lh が成り立つように \lp' と \lh' を推論します。\lp' + 1 ≤ \lp であればよいので、\lp' = \lp - 1 などと推論して通します。

つまり、1.10 の bad は「自分自身を返す」のではなく、「ひとつ下のレベルの宇宙を返す」と解釈されています。矛盾はありません。

1.12.0 では、レベルなしの \Type が無限レベルを表すため、この推論が働きません。無限レベルの \Type はどの宇宙にも属さないので、返り値として置けないのです。

出典：
Universes, Arend Documentation（リリースバージョン 1.12.0）

注意：1.10 の推論の詳細は、筆者が 1.10 のドキュメントと挙動から推定したものです。1.10 のドキュメントには、この推論規則の明示的な記述を確認できませんでした。

📌 中上級者向け：ブログと GitHub の不整合を、どう確認したか

本文の第４部で、ブログは 1.12.0 を告知しているが GitHub には 1.10 しかない、と述べました。

確認した手順を記します。

# 手順 結果
① https://github.com/JetBrains/Arend/releases/latest/download/Arend.jar を取得 8,857,771 バイト
② 本連載で使用してきた Arend.jar と MD5 を比較 一致（c11d1f3674db3a35fa2d92e5c60853e4）
③ java -jar Arend.jar --version Arend 1.10
④ https://github.com/JetBrains/Arend/tags を確認 最新タグは v1.10
⑤ https://raw.githubusercontent.com/JetBrains/Arend/master/build.gradle.kts を確認 version = "1.10.0"
⑥ https://raw.githubusercontent.com/JetBrains/arend-lib/master/arend.yaml を確認 version: 1.10
⑦ https://arend-lang.github.io/arend-lib/v1.12.0/ を確認 403（アクセスできない）

GitHub API はレート制限のため使えませんでした。

推測される理由を、いくつか考えることはできます。しかし、本記事では推測を書きません。

執筆時に、IntelliJ Arend プラグインの changelog を確認し、1.12.0 がプラグインに同梱されているかどうかを調べることを、今後の課題とします。

📌 中上級者向け：「宇宙レベルに束縛されない」の厳密な意味

本文の第３部で、「宇宙レベルに束縛されない型」を「無限のレベルの \Type」として説明しました。

告知文の「types not bounded by universe levels」という表現を、もう少し正確に読みます。

**「bounded by」は「〜によって上から抑えられる」という意味です。**通常の型は、ある有限の可述的レベル n について \Type n に属します。つまり、レベル n によって上から抑えられています。

**「not bounded by universe levels」とは、どの有限レベルによっても上から抑えられない、ということです。**それが、無限レベルの \Type に属する型です。

1.12.0 のドキュメントは、無限の \Type を「the universe with the largest, infinite, predicative level」と述べています。

「largest」とあるので、有限レベルの宇宙はすべてこの中に含まれます。しかし、この宇宙自身はどの有限レベルの宇宙にも属しません。

**この構造は、集合論におけるグロタンディーク宇宙と「すべての集合のクラス」の関係に似ています。**ただし、型理論の宇宙は集合ではなく型であり、この類比は厳密ではありません。

出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日、Universes, Arend Documentation（リリースバージョン 1.12.0）

出典一覧

Arend

連載記事

検証環境

本記事に掲載したコードは、Arend 1.10（Java 21）で実機検証しました。

1.12.0 の jar は、2026年9月5日時点で GitHub から取得できませんでした。

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?