正本：FormalLab/Mathematics/Sets.lean

第20章：集合を述語として読む#

集合を扱う最小の操作は、ある要素がその集合に属するかを問うことです。母集団を型 A として固定すれば、部分集合 S は各 x : A に所属命題 x ∈ S を対応させる述語として読めます。この見方では、包含は含意、共通部分は連言、和集合は選言へ分解されます。

本章では集合論全体を型理論へ置き換えるのではなく、固定した母型上の述語集合を構成します。集合演算と外延性を既知の論理から導き、集合としての述語と、その述語を満たす値を保持する部分型を区別します。後の像・逆像、関係、篩型を読むための共通語彙をここで整えます。

集合を要素が満たす条件で表す#

母集団 A の部分集合 S は、各 x ∈ A について所属命題 x ∈ S を定めます。本章ではこの特性述語を直接表現し、型 α 上の集合を述語 α → Prop として形式化します。s x は「x が s に属する」という命題です。ここで α は議論する要素の母型です。集合だけを単独で持つのではなく、どの型の要素を集めているかが常に型に現れます。集合演算は論理結合子を点ごとに使うだけです。

\mathcal P(A)\;\widehat{=}\;A\to\mathsf{Prop}, \qquad x\in S\;\widehat{=}\;S(x).

ここで帽子付き等号は、Zermelo–Fraenkel集合論の冪集合と同一だという主張ではなく、本章で使う固定母型上の述語表現を示します。この表現の下で包含と演算は

S\subseteq T\;\Longleftrightarrow\;\forall x:A.\,S(x)\to T(x),

(S\cup T)(x)\;\Longleftrightarrow\;S(x)\lor T(x), \quad (S\cap T)(x)\;\Longleftrightarrow\;S(x)\land T(x)

と読めます。

集合概念	要素ごとの論理式
`s ⊆ t`	`∀ x, s x → t x`
`s ∪ t`	`fun x => s x ∨ t x`
`s ∩ t`	`fun x => s x ∧ t x`
`sᶜ`	`fun x => ¬s x`

Leankernel-checked counterpartL53–55

namespace FormalLab.Mathematics.Sets

universe u

所属を述語の適用として表す#

この表現では「集合を作る」ことは「所属条件を書く」ことです。列挙できない無限集合でも、 fun n : Nat => n % 2 = 0 のように条件を述べられます。反対に、同じ型 α 上でも異なる所属条件は異なる集合を定めます。

α の集合を、その所属述語として表す本章の定義です。

Leankernel-checked counterpartL66–67

def PredSet (α : Type u) :=
  α → Prop

s の全要素が t にも属することを包含と定義します。

Leankernel-checked counterpartL70–71

def Subset {α : Type u} (s t : PredSet α) : Prop :=
  ∀ ⦃x⦄, s x → t x

どの要素にも偽を返す空集合です。

Leankernel-checked counterpartL74–75

def Empty {α : Type u} : PredSet α :=
  fun _ => False

どの要素にも真を返す全体集合です。

Leankernel-checked counterpartL78–79

def Universal {α : Type u} : PredSet α :=
  fun _ => True

所属を選言で定める和集合です。

Leankernel-checked counterpartL82–83

def Union {α : Type u} (s t : PredSet α) : PredSet α :=
  fun x => s x ∨ t x

所属を連言で定める共通部分です。

Leankernel-checked counterpartL86–87

def Intersection {α : Type u} (s t : PredSet α) : PredSet α :=
  fun x => s x ∧ t x

所属を否定して得る補集合です。

Leankernel-checked counterpartL90–91

def Complement {α : Type u} (s : PredSet α) : PredSet α :=
  fun x => ¬s x

指定した一点だけを含む一元集合です。

Leankernel-checked counterpartL94–95

def Singleton {α : Type u} (chosen : α) : PredSet α :=
  fun x => x = chosen

自然数上の偶数全体を、所属条件で直接定めます。

Leankernel-checked counterpartL98–104

def EvenNumbers : PredSet Nat :=
  fun n => n % 2 = 0

example : EvenNumbers 4 := rfl
example : ¬EvenNumbers 3 := by
  change ¬(3 % 2 = 0)
  decide

法則：論理の証明を集合の証明として再利用する#

包含 Subset s t は、集合を新しい値へ変換する関数ではありません。s x という所属証明を受け取るたびに t x を返す、要素ごとの含意です。このため包含の反射性は恒等関数、推移性は証明関数の合成と同じ形になります。

集合包含の反射性です。

Leankernel-checked counterpartL115–116

theorem subsetReflexive {α : Type u} (s : PredSet α) : Subset s s :=
  fun {_} membership => membership

集合包含の推移性です。

Leankernel-checked counterpartL119–121

theorem subsetTransitive {α : Type u} {s t u : PredSet α}
    (st : Subset s t) (tu : Subset t u) : Subset s u :=
  fun {_} membership => tu (st membership)

一元集合が s に含まれることと、その一点が s に属することは同値です。

Leankernel-checked counterpartL124–131

theorem singletonSubset_iff {α : Type u} {chosen : α} {s : PredSet α} :
    Subset (Singleton chosen) s ↔ s chosen := by
  constructor
  · intro subset
    exact subset rfl
  · intro membership _ equality
    cases equality
    exact membership

要素ごとの所属が同値なら、二つの述語集合は等しい。

Leankernel-checked counterpartL134–137

theorem extensionality {α : Type u} {s t : PredSet α}
    (sameMembers : ∀ x, s x ↔ t x) : s = t := by
  funext x
  exact propext (sameMembers x)

和集合の交換性は選言の交換性です。

Leankernel-checked counterpartL140–147

theorem unionCommutative {α : Type u} (s t : PredSet α) : Union s t = Union t s := by
  apply extensionality
  intro x
  constructor
  · intro membership
    exact Or.elim membership Or.inr Or.inl
  · intro membership
    exact Or.elim membership Or.inr Or.inl

共通部分の交換性は、所属証明の二成分を入れ替えて示します。

Leankernel-checked counterpartL150–156

theorem intersectionCommutative {α : Type u} (s t : PredSet α) :
    Intersection s t = Intersection t s := by
  apply extensionality
  intro x
  constructor <;> intro membership
  · exact ⟨membership.2, membership.1⟩
  · exact ⟨membership.2, membership.1⟩

unionCommutative の証明は、集合の等式を二段階で分解します。まず funext に対応して任意の要素 x を固定し、次に propext に対応して二つの所属命題の同値を示します。その内部は選言の交換だけです。この「集合等式 → 所属同値 → 命題論理」という翻訳が、述語集合を使う際の基本手順です。

De Morgan則のうち、和集合の補集合は構成的に共通部分へ分配できます。

Leankernel-checked counterpartL167–175

theorem complementUnion {α : Type u} (s t : PredSet α) :
    Complement (Union s t) = Intersection (Complement s) (Complement t) := by
  apply extensionality
  intro x
  constructor
  · intro notEither
    exact ⟨fun sx => notEither (Or.inl sx), fun tx => notEither (Or.inr tx)⟩
  · intro ⟨notS, notT⟩ either
    exact either.elim notS notT

排中律を使えば、集合とその補集合の和は全体集合になります。

Leankernel-checked counterpartL178–186

theorem unionComplement {α : Type u} (s : PredSet α) :
    Union s (Complement s) = Universal := by
  apply extensionality
  intro x
  constructor
  · intro _
    exact True.intro
  · intro _
    exact Classical.em (s x)

述語集合と集合論#

集合の外延性は、所属が同値なら述語として等しいという funext と propext の合成です。また補集合の定義 ¬s x 自体は構成的ですが、s ∪ sᶜ = Universal のような法則は全ての所属命題について排中律を使います。演算の定義と法則の論理的強さを分けます。

mathlibの Set α も述語を基礎にしますが、ここでは所属の仕組みを定義から追えるよう PredSet を使います。

述語集合 PredSet α と、後に扱う篩型 {x : α // s x} も区別します。前者は所属を尋ねる述語、後者は要素と所属証明を組にした型です。集合の要素を実際の入力として要求する段階で、この二つの見方を橋渡しします。

要点#

型 α 上の集合は所属述語 α → Prop として表せる。
包含は要素ごとの含意、和・共通部分・補集合は選言・連言・否定である。
集合の等式は、各要素について所属命題が同値であることへ分解する。
集合演算の定義が構成的でも、特定の法則が古典論理を要求する場合がある。
述語としての集合と、所属証明を持つ要素の型は同じ対象ではない。

研究史と文献案内#

集合論はCantorとDedekindの1870年代以後の研究から発展し、Zermeloは1908年に公理化を提示しました [ZER08]。本章の PredSet α は一つの既定の型の部分を特性述語で表すもので、 Zermelo集合論の累積的な集合宇宙ではありません。歴史的展開は付録Cの二次文献、型理論内の集合・型・setoidの差は [ML84] を参照してください。

問題#

集合演算を論理式へ翻訳する#

Subset s t と Intersection s (Union t u) x を、集合記号を使わない量化・含意・連言・選言の式へ翻訳せよ。次に積集合の交換性を連言の交換から証明し、集合の証明が要素を固定した命題の証明へ還元される順序を示す。

同じ方法で Subset (Singleton x) s ↔ s x をLeanで証明する。数式中の各推論が、関数適用、等式による書換え、含意のどれとして現れるかを対応づけること。

外延性が重ねて使われる箇所を追う#

二つの述語 s t : α → Prop が同じ集合を表すための条件を述べ、関数外延性と命題外延性をどの順に使えば s = t が得られるかを導出せよ。要素ごとの同値、命題の等式、関数の等式を混同せず、三段階に分けて書くこと。

Leanの集合が述語として表現されることから従う実装上の説明と、数学における集合外延性の原理を区別する。どの段階がLeanの表現選択に依存するかを指摘できれば完了である。

補集合と古典論理の境目を特定する#

s ∪ sᶜ = Universal の通常の証明を要素ごとの命題へ展開し、排中律を用いる正確な一行を指せ。一方、s ∩ sᶜ = Empty は同じ古典原理なしに証明できることを示し、否定の導入と排中律の違いを説明する。

最後に、構成的に証明できる包含関係と、古典論理を仮定して初めて等号まで強められる関係を一つずつ挙げる。古典性を集合記号の見かけではなく、対応する論理式から判定すること。