- https://www.urhur.com/archives/50 第三方网站 （其内容大多翻译于维基英文https://en.wikipedia.org/wiki/Curry%27s_paradox，故该网站没有版权）
库里的悖论是一种悖论，其中仅从句子C的存在就证明了任意主张F，而句子C本身说“如果C，则F”，只需要一些显然无害的逻辑推导规则。 由于F是任意的，因此具有这些规则的任何逻辑都可以证明一切。 悖论可以用自然语言和各种逻辑表达，包括集合论，lambda微积分和组合逻辑的某些形式。 悖论以逻辑学家Haskell Curry命名。 由于它与洛伯定理的关系，它在马丁·雨果·洛伯之后也被称为洛伯悖论。 用自然语言 “如果是A，则是B”形式的声明称为有条件声明。 库里悖论使用了一种特殊的自我指称条件句，如以下示例所示： 如果这句话是正确的，那么德国与中国接壤。 尽管德国没有与中国接壤，但例句肯定是自然语言的句子，因此可以分析该句子的真实性。 悖论来自于此分析。 分析包括两个步骤。 首先，可以使用常见的自然语言证明技术来证明例句是正确的。 其次，例句的真实性可以用来证明德国与中国接壤。 因为德国不与中国接壤，所以这表明其中一个证据有误。 “德国与中国接壤”的主张可以用任何其他主张代替，并且该判决仍然可以证明。 因此，每个句子似乎都是可以证明的。 由于证明仅使用公认的推论方法，并且由于这些方法似乎都不正确，因此这种情况是自相矛盾的。 非正式证明 证明条件句子（句子形式为“如果A，那么B”的标准方法）的标准方法称为“条件证明”。 在该方法中，为了证明“如果A，则B”，首先假设A，然后在该假设下B被证明是正确的。
为了产生上述两个步骤中描述的库里悖论，请将此方法应用于句子“如果该句子为真，则德国与中国接壤”。 这里的A，“这句话是正确的”，是指整个句子，而B是“德国与中国接壤”。 因此，假设A与假设“如果A，则B”相同。 因此，在假设A中，我们同时假设了A和“如果A，则B”。 因此，根据惯用法，B是正确的，并且我们已经证明“如果这句话是正确的，那么“德国与中国接壤”就是正确的。” 通常，通过假设和推论得出结论。
现在，由于我们已经证明“如果这句话是正确的，那么’德国毗邻中国’是正确的”，那么我们就可以再次采用惯用语，因为我们知道“这句话是正确的”主张是正确的。 这样，我们可以推断出德国与中国接壤。 正式证明 句子逻辑
上一节中的示例使用了非形式化的自然语言推理。 库里悖论也出现在形式逻辑的某些变体中。 在这种情况下，它表明如果我们假设存在一个形式句子（X→Y），其中X本身等于（X→Y），那么我们可以用形式证明来证明Y。 这种形式证明的一个例子如下。 有关本节中使用的逻辑符号的说明，请参阅逻辑符号列表。
X：=（X→Y） 假设，起点，等同于“如果此句子为真，则为Y” X→X 身份定律 X→（X→Y） 因为X等于X→Y等于1，所以用2代替右边 X→Y 从3起收缩 X 用1代替4 ÿ 从5和4通过modus ponens
另一种证明是通过皮尔斯定律。 如果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}。
假设ε优先于→和both，则证明按如下方式进行：
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 方式（6和7） ÿ 方式（8和6） 步骤4是一致集理论中唯一无效的步骤。 在Zermelo–Fraenkel集理论中，将需要一个额外的假设来说明X是一个集，这在ZF或其扩展ZFC（带有选择公理）中无法得到证明。
因此，在一致集合论中，对于假Y，不存在集合{x ∣ x∈x→Y}。这可以看作是罗素悖论的一种变体，但并不完全相同。 关于集合论的一些建议试图解决罗素的悖论，不是通过限制理解规则，而是通过限制逻辑规则，以便它可以容忍所有非其自身集合的集合的矛盾性质。 像上面的证明这样的证明的存在表明这样的任务不是那么简单，因为上面证明中使用的至少一个推导规则必须被省略或限制。
λ演算
咖喱的悖论可以用无类型的Lambda演算来表达，并通过有限的最小逻辑来丰富。 为了应付lambda演算的句法限制，m表示包含两个参数的蕴涵函数，即lambda项（（m A）B）应等效于通常的中缀符号A→B。任意公式Z可以是通过定义λ函数N：=λp证明。 （（mp）Z）和X：=（YN），其中Y表示Curry的定点组合器。 然后，根据Y和N的定义，X =（NX）=（（m X）Z），因此可以在演算中复制以上的句法逻辑证明：
X（（m X）X）由最小逻辑公理A→A⊢（（m X）（（m X）Z）），因为X =（（m X）Z）⊢（（m X）Z）由极小逻辑⊢X的定理（A→（A→B））⊢（A→B），因为X =（（m X）Z）⊢Z由模态A构成，（A→B）⊢B由X和（（ m X）Z）
在简单类型的lambda演算中，定点组合器无法键入，因此不被接受。 组合逻辑 库里悖论也可以表达为组合逻辑，其表达能力与λ演算具有同等的表达力。 任何lambda表达式都可以转换为组合逻辑，因此在lambda微积分中对Curry悖论的实现进行翻译就足够了。 上述项X在组合逻辑中转换为（rr），其中
r = S（S（K m）（SII））（KZ）;
因此 （rr）＝（（m（rr））Z）。 讨论区
Curry悖论可以用支持基本逻辑运算的任何语言来表达，这些语言还允许将自递归函数构造为表达式。 支持悖论建构的两种机制是自我参照（从句子中引用“这个句子”的能力）和天真集合论中的不受限制的理解。 自然语言几乎总是包含许多可用于构造悖论的功能，就像许多其他语言一样。 通常，向语言添加元编程功能会添加所需的功能。 数学逻辑通常不支持显式引用其自身的句子。 然而，哥德尔不完备性定理的核心是观察到可以添加不同形式的自我参照。 参见哥德尔编号。
无限制理解的公理增加了在集合论中构造递归定义的能力。 这个公理不受现代集合论的支持。 证明的构造中使用的逻辑规则是条件证明的假设规则，收缩规则和惯用方式。 这些包含在最常见的逻辑系统中，例如一阶逻辑。 一些形式逻辑的后果 在1930年代，Curry悖论和相关的Kleene-Rosser悖论在显示基于自递归表达式的形式逻辑系统不一致方面起了主要作用。 这些包括lambda演算和组合逻辑的某些版本。 Curry从Kleene-Rosser悖论开始，推论核心问题可以用这个简单的Curry悖论来表达。 他的结论可以说是说，组合逻辑和拉姆达演算不能作为演绎语言保持一致，而仍然允许递归。 在对有害（演绎）组合逻辑的研究中，库里（Curry）在1941年认识到这种悖论的含义是，它无限制地暗示了组合逻辑的以下特性是不兼容的： 组合完整性。 这意味着抽象运算符在系统中是可定义的（或原始的），这是对系统表示能力的要求。 演绎完整性。 这是对可导性的要求，即在具有实质性含义和惯用语形式的形式系统中，如果根据假设X证明Y，则也存在X→Y的证明。 术语 自然语言和数学逻辑都基于断言某些陈述为真。 该语句可以表示为逻辑（或布尔）表达式（或公式），可以对其进行评估以得出true或false的值。 语句是一种语句或逻辑表达式，在被求值时将声明其为真值。 也可以以更复杂的方式考虑示威。 陈述可以通过您主张或相信的陈述以及确定性的等级来限定。 但是，对于逻辑，上面给出的简单定义就足够了。 存在问题 这个悖论类似于， 骗子的悖论 罗素悖论 其中每个悖论都试图给不存在的事物起一个名字。 这些悖论都试图为方程的解给出名称或表示， X =¬X 请注意，悖论不是强制执行¬X语句而引起的，因为这样的语句将是谎言。 它源于对声明的审议和命名。 悖论是通过将¬X形式的表达式命名或表示为X来产生的。在Curry悖论的情况下，否定是由蕴涵构成的， X = X→假=¬X∨假=¬X 布尔变量X的域是集合{true，false}。 但是，对上述方程式的解决方案都不为真或为假。 因此，宣称X的存在一定是错误的，并且将¬X表达式命名为X是一个谎言。
矛盾的是，总是可以构造一个其值不存在的表达式。 这可以使用“ this statement”来实现，但是还有许多其他语言功能，这些功能允许构建不存在的表达。
表达矛盾的语言资源 可以用支持基本逻辑运算的任何语言来表达Curry的悖论，这也允许将自动递归函数构造为表达式。 下面的列表提供了一些支持悖论构造的机制，但是列表并不详尽。 自我参考； “这个句子”。 通过包含名称的表达式的命名法。 应用朴素集理论（不受限制的理解）。 Lambda表达式。 一个单词中的一个Eval函数。 构建证据所使用的逻辑规则是： 假设规则 收缩 方式 然后可以使用自动递归函数来定义终止计算，该终止计算的值不是方程的解。 在库里悖论中，我们使用蕴涵来构造一个否定词，该否定词会建立一个没有解的方程式。 然后，递归表达式表示一个不存在的值。 逻辑定律仅对{true，false}中的布尔值有效，因此对表达式的任何保留都可能是错误的。 自然语言几乎总是包含许多可用于构造悖论的资源，就像许多其他语言一样。 通常，为一种语言添加元编程功能会添加必要的功能。 数学逻辑通常不容许明确引用其自身的句子。 但是，哥德尔不完备性定理的核心是观察到可以添加自我参照。 参见哥德尔编号。 不受限制的理解公理增加了在集合论中构造递归定义的能力。 这个公理不受现代集合论的支持。 一些形式逻辑的后果 在1930年代，Curry悖论和相关的Kleene-Rosser悖论在表明基于自递归表达式的形式逻辑系统不一致方面发挥了重要作用。 λ演算 组合逻辑 Curry从Kleene-Rosser悖论开始，推论出中心问题可以用Curry的这个更简单的悖论来表达，他的结论可以说是说组合逻辑和Lambda计算不能作为一种演绎语言连贯，允许递归。 在对表示（演绎）组合逻辑的研究中，库里（Curry）在1941年认识到这种悖论的含义是，它无限制地暗示了组合逻辑的以下特性是不兼容的： 组合完整性。 这意味着抽象运算符在系统中是可定义的（或原始的），这是对系统表示能力的要求。 演绎完整性。 这是一个可推导性要求，即在具有内蕴和物质模态形式的形式系统中，如果从假设X可以推导Y，那么也存在X→Y的证明。 分辨率 本节未引用任何来源。 请通过在可靠来源中添加引文来帮助改进本节。 无法查证的内容可能被提出异议而移除。 查找来源：“ Curry的悖论” –新闻•报纸•书籍•学者•JSTOR（2019年8月）（了解如何以及何时删除此模板消息）
本部分的事实准确性存在争议。 相关讨论可以在Talk：Curry的悖论上找到。 请帮助确保有争议的陈述来源可靠。 （2019年8月）（了解如何以及何时删除此模板消息）
请注意，与说谎者悖论或罗素悖论不同，库里的悖论并不取决于所使用的否定模型，因为它是完全无否定的。 因此，即使相矛盾的逻辑不受骗子悖论的影响，但仍然容易受到这种悖论的影响。 Lambda演算中没有分辨率 阿隆佐·丘奇（Alonzo Church）的lambda演算的起源可能是“如何解决方程式，以提供函数定义？”。 这是等效的，
fx = y⟺f =λxy
如果只有一个函数f满足方程fx = y，则此定义有效，否则无效。 这是Stephen Cole Kleene和Haskell Curry通过组合逻辑和Lambda微积分发现的问题的核心。
情况可以与定义
y = x 2 x = y。
只要平方根仅允许正值，此定义就可以了。 在数学中，存在量化变量可以表示多个值，但一次只能表示一个。 存在量化是一个方程的许多实例的析取。 在每个方程式中，变量的一个值。
但是，在数学中，没有自由变量的表达式必须只有一个值和一个值。 因此4只能表示+2。但是，没有方便的方法将lambda抽象限制为一个值或确保有一个值。
Lambda演算可以通过传递与参数相同的函数来进行递归。 这允许fx = y对f有多个或没有解的情况。
如果仅允许代表一个方程式的单个解的lambda抽象，则可以将Lambda微积分视为数学的一部分。 其他lambda抽像在数学上是不正确的。 咖喱的悖论和其他悖论在Lambda演算中出现，因为被认为是演绎系统的Lambda演算的不一致。 另请参见演绎λ演算。 Lambda演算领域
Lambda演算是其自身领域中的一致理论。 但是，将lambda抽象定义添加到通用数学中并不一致。 Lambda术语描述了Lambda演算域中的值。 每个lambda项在该域中都有一个值。
当将表达式从数学转换为lambda演算时，lambda演算项的域并不总是与数学表达式的域同构。 这种同构的缺乏是明显矛盾的根源。 不受限制的语言解析 有许多语言构造可隐式调用一个可能没有解决方案或有很多解决方案的方程式。 解决此问题的合理方法是将这些表达式在语法上炼接到一个存在的量化变量。 该变量以在普通人类推理中有意义的方式表示多个值，但在数学中也有效。 例如，允许Eval函数的自然语言在数学上不一致。 但是，用这种自然语言对Eval的每次调用都可以以一致的方式转换为数学。 将Eval转换为数学是 令x = x中的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）中，无限制理解的公理被一组允许构建集的公理代替。 因此，Curry的悖论无法在ZFC中陈述。 ZFC的发展是对Russell悖论的回应。 ← 理发店悖论 → 埃皮梅尼德斯悖论 搜寻关键字: 近期文章 皮诺奇悖论 融贯论 关怀伦理 骗子悖论 平等主义 汇整
| 
