龍樹の中論における空の数理化—マルティン＝レーフ型理論による三層構造—（第二稿）
概要
龍樹（Nāgārjuna）の『中論』（Mūlamadhyamakakārikā）が提示する空（śūnyatā）は、単なる「存在しない」という否定命題ではない。諸法が縁起することを認めながら、それらに自性（svabhāva）を認めることができないという構造を示すものである。さらに、空そのものを究極的実体として扱うこともできない。この「自性の否定」と「その否定の自性化の阻止」という二重の構造は、空の空性（śūnyatā-śūnyatā）として理解できる。
本稿では、この構造をマルティン＝レーフ型理論（Martin-Löf Type Theory, MLTT）を基盤として形式化する。
ただし、本稿は、龍樹の「空」そのものをマルティン＝レーフ型理論（MLTT）へ還元することを目的とするものではなく、縁起・自性の否定・空そのものの自性化の拒否という、空の論理的構造をMLTTを用いて形式化することを試みる。
また、初稿における「条件に依存しない性質は型論的に表現できない」という前提を採用しない。実際、F := λx.λc.⊤ のような条件に依存しない関数はMLTT内で容易に構成できる。したがって、「条件不変性」と「自性」を同一視することはできない。
そこで本稿では、第一に、縁起的な性質を依存型として表現し、条件間で値が変化しないことを ConditionInvariant として形式化する。第二に、これとは別に、自性を「他の条件への依存を必要としない成立根拠」という型 Svabhava として明示的に導入する。第三に、「自性を持つ対象が存在しない」という Emptiness₁ を、MLTTそのものから自動的に導出される定理ではなく、縁起の分析に対応する追加的な制約として位置づける。さらに、その制約そのものが究極的な自性として実体化されることを防ぐため、第二階の自性とその否定として MetaSvabhava と Emptiness₂ を導入する。
この構成によって、「空」は型理論そのものと同一視されない。MLTTは自性を表現することも、条件非依存的な性質を構成することもできる。しかし、空とは、そのように表現可能な自性概念に項を与えることを拒む制約である。そして、その制約自身にも自性を与えない。この自己適用的な構造に、龍樹の「空の空性」との形式的対応を見ることができる。
1 序論
龍樹の『中論』は、諸法が自性（svabhāva）を持たないことを論じる。ここでいう自性とは、単に「ある性質が変化しない」という意味ではない。あるものが他の条件によって成立するのではなく、それ自体として成立することを意味する。
したがって、「条件が変化しても同じ性質を示す」ということと、「そのものが自性によって成立している」ということは区別しなければならない。例えば、ある対象について、どの条件でも「真である」と評価される性質を考えることはできる。しかし、その性質が一定であることだけから、その対象が自性によって成立しているとは言えない。
この区別は、空を型理論によって形式化する場合に決定的に重要である。
初稿では、
F : Obj → Cond → U₀という依存型によって縁起を表現したうえで、「条件に依存しない性質」は型論的に表現できないと考えた。しかし、この主張は成立しない。例えば、
F := λx.λc.⊤とすれば、F は条件 c に全く依存しない性質を容易に定義できる。また、この F はどの条件に対しても同じ命題を返すため、条件間の不変性も自明に証明できる。
したがって、単なる条件不変性を Intrinsic として定義し、それを自性と同一視することはできない。
本稿では、この問題を受けて形式化を根本的に改める。
本稿の中心的な区別は次の三つである。
縁起――条件に依存する性質を依存型として表現すること。
条件不変性――条件を変えても性質の真偽が変化しないこと。
自性――他の条件への依存を必要としない成立根拠を持つこと。
この三つを分離したうえで、空を「自性という型に項を与えることの不可能性」として形式化する。
さらに龍樹の空の空性に対応するため、空そのものについても同じ操作を適用する。すなわち、自性を否定する制約そのものを新たな究極的実体として扱うことを禁じる。
本稿の目的は、龍樹の思想をMLTTへ還元することではない。むしろ、MLTTが提供する型・項・依存性・非居住性という構造を利用して、中論における「縁起→無自性→空の空性」という関係を、可能な限り誤解の少ない形で記述することである。
2 なぜマルティン＝レーフ型理論か
中論の構造を形式化する際には、少なくとも三つの問題を区別する必要がある。
第一に、対象についての記述と、その記述についての制約を区別する必要がある。ある対象がどのような条件で成立するかを記述することと、その対象に自性がないことを述べることは、同一の論理階層に属する単純な命題ではない。
第二に、条件依存性を明示的に表現する必要がある。縁起は単なる「原因がある」という命題ではなく、対象のあり方が複数の条件との関係において定まる構造だからである。この点で依存型は自然な表現手段になる。
第三に、「空」を単なる否定命題ではなく、ある型の非居住性として扱う必要がある。型理論では、型 A に項が存在することと、A が空であることを明確に区別できる。
ただし、ここで注意すべきなのは、MLTTの宇宙階層そのものを世俗諦・勝義諦・空の空性と同一視することではない。
標準的なMLTTでは、例えば
U₀ : U₁のような宇宙階層があり、型を分類する宇宙はさらに上位の宇宙に属する。しかし、ある命題が別の命題についての命題であるからといって、それだけで自動的に次の宇宙へ移るわけではない。
例えば、
F : Obj → Cond → U₀に対して、
∏x:Obj. ∏c:Cond. F(x)(c)が必ず U₁ に上がるわけではない。
したがって本稿では、U₀、U₁、U₂という記号を哲学的三層そのものと同一視しない。以下では、対象レベル、第一メタレベル、第二メタレベルという三層を区別し、それぞれが必要に応じてMLTTの型と宇宙によって実装されるものとする。
この修正は、数学的な宇宙階層と、哲学的な「語りの階層」を混同しないために重要である。
3 第一層：世俗諦―縁起する対象の記述
3.1 基本型
対象と条件を導入する。
Obj : U₀
Cond : U₀Obj は対象の型、Cond は対象の成立や性質に関与する条件の型である。
ここでいう条件には、物理的条件、因果的条件、認識的文脈、関係的文脈などを抽象的に含めることができる。
重要なのは、ここでは「条件」を特定の哲学的理論に固定しないことである。何を条件とみなすかは、形式化する対象に応じて決定される。
3.2 縁起の型論的表現
対象 x : Obj が条件 c : Cond のもとである性質を持つことを、依存型
F : Obj → Cond → U₀によって表現する。
すなわち、
F(x)(c)がその性質を表し、その居住性を
holds(F,x,c) := ‖F(x)(c)‖とする。
ここで ‖−‖ は命題切り捨てであり、性質の具体的な証明データではなく、その命題が成立するかどうかだけを扱う。
この構造によって、条件に依存する性質を自然に表現できる。
ただし、ここで重要な修正がある。
F : Obj → Cond → U₀という型は、条件非依存性を禁止しない。
例えば、
F₀ := λx.λc.⊤と定義できる。
この F₀ は条件 c を受け取るものの、その値は c に依存しない。したがって、依存型による縁起の表現から「条件非依存的な性質が型論的に表現できない」と結論することはできない。
これは欠陥ではない。むしろ、ここから「条件不変性」と「自性」を区別する必要が明確になる。
3.3 条件不変性
条件を変えても性質の真偽が変化しないことを、次のように定義する。
ConditionInvariant(F) : U₀
ConditionInvariant(F) :=
∏(x:Obj) ∏(c₁:Cond) ∏(c₂:Cond)
(Admissible(c₁,c₂,x)
→ (‖F(x)(c₁)‖ ↔ ‖F(x)(c₂)‖))ここで、
Admissible : Cond → Cond → Obj → U₀は、二つの条件 c₁ と c₂ が対象 x に関して比較可能であることを表す。
ConditionInvariant(F) は、「条件が変化しても F の真偽が変わらない」という意味である。
しかし、これは自性ではない。
例えば、
F₀ := λx.λc.⊤については、
ConditionInvariant(F₀)を容易に構成できる。
実際、
λx.λc₁.λc₂.λa.(id,id)によって証明できる。
したがって、
ConditionInvariant(F)から
Svabhava(x)を導くことはできない。
この反例は重要である。なぜなら、龍樹のいう自性は「いつでも同じ性質を示すこと」ではなく、「他に依存せず、それ自体として成立すること」だからである。
4 第二層：勝義諦―自性の不在
4.1 自性を別個の型として導入する
自性を表現するためには、条件不変性とは別の概念が必要である。
そこで、対象 x : Obj に対して、
Svabhava : Obj → U₀という型を導入する。
Svabhava(x) は、「xが自性によって成立する」という主張を表す型である。
ここで重要なのは、この型自体を定義できることと、その型に項が存在することを区別することである。
MLTTは、
Svabhava(x) : U₀という型を表現することを妨げない。
したがって、
自性は型論的に表現できない
という主張は採用しない。
正確な主張は、
自性という概念は型論的に表現できるが、その型が居住していることはMLTTから自動的には保証されない。
である。
さらに、ConditionInvariant(F) と Svabhava(x) は別物である。
ConditionInvariant(F)は条件間での性質の不変性を表す。
それに対して、
Svabhava(x)は対象そのものの成立様式に関する主張である。
この区別によって、F = λx.λc.⊤ という反例を自性の反例としてではなく、条件不変性と自性の混同に対する反例として正しく位置づけられる。
4.2 自性概念の意味論的条件
Svabhava(x) の意味をより明確にするため、本稿では自性を次の条件によって特徴づける。
自性とは、対象の成立根拠が、対象を成立させる他の条件への依存によって与えられるものではない、という成立様式である。
これを完全にMLTT内部の構成として還元することは、本稿の目的ではない。なぜなら、「成立根拠そのもの」を何をもって形式化するかという問題が、すでに存在論的な選択を含むからである。
したがって、
Svabhava : Obj → U₀は、自性という存在論的概念を型論上に明示的に配置するための原始的な述語型として扱う。
ここで重要なのは、これを隠れた仮定として扱わないことである。
本稿は、
MLTT ⊢ ¬Svabhava(x)を主張するのではない。
むしろ、
MLTT + Emptiness₁という拡張された体系において、自性の不存在を制約として与える。
この区別によって、形式体系そのものと、そこに与える中論的制約を分離できる。
4.3 空（Emptiness₁）
第一の空を、
Emptiness₁ :=
¬(Σ(x:Obj) Svabhava(x))と定義する。
すなわち、
Emptiness₁ :
(Σ(x:Obj) Svabhava(x)) → ⊥である。
これは、
「自性」という概念が存在しない
という意味ではない。
自性という型そのものは存在する。
否定されるのは、
Σ(x:Obj) Svabhava(x)という、自性を持つ対象の存在である。
この違いは非常に重要である。
「自性という概念を考えられない」のではなく、
自性を持つ対象を成立させる項が存在しない
というのが、ここで形式化される空である。
4.4 なぜ F = λx.λc.⊤ は空を破らないのか
先ほどの反例をここで検討する。
F₀ := λx.λc.⊤について、
ConditionInvariant(F₀)は成立する。
しかし、
Svabhava(x)はそこから導出されない。
したがって、
ConditionInvariant(F₀)から
Σ(x:Obj) Svabhava(x)を構成することはできない。
この結果、F₀ は Emptiness₁ に対する反例ではない。
むしろ、この反例によって、
条件不変性 ≠ 自性という区別が形式的に明らかになる。
これは本稿の形式化における重要な修正点である。
5 空の空性―空そのものを自性化しない
5.1 なぜ第二段階が必要なのか
Emptiness₁ によって自性を持つ対象の存在を否定したとしても、そこで議論を止めれば新たな問題が生じる。
すなわち、
「自性がない」というこの原理こそが、究極的に正しい自性を持つのではないか
という問題である。
これは龍樹が「空もまた空である」とする構造に対応する。
したがって、次の段階では Emptiness₁ 自身を含む、第一層についての制約や理論を対象化し、その自性化を禁止する必要がある。
5.2 第一メタレベル
第一メタレベルでは、対象レベルについての制約を扱う。
ここでは、対象レベルの命題を一つの型として扱うために、必要な範囲で上位宇宙を用いる。
例えば、
T : U₁を第一メタレベルの理論・制約・命題体系の型とする。
ここで重要なのは、U₁ がそのまま「勝義諦」という意味ではないことである。
U₁ はMLTTの宇宙であり、
その宇宙に住む型を、対象レベルについて語るメタレベルの対象として利用する
という形式的役割を持つ。
5.3 Admissible₂
第一メタレベルにおける比較関係を、
Admissible₂ : U₁ → U₁ → U₀とする。
ここでは、初稿と異なり、Admissible₂ 自体を U₁ に置く必要はない。
必要なのは、二つのメタレベルの枠組み T₁ と T₂ が比較可能であるかを命題として記述することである。
最低限、
Adm2-Refl :
∏(T:U₁) Admissible₂(T,T)だけを仮定する。
つまり、
少なくとも一つの枠組みは、それ自身との比較可能性を持つ
という最小限の条件だけを認める。
対称律や推移律は、最初から与えない。
ただし、この点について重要な留保が必要である。
初稿では、推移律や対称律を導入すると必然的に「空の実体化」が起こると主張した。しかし、Admissible₂ の意味を具体的に定義しないままでは、このことを一般的なMLTTの定理として示すことはできない。
したがって以下では、
推移律・対称律を加えれば必ず破綻する
とは主張せず、
特定の意味論を与えた Admissible₂ において、それらの公理が究極的視点を導入する場合がある
という限定された主張に改める。
これは形式的厳密性のために必要な修正である。
5.4 第二の自性
第一層の自性と同じ問題が、メタレベルでも発生する。
そこで、メタレベルの対象 P に対して、
MetaSvabhava : U₁ → U₀という型を導入する。
MetaSvabhava(P) は、
Pが第一メタレベルにおいて、他の比較枠組みに依存せず、それ自体として究極的な成立根拠を持つ
という主張を表す。
ここでも、
Admissible₂(T₁,T₂)のもとでPの値が変わらないことと、
MetaSvabhava(P)は同一ではない。
したがって、初稿の Intrinsic₂ に相当する条件不変性をそのまま二階自性と呼ぶことはしない。
5.5 空の空性（Emptiness₂）
第二の空を、
Emptiness₂ :=
¬(Σ(P:U₁) MetaSvabhava(P))とする。
すなわち、
Emptiness₂ :
(Σ(P:U₁) MetaSvabhava(P)) → ⊥である。
これは、
「第一層の自性を否定する原理そのものが、究極的な自性を持つ」
という事態を拒む。
したがって、
Emptiness₁は絶対的な実体ではない。
さらに、
Emptiness₂も、それ自体を新たな究極的原理として固定してはならない。
この意味で、
Svabhava
↓ 否定
Emptiness₁
↓ 自性化を拒む
Emptiness₂という構造が得られる。
ここでの重要な点は、空が「究極的に存在する何か」へ変化していないことである。
6 「空こそ究極真理」という主張の位置づけ
例えば、
P_abs : U₁を、
「Emptiness₁ が究極的な成立原理である」
という主張として定義することができる。
しかし、P_abs が存在することと、
MetaSvabhava(P_abs)が成立することは別である。
後者を構成するには、P_absが第一メタレベルにおいて他の成立条件に依存しない究極的な成立根拠を持つことを示さなければならない。
したがって、
P_abs : U₁だけから、
MetaSvabhava(P_abs)を導くことはできない。
もし追加の公理や意味論によって
m : MetaSvabhava(P_abs)が与えられたなら、
Emptiness₂(P_abs,m) : ⊥を得ることができる。
つまり、空の空性は、
「空という概念を語ること」
を禁止するのではない。
禁止するのは、
空を自性を持つ究極的実体として成立させること
である。
これは中論における空の空性との対応を、初稿より明確に表現する。
7 「薬を捨てる」と形式体系の限界
ここまでの形式化によって、空は二段階の制約として記述される。
第一段階では、
Emptiness₁ :
¬(Σx:Obj Svabhava(x))によって対象の自性化を拒む。
第二段階では、
Emptiness₂ :
¬(ΣP:U₁ MetaSvabhava(P))によって、その拒否原理自身の自性化を拒む。
ここで重要なのは、Emptiness₂ をさらに「究極的に正しい原理」として固定しないことである。
もし、
MetaMetaSvabhava(Emptiness₂)のような第三段階を導入すれば、同じ構造を再び適用できる。
この操作を無限に続けることは、MLTTの宇宙階層そのものが示しているように可能である。
しかし、本稿はこれを無限階層の存在論として提示するものではない。
龍樹にとって重要なのは、空という薬を新たな実体として握りしめないことである。
したがって、
さらに上位の空を探し続ける
こと自体が、本稿の目的ではない。
「空の空性」は、第三の究極的実体を発見することではなく、空そのものへの執着を解除する操作として理解される。
この意味で、龍樹の「薬を捨てる」という比喩は、型理論上では「制約をさらに究極的対象として固定しない」というメタ理論的態度に対応する。
8 三層構造の整理
本稿の形式化は、次のように整理できる。
層型論的内容哲学的対応第一層Obj, Cond, F : Obj → Cond → U₀世俗諦・縁起第一層の制約Svabhava : Obj → U₀ と Emptiness₁無自性・空第二層P : U₁、メタレベルの比較空についての語り第二層の制約MetaSvabhava と Emptiness₂空の空性さらに上必要ならさらにメタ化可能ただし究極化しない
ここで「U₀＝世俗諦、U₁＝勝義諦、U₂＝空の空性」という単純な同一視は行わない。
より正確には、
世俗諦・勝義諦・空の空性という哲学的区別が、MLTTにおける型・メタ型・メタメタ型という階層構造を利用して表現される
のである。
この区別によって、MLTTの宇宙階層そのものに哲学的意味を過剰に背負わせることを避けられる。
9 この形式化によって何が示されるのか
9.1 本質主義
Svabhava(x) という型そのものを表現することはできる。
したがって、
自性という概念は型論的に表現できない
という主張はしない。
しかし、
Emptiness₁ :
¬(Σx:Obj Svabhava(x))を追加すれば、自性を持つ対象の存在を体系上の制約として排除できる。
ここで空は、概念の消去ではなく、項の不在として表現される。
9.2 条件不変性と自性の混同
ConditionInvariant(F) は正当に構成できる。
特に、
F₀ := λx.λc.⊤について、
ConditionInvariant(F₀)が成立する。
したがって、
条件不変性そのものを自性とみなす
ことはできない。
この反例を認めることで、本稿の自性概念はより限定的かつ明確になる。
9.3 空の実体化
Emptiness₁ 自体を第一メタレベルの対象として扱うことはできる。
しかし、
MetaSvabhava(Emptiness₁)を自動的に導くことはできない。
もしこれを追加的に主張すれば、
Emptiness₂ :
¬(ΣP:U₁ MetaSvabhava(P))によって拒否される。
この構造が「空もまた空である」に対応する。
9.4 虚無論との区別
Emptiness₁ は、
¬(Σx:Obj Svabhava(x))であって、
¬(Σx:Obj TrueExistence(x))のような全面的存在否定ではない。
したがって、
Obj
Cond
Fによる世俗的な記述そのものは保持される。
空とは、
対象が存在しない
という主張ではなく、
対象を自性によって成立するものとして捉えることができない
という制約である。
これは縁起と空を対立させないために重要である。
10 Admissible₂についての限定
初稿では、Admissible₂ に推移律や対称律を追加すると形式的に必ず空の実体化が生じるとした。
しかし、これは一般のMLTTから直ちに導出される命題ではない。
例えば、単に
Admissible₂ :
U₁ → U₁ → U₀とだけ置いて、
Adm2-Refl
Adm2-Sym
Adm2-Transを追加したとしても、それだけで特定の P が MetaSvabhava(P) を持つとは限らない。
したがって、ここでは主張を限定する。
もし Admissible₂ が、
すべての比較対象を一つの同値類へまとめる、
比較関係から対象間の普遍的な可視性を導く、
特定の枠組みを全体の外部から評価できる構造を導入する、
などの意味論を持つなら、対称律や推移律が「究極的な比較視点」を密輸する可能性がある。
しかし、その破綻は Admissible₂ の具体的意味論に依存する。
したがって、
反射律のみがMLTTから数学的に必然である
とは主張しない。
より慎重には、
空を究極的な比較基準として固定しないという中論的要請から、Admissible₂ には最小限の反射律だけを与え、対称律・推移律については追加の意味論を必要とするものとして保留する
とする。
これは形式化の強度を下げるのではなく、証明されていないことを証明済みとして扱わないための修正である。
11 残された問い
本稿の形式化には、なおいくつかの限界がある。
第一に、Svabhava は原始的な型として導入されている。
これは、自性という存在論的概念を完全に型理論内部へ還元できたことを意味しない。むしろ、何を自性と呼ぶかという哲学的選択を明示的に残している。
しかし、この明示化には利点がある。
初稿のように、
ConditionInvariant(F)を密かに
Svabhavaと同一視することを避けられるからである。
第二に、Emptiness₁ はMLTTそのものから導出される定理ではない。
より正確には、
MLTT + Emptiness₁という拡張体系を考えている。
これは重要な制限である。MLTTは自性を表現することもできるし、自性を持つ項を構成することも一般には排除しない。空という中論的主張は、そこに追加される哲学的・論理的制約である。
第三に、Emptiness₂ も同様に追加制約である。
したがって、
MLTT ⊢ Emptiness₁や、
MLTT ⊢ Emptiness₂と主張することはできない。
本稿の主張は、
MLTT
↓
自性を表現できる
↓
空を追加制約として定式化できる
↓
その制約自体の自性化も同様に拒否できるという構造にある。
第四に、MLTTの宇宙階層は原理的にはさらに上へ続く。
したがって、「空の空性」のさらに上に新しいメタレベルを構成すること自体は可能である。
しかし、それを行うことは、必ずしも龍樹の思想をより正確にするわけではない。
空の空性の役割は、究極的な第三実体を確立することではなく、空を究極的実体として握りしめることを拒むことだからである。
12 結論
本稿では、龍樹の空をマルティン＝レーフ型理論によって形式化するため、初稿の定式化を根本的に修正した。
第一に、縁起を
F : Obj → Cond → U₀という依存型によって表現した。
ただし、この型は条件非依存的な関数を排除しない。例えば、
F₀ := λx.λc.⊤が構成可能である。
したがって、条件を変えても性質が変化しないことを表す
ConditionInvariant(F)と、自性を表す
Svabhava(x)を区別した。
この区別によって、条件不変性を自性と誤認することを避けた。
第二に、自性を
Svabhava : Obj → U₀という型として明示的に表現した。
重要なのは、自性という型を表現できることと、その型に項が存在することを区別したことである。
空は、
Emptiness₁ :
¬(Σx:Obj Svabhava(x))として定式化される。
つまり、空とは「自性という概念を表現できない」ということではなく、「自性を持つ対象を成立させる項が存在しない」という制約である。
第三に、この制約自身が新たな自性として実体化されることを防ぐため、
MetaSvabhavaと、
Emptiness₂ :
¬(ΣP:U₁ MetaSvabhava(P))を導入した。
これによって、
自性がないという原理こそが究極的自性である
という「空の実体化」を拒否する構造を得た。
この構造は、
対象
↓
自性の否定
↓
空の自性化の否定という、縁起・空・空の空性の関係に対応する。
そして、この形式化が示す最も重要な点は、空が一つの究極的存在者ではないということである。
MLTTは自性を表現できる。条件非依存的な関数も構成できる。空も、追加制約として型に記述できる。しかし、空を記述できたからといって、それが究極的実体になるわけではない。
むしろ、空という制約にも自性を与えない。
したがって、本稿における「空」は、
「何もない」という対象ではない。
また、
「すべてのものの背後にある究極的実在」でもない。
それは、自性によって世界を成立させようとする構造を拒み、その拒否そのものについても同じことを行う操作である。
この意味で、型理論による空の形式化が目指すべきなのは、「空という究極的な型」を発見することではない。
むしろ、
型を作る
↓
その型に自性を与えない
↓
その制約にも自性を与えないという構造を明示することである。
龍樹の「空の空性」は、ここにおいて、単なる二重否定ではなく、形式化そのものが自らを究極化することを拒む自己適用的な制約として理解できる。
空は、型ではある。
しかし、究極的な型ではない。
そして、この「究極的な型を置かない」というところに、空の形式化が形式体系そのものを実体化しないための境界がある。
主要記号一覧
U₀, U₁, ... MLTTの宇宙階層
Obj 対象の型
Cond 条件の型
F : Obj → Cond → U₀ 条件依存的な性質
‖A‖ 命題切り捨て
Admissible 一次レベルの条件比較可能性
ConditionInvariant(F) Fの条件不変性
Svabhava(x) xが自性を持つという型
Emptiness₁ 自性を持つ対象の非存在
Admissible₂ 第一メタレベルの比較関係
MetaSvabhava(P) Pのメタレベルにおける自性
Emptiness₂ メタレベルの自性の非存在
Σ 依存和型
Π 依存積型
⊥ 空型・矛盾性Emptiness₂メタレベルの自性の非存在Σ依存和型Π依存積型⊥空型・矛盾
