命题逻辑

Question

我想从(p→q) and (qr→s)到(pr→s)，这是一样的((not p) or q) and (not(q and r) or s)到(not(p and r) or s)

Answer 1

定理：

p → q 
= ¬p ∨ q  -- 1 

    (q ∧ r) → s 
= ¬(q ∧ r) ∨ s 
= ¬q ∨ ¬r ∨ s -- 2 

    ¬p ∨ ¬r ∨ s -- from 1 and 2, q and ¬q cancel 
= ¬(p ∧ r) ∨ s 
= (p ∧ r) → s 

QED。

---

使用Coq的，我们可以按照如下证明这个定理：

Coq < Theorem prop : forall p q r s : Prop, (p -> q) /\ (q /\ r -> s) -> p /\ r -> s. 
1 subgoal 

    ============================ 
    forall p q r s : Prop, (p -> q) /\ (q /\ r -> s) -> p /\ r -> s 

prop < intros. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Prop 
    s : Prop 
    H : (p -> q) /\ (q /\ r -> s) 
    H0 : p /\ r 
    ============================ 
    s 

prop < destruct H. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Prop 
    s : Prop 
    H : p -> q 
    H1 : q /\ r -> s 
    H0 : p /\ r 
    ============================ 
    s 

prop < destruct H0. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Prop 
    s : Prop 
    H : p -> q 
    H1 : q /\ r -> s 
    H0 : p 
    H2 : r 
    ============================ 
    s 

prop < apply H1. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Prop 
    s : Prop 
    H : p -> q 
    H1 : q /\ r -> s 
    H0 : p 
    H2 : r 
    ============================ 
    q /\ r 

prop < split. 
2 subgoals 

    p : Prop 
    q : Prop 
    r : Prop 
    s : Prop 
    H : p -> q 
    H1 : q /\ r -> s 
    H0 : p 
    H2 : r 
    ============================ 
    q 

subgoal 2 is: 
r 

prop < exact (H H0). 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Prop 
    s : Prop 
    H : p -> q 
    H1 : q /\ r -> s 
    H0 : p 
    H2 : r 
    ============================ 
    r 

prop < exact H2. 
No more subgoals. 

prop < Qed. 
intros. 
destruct H. 
destruct H0. 
apply H1. 
split. 
exact (H H0). 

exact H2. 

prop is defined 

希望有所帮助。