证明转置定理

Posted 2023-05-08

【中文标题】证明转置定理

【英文标题】：Prove the Transposition Theorem

【发布时间】：2017-02-12 01:58:22

【问题描述】：

我正在证明命题逻辑中的一些定理。

Modus Ponens 说，如果 P 暗示 Q 并且 P 为真，那么 Q 为真

P → Q
P
-----
Q

在 Haskell 中会被解释为

modus_ponens :: (p -> q) -> p -> q
modus_ponens pq p = pq p

你可能会发现它类型等价于定理，程序等价于证明。

逻辑析取

data p \/ q = Left  p
            | Right q

逻辑连接

data p /\ q = Conj p q

当且仅当

type p <-> q = (p -> q) /\ (q -> p)

承认是用来假设一个没有证据的公理

admit :: p
admit = admit

现在我无法：

(P → Q) ↔ (¬Q → ¬P)

由两部分组成：

从左到右：

P → Q
¬Q
-----
¬P

从右到左：

¬Q → ¬P
P
-------
Q

我已经用Modus tollens 证明了第一部分，但不知道第二部分的方法：

transposition :: (p -> q) <-> (Not q -> Not p)
transposition = Conj left_right right_left
                where left_right p_q not_q = modus_tollens p_q not_q
                      right_left = admit

modus_tollens :: (p -> q) -> Not q -> Not p
modus_tollens pq not_q = \p -> not_q $ pq p

double_negation :: p <-> Not (Not p)
double_negation = Conj (\p not_p -> not_p p) admit

好像可以写成：

(¬Q) → (¬P)
¬(¬P)
-----------
¬(¬Q)

但我不知道如何在这个系统中进行否定（可能还有双重否定）。

有人可以帮我吗？

---

总节目：

-# LANGUAGE TypeOperators        #-
-# LANGUAGE GADTs                #-
-# LANGUAGE NoImplicitPrelude    #-
-# LANGUAGE PolyKinds            #-
-# LANGUAGE DataKinds            #-
-# LANGUAGE TypeFamilies         #-
-# OPTIONS_GHC -fwarn-incomplete-patterns #-

import Prelude (Show(..), Eq(..), ($), (.), flip)

-- Propositional Logic --------------------------------

-- False, the uninhabited type
data False

-- Logical Not
type Not p = p -> False

-- Logical Disjunction
data p \/ q = Left  p
            | Right q

-- Logical Conjunction
data p /\ q = Conj p q

-- If and only if
type p <-> q = (p -> q) /\ (q -> p)

-- Admit is used to assume an axiom without proof
admit :: p
admit = admit

-- There is no way to prove this axiom in constructive logic, therefore we
-- leave it admitted
excluded_middle :: p \/ Not p
excluded_middle = admit

absurd :: False -> p
absurd false = admit

double_negation :: p <-> Not (Not p)
double_negation = Conj (\p not_p -> not_p p) admit

modus_ponens :: (p -> q) -> p -> q
modus_ponens = ($)

modus_tollens :: (p -> q) -> Not q -> Not p
modus_tollens pq not_q = \p -> not_q $ pq p

transposition :: (p -> q) <-> (Not q -> Not p)
transposition = Conj left_right right_left
                where left_right = modus_tollens
                      right_left = admit

【问题讨论】：

从技术上讲，modus_ponens 的类型为 (p -> q, p) -> q（或您的 (p -> q) /\ p -> q），但显然您的定义等同于柯里化。

当你在这种情况下被卡住时，你可能发现了一个不是直觉的经典重言式。在这种情况下，一种可能的策略是开始将excluded_middle 应用于某些（可能是所有）命题变量。如果全部完成，这基本上相当于构建完整的真值表 - 低效且无聊，但有效。

【参考方案1】：

你正确地注意到了

-- There is no way to prove this axiom in constructive logic, therefore we
-- leave it admitted
excluded_middle :: p \/ Not p
excluded_middle = admit

事实上，当添加到构造逻辑中时，以下是等价的公理：

排中律 双重否定 对立定律（您称之为转置定理） 皮尔斯定律

因此，您需要在双重否定证明中使用您已经承认的公理（LEM）。我们可以申请 LEM 获取p \/ Not p。然后，在这个分离上应用案例工作。在Left p 的情况下，很容易显示Not (Not p) -> p。在Right q的情况下，我们使用Not (Not p)到达False，由此我们可以得出p。

也就是说，这是您缺少的部分：

double_negation_rev :: Not (Not p) -> p
double_negation_rev = \nnp -> case excluded_middle of
    Left p -> p
    Right q -> absurd (nnp q)