柯里-霍华德对应指出类型与逻辑同构。具体来说，类型相当于构造性逻辑。那是一种类型的居民就是一个证明。因此，类型可以被视为一个命题。换句话说，所有可以用命题逻辑或一阶逻辑编写的东西都应该用类型语言编写。
那么我的问题是如何用类型语言编写各种逻辑连接词？对于“合取（∧）”和“不相交（∨）”我会分别使用乘积类型和和类型来表示它们，对吗？但是“否定（Ø）”又如何呢？我无法弄清楚类型的否定是什么？
事实上，维基百科文章以及我能找到的大多数技术演示甚至都没有提到否定：我无法解释原因。不管怎样，这些是我找到的几篇介绍性文章，它们解释了通信如何在更基础/实用的层面上发挥作用：
特别是，这是第一篇文章中如何解释否定的：
否定。 这个连接词是最棘手的。让我们将否定视为语法糖。特别是，假设命题公式
实际上意味着这个公式：~ p。为什么？公式p -> false应该意味着~ p不成立。因此，如果pdid 成立，那么就会导致矛盾。因此，给定p，我们可以得出p的结论。这是理解构造逻辑中否定的标准方式。false鉴于语法糖，
因此对应于返回类型为~ p的函数类型。这样的函数永远不会真正返回。鉴于我们一直假设程序是完整的，这必定意味着甚至不可能调用该函数。因此，不可能构造函数输入类型的值。因此，否定对应于不可能性或矛盾的想法。empty