这种空集的形式化在 Agda 中是否正确？

Question

我正在关注 Haskell 通往 Agda 中的逻辑、数学和编程之路。书上写着：

The empty set is trivially a relation and is the smallest relation between two sets A and B

在 Agda 中：

data ∅ : Set where

record ⊤ : Set where

record Σ (A : Set) (B : A → Set) : Set₁ where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁

_×_ : Set → Set → Set₁
A × B = Σ A (λ _ → B)
infixr 5 _×_ _,_

Relation : Set → Set₁
Relation P = P × P → Set

有了它，我可以定义特定集合的关系：

lteℕ : Relation ℕ
lteℕ(x , y) = x ≤ℕ y where
  _≤ℕ_ : ℕ → ℕ → Set
  O ≤ℕ O = ⊤
  O ≤ℕ S y = ⊤
  S x ≤ℕ O = ∅
  S x ≤ℕ S y = x ≤ℕ y
  infixr 5 _≤ℕ_

但现在我遇到了问题，因为空集关系的签名：

不能是空集，因为我之前已经把它定义为无人居住的类型了
导致错误 Set₁ != Set when checking that the expression Set has type Set，即使使用不同的符号定义为 Ø : Relation Set，因为必须避免语言中的罗素悖论。

有没有办法在逻辑上保持一致？谢谢！

Answer 1

答案取决于你所说的集合。如果你所说的集合是指数学集合的表示，比如列表，那么空集就是用空列表表示的。

如果你所说的集合指的是 Agda Set 这意味着一种类型，那么答案有点复杂：没有 an 空类型，不过你能想到的就有很多。更准确地说，空类型的数量与您未为其提供任何构造函数的数据类型的数量一样多。问题是“我选择了哪些类型来模拟空集？”而不是“我如何模拟空集？".

这是一个强调这方面的 agda 模块的例子：首先，我有一些导入和我的模块的 header：

open import Agda.Primitive
open import Data.Nat hiding (_⊔_)

module EmptySets where

那我先从一个空类型开始，你能想到的越简单：

data Empty : Set where

从这个数据类型，可以写一个消除器：

Empty-elim : ∀ {a} {A : Set a} → Empty → A
Empty-elim ()

这基本上是说，如果 Empty 成立，任何事情都成立。

但是，我也可以选择通过定义一个类型族来将空集表示为空关系，所有类型都是空的，它们都是关系。首先，需要定义关系（我从标准库中获取定义）：

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ

那么可以定义空关系族：

data EmptyRelation {a b ℓ} {A : Set a} {B : Set b} : REL A B ℓ where

由于所有这些类型都是空的，它们也都提供了一个消除器：

EmptyRelation-elim : ∀ {a b x ℓ} {A : Set a} {B : Set b} {X : Set x} {u : A} {v : B} → EmptyRelation {ℓ = ℓ} u v → X
EmptyRelation-elim ()

因此，可以实例化此泛型以获得特定的空类型，例如，自然数上的空关系，它永远不会成立：

EmptyNaturalRelation : REL ℕ ℕ lzero
EmptyNaturalRelation = EmptyRelation

书上是这么解释的：既然关系是一对的集合，那么空类型就是这个关系中最小的：没有对的那个。

但是你也可以使用谓词而不是关系，也就是说空集是给定类型上的最小谓词：永远不成立的谓词，在这种情况下，它表示如下：

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Pred A ℓ = A → Set ℓ

data EmptyPredicate {a ℓ} {A : Set a} : Pred A ℓ where

你可能会更疯狂，决定按如下方式对空集建模：

data EmptySomething {a} {A B C D E Z : Set a} : A → B → C → D → E → Z → Set where

总而言之，agda 中没有空集，但空类型有无限可能。

至于您在问题中提供的代码，有几个不准确之处：

关系通常是在两个参数而不是参数对上定义的，如果需要，您可以对它们进行柯里化，使它们以一对作为参数。
为什么要让 lteℕ 依赖于 _≤ℕ_ 而不是直接定义它？
您应该将 lteℕ 定义为数据类型而不是 returns 底部或顶部的函数，这将允许您 case-split 在这样的将来的期限。通常，这是这样定义的（在标准库中）：
```
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n}                 → zero  ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
```

这种空集的形式化在 Agda 中是否正确？

Is this formalization of the empty set correct in Agda?

logic

set-theory

theorem-proving

agda