Isabelle中Filter.thy拓扑滤子定义疑问：为何公理为UNIV∈F而非{}∉F？

我正在学习Isabelle的Filter.thy中的拓扑滤子，其原始定义代码如下：

theory Filter
imports Set_Interval Lifting_Set
begin

subsection ‹Filters›

text ‹
  This definition also allows non-proper filters.
›

locale is_filter =
  fixes F :: "('a ⇒ bool) ⇒ bool"
  assumes True: "F (λx. True)"
  assumes conj: "F (λx. P x) ⟹ F (λx. Q x) ⟹ F (λx. P x ∧ Q x)"
  assumes mono: "∀x. P x ⟶ Q x ⟹ F (λx. P x) ⟹ F (λx. Q x)"

typedef 'a filter = "{F :: ('a ⇒ bool) ⇒ bool. is_filter F}"
proof
  show "(λx. True) ∈ ?filter" by (auto intro: is_filter.intro)
qed

我对该定义做了简化：通过λ演算的η规约，将F (λx. P x)简化为F P；同时将谓词'a ⇒ bool视为集合'a set，('a ⇒ bool) ⇒ bool视为'a set set，改写后的公理如下：

assumes conj: "P ∈ F ∧ Q ∈ F ⟹ Q ∩ P ∈ F"
assumes mono: "P ⊆ Q ∧ P ∈ F ⟹ Q ∈ F"

但我对其中的True公理存在疑问，它等价于：

assumes True: "UNIV ∈ F"

这和我了解的标准滤子定义不符——标准滤子会要求{} ∉ F（此时原公理名True就不再贴切），而且UNIV ∈ F其实可以通过mono公理推导出来。想知道Isabelle为什么要采用这样的滤子定义？

解答 #

Isabelle的这个定义核心是包含了非真滤子（non-proper filter，也称平凡滤子）——也就是包含空集的滤子，这类滤子满足F = Pow(UNIV)（所有子集都属于滤子），设计原因主要有三点：

• 实用性：在极限、拓扑等场景中，允许非真滤子能让推理更连贯，比如用来对应“发散到全体”的边界情况，避免额外的分支判断。
• 简洁性与模块化：先定义最宽泛的滤子概念（涵盖非真滤子），再通过添加{} ∉ F的约束得到你熟悉的“真滤子”（Isabelle库中对应proper_filter），符合它先基础后特殊的模块化设计思路。
• 排除无意义情况：如果没有UNIV ∈ F公理，空集也会满足conj和mono（因为两个公理的前提都无法触发），添加该公理可以排除这种无意义的空滤子，同时自然兼容非真滤子的存在。

你提到的UNIV ∈ F可由mono推导的前提是假设F非空，但Isabelle的基础定义不预设这一点，所以直接把UNIV ∈ F作为公理是更严谨的选择。

内容的提问来源于stack exchange，提问作者alagris