Beweisen Sie das Transpositions-Theorem

Question

Ich beweise einige Sätze in der Aussagelogik.

sagt, Modus Ponens, die besagt, dass wenn P Q bedeutet und P wahr ist, dann Q wahr ist

P → Q 
P 
----- 
Q 

würde in Haskell als

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

Sie interpretiert werden könnten, finden es Typen sind gleichbedeutend mit Theoremen und Programme entsprechen Beweisen.

Disjunktion

data p \/ q = Left p 
      | Right q 

logische Verknüpfung

data p /\ q = Conj p q 

Wenn und nur wenn

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

Zugeben, verwendet, um ein Axiom ohne Beweis anzunehmen

admit :: p 
admit = admit 

Jetzt habe ich Probleme die Umsetzung Theorem zu beweisen:

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

, die besteht aus 2 Teilen:

links nach rechts:

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

rechts nach links:

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

Ich habe bereits die 1. pa bewiesen rt mit Modus tollens kann aber nicht einen Weg für die 2. Teil herauszufinden:

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 

Es scheint, dass es so schreiben könnte:

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

Aber ich habe keine Ahnung, wie die Negation zu tun (und vielleicht doppelte Negation) in diesem System.

Könnte mir jemand dabei helfen?

---

Gesamtprogramm:

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

Sie beachten zu Recht, dass

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

In der Tat, die folgende äquivalente Axiome sind, wenn sie konstruktive Logik hinzugefügt:

• Gesetz der Ausgeschlossen Mitte
• Doppel Negierung
• Gesetz des contra (was man den Umsetzungs Satz genannt hat)
• Peirce Gesetz

Daher müssen Sie das Axiom verwenden, die Sie zugelassen haben (der LEM) in Ihrem Beweis der doppelten Verneinung. Wir können LEM anwenden, um p \/ Not p zu erhalten. Wenden Sie dann Fallarbeit auf diese Disjunktion an. Im Fall Left p ist es einfach, Not (Not p) -> p anzuzeigen. Im Fall Right q verwenden wir Not (Not p), um False zu erreichen, aus dem wir schließen können p.

Nämlich, das ist der Teil Sie verpassen:

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