章节出错了,点此刷新,刷新后小编会在两分钟内校正章节内容,请稍后再试。
库裡悖论
库裡悖论是一个悖论，其中任意断言F仅从一个自称“如果C，则F”的句子C的存在中得到证明，只需要一些看似无害的逻辑演绎规则。由于F是任意的，任何具有这些规则的逻辑都可以证明一切。这个悖论可以用自然语言和各种逻辑来表达，包括某些形式的集合论、λ演算和组合逻辑。
这个悖论以逻辑学家HaskellCurry的名字命名。由于它与Löb定理的关係，它在MartinHugoLöb之后也被称为Löb悖论。
用自然语言
“如果A，那麽B”形式的声明称为条件声明。库裡悖论使用了一种特殊的自指条件句，如下例所示：
如果这句话是真的，那麽德国与中国接壤。
儘管德国不与中国接壤，但例句肯定是自然语言句子，因此可以分析该句子的真实性。悖论由此分析而来。分析包括两个步骤。
首先，可以使用常见的自然语言证明技术来证明例句是真实的。
其次，例句的真实性可以用来证明德国与中国接壤。由于德国不与中国接壤，这表明其中一个证据存在错误。
“德国与中国接壤”的说法可以被任何其他说法取代，并且该判决仍然可以证明。因此，每个句子似乎都是可证明的。因为证明只使用了广为接受的演绎方法，而且这些方法似乎都不是错误的，所以这种情况是自相矛盾的。
非正式证明
证明条件句（“如果A，则B”形式的句子）的标准方法称为“条件证明”。在这种方法中，为了证明“如果A，则B”，首先假设A，然后通过该假设证明B为真。
为了产生库裡悖论，如上两步所述，将这种方法应用于“如果这句话是真的，那麽德国与中国接壤”这句话。这裡A，“这句话是真的”，指的是整体句子，而B是“德国与中国接壤”。因此，假设A与假设“如果A，则B”相同。因此，在假设A时，我们同时假设了A和“如果A，则B”。因此，B为真，通过modalsponens，我们已经证明“如果这句话是真的，那麽‘德国与中国接壤’是真的。”以通常的方式，通过假设假设并得出结论。
现在，因为我们已经证明了“如果这句话是真的，那麽‘德国与中国接壤’是真的”，那麽我们可以再次应用前件式，因为我们知道“这句话是真的”这个说法是正确的。这样，我们就可以推断出德国与中国接壤。
形式证明
句子逻辑
上一节中的示例使用了非形式化的自然语言推理。库裡悖论也出现在一些形式逻辑中。在这种情况下，它表明如果我们假设有一个正式的句子(X→Y)，其中X本身等价于(X→Y)，那麽我们可以用正式的证明来证明Y。这种形式证明的一个例子如下。有关本节中使用的逻辑符号的说明，请参阅逻辑符号列表。
X:=(X→Y)
假设，起点，相当于“如果这句话是真的，那麽Y”
X→X
同一律
X→(X→Y)
替换2的右侧，因为X等价于X→Y乘以1
X→Y
从3收缩
X
用1代替4
是
从5和4由modusponens
另一种证明是通过皮尔斯定律。如果X=X→Y则(X→Y)→X。这与皮尔士定律((X→Y)→X)→X和前件式暗示X和随后的Y（如上面的证明）。
因此，如果Y是一个形式系统中不可证明的陈述，那麽在该系统中没有陈述X使得X等价于蕴涵(X→Y)。相比之下，上一节表明，在自然（非形式化）语言中，对于每个自然语言语句Y，都有一个自然语言语句Z，使得Z等价于自然语言中的(Z→Y)。即，Z是“如果这句话是真的，那麽Y”。
在Y的分类已知的特定情况下，需要很少的步骤来揭示矛盾。例如，当Y是“德国与中国接壤”时，就知道Y是假的。
X=(X→Y)
假设
X=(X→假)
替换Y的已知值
X=(¬X∨假)
含义
X=¬X
身份
朴素集合论
即使底层的数理逻辑不允许任何自指语句，某些形式的朴素集合论仍然容易受到库裡悖论的影响。在允许无限制理解的集合论中，我们仍然可以通过检查集合来证明任何逻辑语句Y
X=deF{X∣X∈X→Y}.
假如说∈优先于两者→和↔，证明过程如下：
X={X∣X∈X→Y}
X的定义
X=X→(X∈X↔X∈X)
成员中等量的替代
X=X→((X∈X→Y)↔(X∈X→Y))
在双条件式的两边加一个后件（从2开始）
X∈X↔(X∈X→Y)
凝固法则（从1到3）
X∈X→(X∈X→Y)
双条件消除（从4开始）
X∈X→Y
收缩（从5开始）
(X∈X→Y)→X∈X
双条件消除（从4开始）
X∈X
Modusponens（来自6和7）
Y
Modusponens（来自8和6）
步骤4是一致集合论中唯一无效的步骤。在Zermelo-Fraenkel集合论中，需要一个额外的假设来说明X是一个集合，这在ZF或其扩展ZFC（使用选择公理）中是不可证明的。
因此，在一致的集合论中，集合{X∣X∈X→Y}假Y不存在。这可以看作是罗素悖论的一个变体，但并不完全相同。一些关于集合论的提议试图通过限制理解规则而不是通过限制逻辑规则来处理罗素的悖论，以便它容忍不属于它们自己的所有集合的集合的矛盾性质。上述证明的存在表明这样的任务并不是那麽简单，因为上述证明中使用的至少一个演绎规则必须被省略或限制。
Lambda演算
库裡悖论可以用无类型的lambda演算来表达，并由受限的最小逻辑来丰富。为了应对lambda演算的语法限制，M应表示採用两个参数的蕴涵函数，即lambda项((Ma)B)应等同于通常的中缀表示法A→B.
任意公式Z可以通过定义一个lambda函数来证明ñ:=λp.((Mp)Z)，和X:=(Yñ)，在哪裡Y表示Curry的定点组合器。然后X=(ñX)=((MX)Z)根据定义Y和ñ，因此上述句子逻辑证明可以在微积分中重複：
在简单类型的lambda演算中，不能输入定点组合子，因此不被允许。
组合逻辑
库裡悖论也可以用组合逻辑来表达，它具有与lambda演算等价的表达能力。任何lambda表达式都可以转换为组合逻辑，因此在lambda演算中翻译Curry悖论的实现就足够了。
上述术语X翻译成(r/r)在组合逻辑中，其中
讨论
Curry悖论可以用任何支持基本逻辑操作的语言来表述，这些语言还允许将自递归函数构造为表达式。支持悖论构造的两种机制是自指（从句子中引用“这句话”的能力）和朴素集合论中的无限制理解。自然语言几乎总是包含许多可用于构造悖论的特徵，许多其他语言也是如此。通常，向语言添加元编程功能会添加所需的功能。数理逻辑通常不允许明确引用它自己的句子。然而，哥德尔不完备定理的核心是观察到可以添加不同形式的自我参照；见哥德尔数。
不受限制的理解公理增加了在集合论中构造递归定义的能力。现代集合论不支持这个公理。
证明构造中使用的逻辑规则是条件证明的假设规则、收缩规则和前件式。这些都包含在最常见的逻辑系统中，例如一阶逻辑。
一些形式逻辑的后果
在1930年代，Curry悖论和相关的Kleene-Rosser悖论在表明基于自递归表达式的形式逻辑系统不一致方面发挥了重要作用。其中包括一些版本的lambda演算和组合逻辑。
Curry从Kleene-Rosser悖论开始，并推断出核心问题可以用这个更简单的Curry悖论来表达。他的结论可以说是组合逻辑和lambda演算不能作为演绎语言保持一致，同时仍然允许递归。
在对命题（演绎）组合逻辑的研究中，Curry在1941中认识到悖论的含义是暗示，在没有限制的情况下，组合逻辑的以下属性是不相容的：
组合完整性。这意味着抽象运算符在系统中是可定义的（或原始的），这是对系统表达能力的要求。
演绎完备性。这是对可推导性的要求，即在具有实质含义和前件式的形式系统中，如果Y可以从假设X中证明，那麽也有X→Y的证明。
解析度
请注意，与说谎者悖论或罗素悖论不同，库裡悖论不取决于使用的否定模型，因为它完全没有否定。因此，平行一致的逻辑仍然容易受到这种悖论的影响，即使它们不受骗子悖论的影响。
lambda演算中没有解决方案
AlonzoChurch的lambda演算的起源可能是“你如何求解方程，以提供函数的定义？”。这在等价中表达，
FX=Y⟺F=λX.Y.
如果只有一个函数，这个定义是有效的F满足方程FX=Y，否则无效。这是StephenColeKleene和HaskellCurry用组合逻辑和Lambda演算发现的问题的核心。
这种情况可以比作定义
Y=X2⟺X=Y.
只要平方根只允许正值，这个定义就很好。在数学中，一个存在量化的变量可能表示多个值，但一次只能表示一个。存在量化是方程的许多实例的析取。在每个等式中都有一个变量值。
然而，在数学中，没有自由变量的表达式必须只有一个值。所以4只能代表+2.但是，没有方便的方法将lambda抽象限制为一个值或确保存在一个值。
Lambda演算通过传递作为参数调用的相同函数来允许递归。这允许在以下情况下FX=Y有多个或没有解决方案F.
如果仅允许表示方程的单个解的lambda抽象，则可以将Lambda演算视为数学的一部分。其他lambda抽像在数学上是不正确的。
Curry悖论和其他悖论出现在Lambda演算中是因为Lambda演算被视为演绎系统的不一致。另请参见演绎lambda演算。
lambda演算项的域
Lambda演算在其自身领域内是一个一致的理论。但是，将lambda抽象定义添加到通用数学中并不一致。Lambda术语描述来自lambda演算域的值。每个lambda项在该域中都有一个值。
将表达式从数学转换为lambda演算时，lambda演算项的域并不总是与数学表达式的域同构。这种缺乏同构性是明显矛盾的根源。
不受限制的语言分辨率
有许多语言结构隐含地调用一个可能没有或有很多解的方程。这个问题的合理解决方案是将这些表达式在句法上鍊接到一个存在量化的变量。该变量以在普通人类推理中有意义但在数学中也有效的方式表示多个值。
例如，允许Eval函数的自然语言在数学上是不一致的。但是，以这种自然语言对Eval的每次调用都可以以一致的方式翻译成数学。Eval(s)到数学的翻译是
让x=x中的Eval(s)。
所以其中s="Eval(s)→y",
让x=x→y在x中。
如果y为假，则x=x→y为假，但这是假的，而不是悖论。
变量x的存在在自然语言中是隐含的。变量x是在将自然语言翻译成数学时创建的。这使我们能够使用具有自然语义的自然语言，同时保持数学完整性。
形式逻辑中的解析
形式逻辑中的论证首先假设命名（X→Y）为X的有效性。然而，这不是一个有效的起点。首先我们必须推断命名的有效性。以下定理很容易证明并表示这样的命名：
∀A,∃X,X=A.
在上面的陈述中，公式A被命名为X。现在尝试用(X→Y)为A实例化公式。但是，这是不可能的，因为∃X是在范围内∀A.量词的顺序可以使用Skolemization颠倒：
∃F,∀A,F(A)=A.
但是，现在实例化给出
F(X→Y)=X→Y,
这不是证明的起点，也不会导致矛盾。A没有其他实例导致悖论的起点。
集合论中的分辨率
在Zermelo-Fraenkel集合论(ZFC)中，无限制理解公理被一组允许构造集合的公理取代。所以库裡悖论不能在ZFC中表述。ZFC是为了应对罗素的悖论而发展起来的。