如何在类型论中建模各类逻辑连接词？求否定连接词的类型表示

合取(∧)与析取(∨)的类型表示 #

• 合取(∧)：你用乘积类型表示是完全正确的。若命题A对应类型A，命题B对应类型B，那么A ∧ B对应乘积类型A × B（部分类型系统也写为(A, B)）。该类型的居民是一对值(a, b)，其中a : A是命题A的证明，b : B是命题B的证明，恰好对应合取命题“两个命题同时成立”的证明要求。
• 析取(∨)：用和类型表示同样正确。A ∨ B对应和类型A + B（或Either A B），它的居民要么是inl a（a : A，对应命题A成立的证明），要么是inr b（b : B，对应命题B成立的证明），完全匹配析取命题“至少一个命题成立”的逻辑。

否定(¬)的类型表示 #

在构造性逻辑中，¬A的核心含义是“若A成立则会导出矛盾”，对应到类型系统里就是函数类型A → ⊥：

• 这里的⊥是空类型（也叫底类型），它没有任何居民——不存在任何值属于这个类型。
• 如果存在一个函数f : A → ⊥，意味着只要你能给出A的一个证明（即a : A），就能通过f a得到空类型的居民，但空类型本就没有居民，这就说明A不可能有证明（否则会产生矛盾），刚好对应“¬A成立”的构造性解释。

举个直观的例子：如果我们同时拥有f : ¬A（即f : A → ⊥）和a : A，那么f a会是⊥的居民，这是不可能的，所以只要¬A有居民，A就不可能有居民，反之亦然。

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