転位の定理を証明する

Question

私は命題論理でいくつかの定理を証明しています。

は、PはQを意味し、Pが真である場合は、Qが真である

P → Q 
P 
----- 
Q 

が

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

あなたが見つけるかもしれないとして、Haskellで解釈されるだろうと述べてモデュスPonensを言いますタイプは定理に相当し、プログラムはプルーフに相当します。

論理和

data p \/ q = Left p 
      | Right q 

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

が証明なし公理を前提とするために使用されて認める

data p /\ q = Conj p q 

場合に限り、論理積

admit :: p 
admit = admit 

左に

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

右：

が左から右へ

：2部で構成されてい

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

：

は今、私は移調定理を証明する問題を抱えています

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

私はすでに第1回PAを証明しました

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 

それはのように書くことができるようだ：Modus tollensとRTが、第2回の部分のための方法を見つけ出すことができませんでした

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

をしかし、私はどのように否定を行うには考えている（そしておそらく二重否定）を行う。

誰かが私に助けてくれますか？

---

合計プログラム：建設的なロジックに追加するときには、当然実際に

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

ことに注意して

{-# 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 

Answer 1

は、次は同等の公理です：

• 法除外された中間
• 二重否定
• Contrapositiveの法則（あなたが移調定理と呼ばれてきたもの）
• パースの法則

したがって、あなたはあなたの中にあなたが入院しました公理（LEM）を使用する必要があります二重否定の証拠。 LEMを適用してp \/ Not pを取得することがあります。そして、この論理和に対してケースワークを適用する。 Left pの場合は、Not (Not p) -> pと表示されます。 Right qの場合、Not (Not p)を使用してFalseに到着します。これからpと結論できます。 （ - > Q、P P） - > q`（またはあなたの `（P

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