アイリーン〈ILean〉

Ireneではない。ideal Lean 理想化Lean。

Lean	ILean	圏論	論理
A→B→C	A B → C	[A, B → C]	A⊃B⊃C or A∧B⊃C
(a:A)(b:B):C	A B ⇒ C	A, B → C	A, B → C
f (a:A)(b:B):C	f (A B) ⇒ C	f: A, B → C	f: A, B → C
(a:A)(b:B)⊢ C	A B ⊢? C	-	-
f:A → B	f ()⇒A→B	f:ε → [A→B]	f: → A⊃B

注：ターンスタイルは U+22A2 'RIGHT TAC'

檜山標準	Lean	圏論	論理
含意	含意＝関数型	指数＝内部ホム	含意
アサーション	定義ヘッド？	プロファイル	シーケント
リクエスト	ゴール	-	-

同義語：

1. 含意、条件法〈conditional〉
2. アサーション、ジャッジメント、条件付きアサーション
3. リクエスト、クエリー、要求〈requirement〉、責務〈オブリゲーション|義務〉
4. アサーション／リクエストのソース、コンテキスト、仮定、前提、
5. アサーション／リクエストのターゲット、結論、帰結

問題点：

標準形が定まらない、次の形式がある。

1. 一般復射形式： A₁, ..., A_n → B in MultiProp
2. 射形式： A → B in MultiProp
3. ポイント形式： ε → B in MultiProp
4. 対象型式： B∈Obj(MultiProp) = Obj(Prop)

さらに、

1. 一般復射形式と射形式の区別はあまり必要ではないかも。
2. ポイント形式と対象型式が区別されない。これは弊害がある。
3. 一般復射 → 射 → ポイント は、包含縮小の関係にあるが、ポイントから対象へのところでギャップがある。
4. 他に、フルカリー化形式と、そうでない形式がある。
5. 仮定のリスト（コンテキストの一種）があるとき、それを連言解釈するか、含意解釈するか、の問題もある。A, B → C を A∧B → C、→ A∧B⊃C、A → B⊃C、→ A⊃(B⊃C)

ほんとに基本的な部分が曖昧にされたままだから、教育は難しい。