Acciones

Diferencia entre revisiones de «Relación 6»

De Razonamiento automático (2018-19)
Línea 793: Línea 793:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
(* pabalagon *)
+
(* pabalagon benber *)
 
lemma ejercicio_25:
 
lemma ejercicio_25:
 
   assumes "p"
 
   assumes "p"
Línea 804: Línea 804:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
(* pabalagon *)
+
(* pabalagon benber *)
 
lemma ejercicio_26:
 
lemma ejercicio_26:
 
   assumes "q"
 
   assumes "q"
Línea 823: Línea 823:
 
next
 
next
 
   assume 3: "q" thus "q ∨ p" by (rule disjI1)
 
   assume 3: "q" thus "q ∨ p" by (rule disjI1)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_27_1:
 +
  assumes "p ∨ q"
 +
  shows  "q ∨ p"
 +
proof -
 +
  have "p ∨ q" using assms .
 +
  moreover have "p ⟹ q ∨ p" by (rule disjI2)
 +
  moreover have "q ⟹ q ∨ p" by (rule disjI1)
 +
  ultimately show "q ∨ p" by (rule disjE)
 
qed
 
qed
  
Línea 842: Línea 853:
 
     thus "p ∨ r" by (rule disjI2)
 
     thus "p ∨ r" by (rule disjI2)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_28_1:
 +
  assumes "q ⟶ r"
 +
  shows  "p ∨ q ⟶ p ∨ r"
 +
proof
 +
  assume "p ∨ q"
 +
  moreover have "p ⟹ p ∨ r" by (rule disjI1)
 +
  moreover have "q ⟹ p ∨ r"
 +
  proof (rule disjI2)
 +
    assume "q"
 +
    with `q ⟶ r` show "r" by (rule mp)
 +
  qed
 +
  ultimately show "p ∨ r" by (rule disjE)
 
qed
 
qed
  
Línea 858: Línea 884:
 
   assume "p" thus "p" .
 
   assume "p" thus "p" .
 
qed
 
qed
 +
 +
(* benber *)
 +
lemma ejercicio_29_1:
 +
  assumes "p ∨ p"
 +
  shows  "p"
 +
  using assms by (rule disjE)
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 864: Línea 896:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
(* pabalagon *)
+
(* pabalagon benber *)
 
lemma ejercicio_30:
 
lemma ejercicio_30:
 
   assumes "p"
 
   assumes "p"
Línea 890: Línea 922:
 
     assume "r" thus ?thesis by (rule disjI2)
 
     assume "r" thus ?thesis by (rule disjI2)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_31_1:
 +
  assumes "p ∨ (q ∨ r)"
 +
  shows  "(p ∨ q) ∨ r"
 +
proof -
 +
  have "p ∨ (q ∨ r)" using assms .
 +
  moreover {
 +
    assume "p"
 +
    hence "p ∨ q" by (rule disjI1)
 +
    hence "(p ∨ q) ∨ r" by (rule disjI1)
 +
  }
 +
  moreover {
 +
    assume "q ∨ r"
 +
    moreover {
 +
      assume "q"
 +
      hence "p ∨ q" by (rule disjI2)
 +
      hence "(p ∨ q) ∨ r" by (rule disjI1)
 +
    }
 +
    moreover {
 +
      assume "r"
 +
      hence "(p ∨ q) ∨ r" by (rule disjI2)
 +
    }
 +
    ultimately have "(p ∨ q) ∨ r" by (rule disjE)
 +
  }
 +
  ultimately show "(p ∨ q) ∨ r" by (rule disjE)
 
qed
 
qed
  
Línea 912: Línea 971:
 
   assume r hence "q ∨ r" by (rule disjI2)
 
   assume r hence "q ∨ r" by (rule disjI2)
 
   thus ?thesis by (rule disjI2)
 
   thus ?thesis by (rule disjI2)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_32_1:
 +
  assumes "(p ∨ q) ∨ r"
 +
  shows  "p ∨ (q ∨ r)"
 +
proof -
 +
  have "(p ∨ q) ∨ r" using assms .
 +
  moreover {
 +
    assume "p ∨ q"
 +
    moreover {
 +
      assume "p"
 +
      hence ?thesis by (rule disjI1)
 +
    }
 +
    moreover {
 +
      assume "q"
 +
      hence "q ∨ r" by (rule disjI1)
 +
      hence ?thesis by (rule disjI2)
 +
    }
 +
    ultimately have ?thesis by (rule disjE)
 +
  }
 +
  moreover {
 +
    assume "r"
 +
    hence "q ∨ r" by (rule disjI2)
 +
    hence ?thesis by (rule disjI2)
 +
  }
 +
  ultimately show ?thesis by (rule disjE)
 
qed
 
qed
  
Línea 935: Línea 1021:
 
     show "q ∨ r" using 1 by (rule conjunct2)
 
     show "q ∨ r" using 1 by (rule conjunct2)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_33_1:
 +
  assumes "p ∧ (q ∨ r)"
 +
  shows  "(p ∧ q) ∨ (p ∧ r)"
 +
proof -
 +
  have "p" using assms by (rule conjunct1)
 +
 +
  have "q ∨ r" using assms by (rule conjunct2)
 +
  moreover {
 +
    assume "q"
 +
    with `p` have "p ∧ q" by (rule conjI)
 +
    hence ?thesis by (rule disjI1)
 +
  }
 +
  moreover {
 +
    assume "r"
 +
    with `p` have "p ∧ r" by (rule conjI)
 +
    hence ?thesis by (rule disjI2)
 +
  }
 +
  ultimately show ?thesis by (rule disjE)
 
qed
 
qed
  
Línea 956: Línea 1063:
 
   have p using 4 by (rule conjunct1)
 
   have p using 4 by (rule conjunct1)
 
   thus ?thesis using 5 by (rule conjI)
 
   thus ?thesis using 5 by (rule conjI)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_34_1:
 +
  assumes "(p ∧ q) ∨ (p ∧ r)"
 +
  shows  "p ∧ (q ∨ r)"
 +
proof -
 +
  have "(p ∧ q) ∨ (p ∧ r)" using assms .
 +
  moreover {
 +
    assume "p ∧ q"
 +
    hence "p" by (rule conjunct1)
 +
    moreover {
 +
      have "q" using `p ∧ q` by (rule conjunct2)
 +
      hence "q ∨ r" by (rule disjI1)
 +
    }
 +
    ultimately have ?thesis by (rule conjI)
 +
  }
 +
  moreover {
 +
    assume "p ∧ r"
 +
    hence "p" by (rule conjunct1)
 +
    moreover {
 +
      have "r" using `p ∧ r` by (rule conjunct2)
 +
      hence "q ∨ r" by (rule disjI2)
 +
    }
 +
    ultimately have ?thesis by (rule conjI)
 +
  }
 +
  ultimately show ?thesis by (rule disjE)
 
qed
 
qed
  
Línea 977: Línea 1111:
 
   hence "p ∨ q" by (rule disjI2)
 
   hence "p ∨ q" by (rule disjI2)
 
   thus ?thesis using 4 by (rule conjI)
 
   thus ?thesis using 4 by (rule conjI)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_35_1:
 +
  assumes "p ∨ (q ∧ r)"
 +
  shows  "(p ∨ q) ∧ (p ∨ r)"
 +
proof -
 +
  have "p ∨ (q ∧ r)" using assms .
 +
  moreover {
 +
    assume "p"
 +
    hence "p ∨ q" by (rule disjI1)
 +
    moreover have "p ∨ r" using `p` by (rule disjI1)
 +
    ultimately have ?thesis by (rule conjI)
 +
  }
 +
  moreover {
 +
    assume "q ∧ r"
 +
    {
 +
      have "q" using `q ∧ r` by (rule conjunct1)
 +
      hence "p ∨ q" by (rule disjI2)
 +
    }
 +
    moreover {
 +
      have "r" using `q ∧ r` by (rule conjunct2)
 +
      hence "p ∨ r" by (rule disjI2)
 +
    }
 +
    ultimately have ?thesis by (rule conjI)
 +
  }
 +
  ultimately show ?thesis by (rule disjE)
 
qed
 
qed
  
Línea 1003: Línea 1164:
 
     qed
 
     qed
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_36_1:
 +
  assumes "(p ∨ q) ∧ (p ∨ r)"
 +
  shows  "p ∨ (q ∧ r)"
 +
proof -
 +
  have "p ∨ q" using assms by (rule conjunct1)
 +
  moreover {
 +
    assume "p"
 +
    hence ?thesis by (rule disjI1)
 +
  }
 +
  moreover {
 +
    assume "q"
 +
    have "p ∨ r" using assms by (rule conjunct2)
 +
    moreover {
 +
      assume "p"
 +
      hence ?thesis by (rule disjI1)
 +
    }
 +
    moreover {
 +
      assume "r"
 +
      with `q` have "q ∧ r" by (rule conjI)
 +
      hence ?thesis by (rule disjI2)
 +
    }
 +
    ultimately have ?thesis by (rule disjE)
 +
  }
 +
  ultimately show ?thesis by (rule disjE)
 
qed
 
qed
  
Línea 1023: Línea 1211:
 
     assume 6: "q" show "r" using 3 6 by (rule mp)
 
     assume 6: "q" show "r" using 3 6 by (rule mp)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_37_1:
 +
  assumes "(p ⟶ r) ∧ (q ⟶ r)"
 +
  shows  "p ∨ q ⟶ r"
 +
proof
 +
  assume "p ∨ q"
 +
  moreover {
 +
    have "p ⟶ r" using assms by (rule conjunct1)
 +
    moreover assume "p"
 +
    ultimately have "r" by (rule mp)
 +
  }
 +
  moreover {
 +
    have "q ⟶ r" using assms by (rule conjunct2)
 +
    moreover assume "q"
 +
    ultimately have "r" by (rule mp)
 +
  }
 +
  ultimately show "r" by (rule disjE)
 
qed
 
qed
  
Línea 1045: Línea 1252:
 
     assume q hence 2: "p ∨ q" by (rule disjI2)
 
     assume q hence 2: "p ∨ q" by (rule disjI2)
 
     show r using assms(1) 2 by (rule mp)
 
     show r using assms(1) 2 by (rule mp)
 +
  qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_38_1:
 +
  assumes "p ∨ q ⟶ r"
 +
  shows  "(p ⟶ r) ∧ (q ⟶ r)"
 +
proof
 +
  show "p ⟶ r"
 +
  proof
 +
    assume "p"
 +
    hence "p ∨ q" by (rule disjI1)
 +
    with assms show "r" by (rule mp)
 +
  qed
 +
next
 +
  show "q ⟶ r"
 +
  proof
 +
    assume "q"
 +
    hence "p ∨ q" by (rule disjI2)
 +
    with assms show "r" by (rule mp)
 
   qed
 
   qed
 
qed
 
qed
Línea 1055: Línea 1282:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
(* pabalagon *)
+
(* pabalagon benber *)
 
lemma ejercicio_39:
 
lemma ejercicio_39:
 
   assumes "p"
 
   assumes "p"
Línea 1072: Línea 1299:
 
proof (rule impI)
 
proof (rule impI)
 
   assume 2: p show q using 1 2 by (rule notE)
 
   assume 2: p show q using 1 2 by (rule notE)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_40_1:
 +
  assumes "¬p"
 +
  shows  "p ⟶ q"
 +
proof
 +
  assume "p"
 +
  with `¬p` show "q" by (rule notE)
 
qed
 
qed
  
Línea 1085: Línea 1321:
 
proof (rule impI)
 
proof (rule impI)
 
   assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
 
   assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_41_1:
 +
  assumes "p ⟶ q"
 +
  shows  "¬q ⟶ ¬p"
 +
proof
 +
  assume "¬q"
 +
  with `p ⟶ q` show "¬p" by (rule mt)
 
qed
 
qed
  
Línea 1101: Línea 1346:
 
next
 
next
 
   assume 2: "q" show "p" using assms(2) 2 by (rule notE)
 
   assume 2: "q" show "p" using assms(2) 2 by (rule notE)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_42_1:
 +
  assumes "p∨q"
 +
          "¬q"
 +
  shows  "p"
 +
proof -
 +
  note `p ∨ q`
 +
  moreover have "p ⟹ p" .
 +
  moreover {
 +
    assume "q"
 +
    with `¬q` have "p" by (rule notE)
 +
  }
 +
  ultimately show "p" by (rule disjE)
 
qed
 
qed
  
Línea 1117: Línea 1377:
 
next
 
next
 
   assume "q" thus "q" .
 
   assume "q" thus "q" .
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_43_1:
 +
  assumes "p ∨ q"
 +
          "¬p"
 +
  shows  "q"
 +
proof -
 +
  note `p ∨ q`
 +
  moreover {
 +
    assume "p"
 +
    with `¬p` have "q" by (rule notE)
 +
  }
 +
  moreover have "q ⟹ q" .
 +
  ultimately show "q" by (rule disjE)
 
qed
 
qed
  
Línea 1137: Línea 1412:
 
     assume 5: "q" show ?thesis using 3 5 by (rule notE)
 
     assume 5: "q" show ?thesis using 3 5 by (rule notE)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_44_1:
 +
  assumes "p ∨ q"
 +
  shows  "¬(¬p ∧ ¬q)"
 +
proof
 +
  assume "¬p ∧ ¬q"
 +
 +
  note `p ∨ q`
 +
  moreover {
 +
    from `¬p ∧ ¬q` have "¬p" by (rule conjunct1)
 +
    moreover assume "p"
 +
    ultimately have "False" by (rule notE)
 +
  }
 +
  moreover {
 +
    from `¬p ∧ ¬q` have "¬q" by (rule conjunct2)
 +
    moreover assume "q"
 +
    ultimately have "False" by (rule notE)
 +
  }
 +
  ultimately show "False" by (rule disjE)
 
qed
 
qed
  
Línea 1157: Línea 1453:
 
     assume "¬q" thus ?thesis using 4 by (rule notE)
 
     assume "¬q" thus ?thesis using 4 by (rule notE)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_45_1:
 +
  assumes "p ∧ q"
 +
  shows  "¬(¬p ∨ ¬q)"
 +
proof
 +
  assume "¬p ∨ ¬q"
 +
  moreover {
 +
    assume "¬p"
 +
    moreover have "p" using `p ∧ q` by (rule conjunct1)
 +
    ultimately have "False" by (rule notE)
 +
  }
 +
  moreover {
 +
    assume "¬q"
 +
    moreover have "q" using `p ∧ q` by (rule conjunct2)
 +
    ultimately have "False" by (rule notE)
 +
  }
 +
  ultimately show False by (rule disjE)
 
qed
 
qed
  
Línea 1178: Línea 1493:
 
     assume q hence 3: "p ∨ q" by (rule disjI2)
 
     assume q hence 3: "p ∨ q" by (rule disjI2)
 
     show False using 1 3 by (rule notE)
 
     show False using 1 3 by (rule notE)
 +
  qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_46_1:
 +
  assumes "¬(p ∨ q)"
 +
  shows  "¬p ∧ ¬q"
 +
proof
 +
  show "¬p"
 +
  proof (rule ccontr)
 +
    assume "¬¬p"
 +
    hence "p" by (rule notnotD)
 +
    hence "p ∨ q" by (rule disjI1)
 +
    with assms show "False" by (rule notE)
 +
  qed
 +
next
 +
  show "¬q"
 +
  proof (rule ccontr)
 +
    assume "¬¬q"
 +
    hence "q" by (rule notnotD)
 +
    hence "p ∨ q" by (rule disjI2)
 +
    with assms show "False" by (rule notE)
 
   qed
 
   qed
 
qed
 
qed
Línea 1200: Línea 1537:
 
     assume 6: q show ?thesis using 3 6 by (rule notE)
 
     assume 6: q show ?thesis using 3 6 by (rule notE)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_47_1:
 +
  assumes "¬p ∧ ¬q"
 +
  shows  "¬(p ∨ q)"
 +
proof
 +
  assume "p ∨ q"
 +
  hence "¬(¬p ∧ ¬q)" by (rule ejercicio_44_1)
 +
  thus "False" using assms by (rule notE)
 
qed
 
qed
  
Línea 1220: Línea 1567:
 
     assume "¬q" thus ?thesis using 4 by (rule notE)
 
     assume "¬q" thus ?thesis using 4 by (rule notE)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_48_1:
 +
  assumes "¬p ∨ ¬q"
 +
  shows  "¬(p ∧ q)"
 +
proof
 +
  assume "p ∧ q"
 +
  hence "¬(¬p ∨ ¬q)" by (rule ejercicio_45_1)
 +
  thus "False" using assms by (rule notE)
 
qed
 
qed
  
Línea 1234: Línea 1591:
 
   have "¬p" using 1 by (rule conjunct2)
 
   have "¬p" using 1 by (rule conjunct2)
 
   thus "False" using 2 by (rule notE)
 
   thus "False" using 2 by (rule notE)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_49_1:
 +
  "¬(p ∧ ¬p)"
 +
proof
 +
  assume "p ∧ ¬p"
 +
  hence "¬p" by (rule conjunct2)
 +
  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
 +
  ultimately show "False" by (rule notE)
 
qed
 
qed
  
Línea 1248: Línea 1615:
 
   show p using 1 by (rule conjunct1)
 
   show p using 1 by (rule conjunct1)
 
   show "¬p" using 1 by (rule conjunct2)
 
   show "¬p" using 1 by (rule conjunct2)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_50_1:
 +
  assumes "p ∧ ¬p"
 +
  shows  "q"
 +
proof -
 +
  have "¬p" using `p ∧ ¬p` by (rule conjunct2)
 +
  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
 +
  ultimately show "q" by (rule notE)
 
qed
 
qed
  
Línea 1255: Línea 1632:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
(* pabalagon *)
+
(* pabalagon benber *)
 
lemma ejercicio_51:
 
lemma ejercicio_51:
 
   assumes "¬¬p"
 
   assumes "¬¬p"
Línea 1277: Línea 1654:
 
   have 4: "p ∨ ¬p" using 2 by (rule disjI2)
 
   have 4: "p ∨ ¬p" using 2 by (rule disjI2)
 
   show "False" using 1 4 by (rule notE)
 
   show "False" using 1 4 by (rule notE)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_52_1:
 +
  "p ∨ ¬p"
 +
proof (rule ccontr)
 +
  assume "¬ (p ∨ ¬ p)"
 +
  hence "¬p ∧ ¬¬p" by (rule ejercicio_46_1)
 +
  hence "¬p" by (rule conjunct1)
 +
  moreover {
 +
    have "¬¬p" using `¬p ∧ ¬¬p` by (rule conjunct2)
 +
    hence "p" by (rule notnotD)
 +
  }
 +
  ultimately show "False" by (rule notE)
 
qed
 
qed
  
Línea 1297: Línea 1688:
 
     show False using 3 4 by (rule notE)
 
     show False using 3 4 by (rule notE)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_53_1:
 +
  "((p ⟶ q) ⟶ p) ⟶ p"
 +
proof
 +
  assume "(p ⟶ q) ⟶ p"
 +
  have "p ∨ ¬p" by (rule ejercicio_52_1)
 +
  moreover have "p ⟹ p" .
 +
  moreover {
 +
    assume "¬ p"
 +
    hence "p ⟶ q" by (rule ejercicio_40_1)
 +
    with `(p ⟶ q) ⟶ p` have "p" by (rule mp)
 +
  }
 +
  ultimately show "p" by (rule disjE)
 
qed
 
qed
  
Línea 1311: Línea 1717:
 
   assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
 
   assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
 
   have "¬¬q" using 1 3 by (rule mt)
 
   have "¬¬q" using 1 3 by (rule mt)
 +
  thus "q" by (rule notnotD)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_54_1:
 +
  assumes "¬q ⟶ ¬p"
 +
  shows  "p ⟶ q"
 +
proof
 +
  assume "p"
 +
  hence "¬¬p" by (rule notnotI)
 +
  with assms have "¬¬q" by (rule mt)
 
   thus "q" by (rule notnotD)
 
   thus "q" by (rule notnotD)
 
qed
 
qed
Línea 1338: Línea 1755:
 
   have 9: "p ∨ q" using 3 by (rule disjI1)
 
   have 9: "p ∨ q" using 3 by (rule disjI1)
 
   show False using 2 9 by (rule notE)
 
   show False using 2 9 by (rule notE)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_55_1:
 +
  assumes "¬(¬p ∧ ¬q)"
 +
  shows  "p ∨ q"
 +
proof (rule ccontr)
 +
  assume "¬(p ∨ q)"
 +
  hence "¬p ∧ ¬q" by (rule ejercicio_46_1)
 +
  with assms show False by (rule notE)
 
qed
 
qed
  
Línea 1360: Línea 1787:
 
     show False using 1 6 by (rule notE)
 
     show False using 1 6 by (rule notE)
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_56_1:
 +
  assumes "¬(¬p ∨ ¬q)"
 +
  shows  "p ∧ q"
 +
proof -
 +
  have "¬¬p ∧ ¬¬q" using assms by (rule ejercicio_46_1)
 +
  hence "¬¬p" by (rule conjunct1)
 +
  hence "p" by (rule notnotD)
 +
  moreover {
 +
    have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
 +
    hence "q" by (rule notnotD)
 +
  }
 +
  ultimately show "p ∧ q" by (rule conjI)
 
qed
 
qed
  
Línea 1390: Línea 1832:
 
     qed
 
     qed
 
   qed
 
   qed
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_57_1:
 +
  assumes "¬(p ∧ q)"
 +
  shows  "¬p ∨ ¬q"
 +
proof (rule ccontr)
 +
  assume "¬(¬p ∨ ¬q)"
 +
  hence "p ∧ q" by (rule ejercicio_56_1)
 +
  with assms show "False" by (rule notE)
 
qed
 
qed
  
Línea 1437: Línea 1889:
 
   hence 3: "¬p" ..
 
   hence 3: "¬p" ..
 
   show False using 3 2 by (rule notE)
 
   show False using 3 2 by (rule notE)
 +
qed
 +
 +
(* benber *)
 +
lemma ejercicio_58_1:
 +
  "(p ⟶ q) ∨ (q ⟶ p)"
 +
proof (rule ccontr)
 +
  assume "¬ ((p ⟶ q) ∨ (q ⟶ p))"
 +
  hence 1: "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule ejercicio_46_1)
 +
 +
  have "p ∨ ¬p" by (rule ejercicio_52_1)
 +
  moreover {
 +
    assume "p"
 +
    hence "q ⟶ p" by (rule ejercicio_7_1)
 +
 +
    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
 +
    hence "False" using `q ⟶ p` by (rule notE)
 +
  }
 +
  moreover {
 +
    assume "¬p"
 +
    hence "p ⟶ q" by (rule ejercicio_40_1)
 +
 +
    have "¬(p ⟶ q)" using 1 by (rule conjunct1)
 +
    hence "False" using `p ⟶ q` by (rule notE)
 +
  }
 +
  ultimately show "False" by (rule disjE)
 +
  moreover {
 +
    assume "p"
 +
    hence "q ⟶ p" by (rule ejercicio_7_1)
 +
 +
    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
 +
    hence "False" using `q ⟶ p` by (rule notE)
 +
  }
 
qed
 
qed
  
 
end
 
end
 
</source>
 
</source>

Revisión del 19:09 21 ene 2019

chapter {* R6: Deducción natural proposicional *}

theory R6_Deduccion_natural_proposicional
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es demostrar cada uno de los ejercicios
  usando sólo las reglas básicas de deducción natural de la lógica
  proposicional (sin usar el método auto).

  Las reglas básicas de la deducción natural son las siguientes:
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
  --------------------------------------------------------------------- 
*}

text {*
  Se usarán las reglas notnotI y mt que demostramos a continuación. *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

section {* Implicaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       p ⟶ q, p ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon josgomrom4 cammonagu*)
lemma ejercicio_1:
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"
proof -
  show "q" using 1 2 by (rule mp)
qed

(* benber *)
lemma ejercicio_1_1:
  assumes "p ⟶ q"
          "p"
  shows "q"
  using assms by (rule mp)


text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ⟶ q, q ⟶ r, p ⊢ r
  ------------------------------------------------------------------ *}

(* pabalagon josgomrom4 cammonagu*)
lemma ejercicio_2:
  assumes 1: "p ⟶ q" and
          2: "q ⟶ r" and
          3: "p"
  shows "r"
proof -
  have 4: "q" using 1 3 by (rule mp)
  show "r" using 2 4 by (rule mp)
qed

(* benber *)
lemma ejercicio_2_1:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
proof -
  have "q" using `p ⟶ q` `p` by (rule mp)
  with `q ⟶ r` show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
  ------------------------------------------------------------------ *}

(* pabalagon josgomrom4 cammonagu*)
lemma ejercicio_3:
  assumes 1: "p ⟶ (q ⟶ r)" and
          2: "p ⟶ q" and
          3: "p"
  shows "r"
proof -
  have 4: "q ⟶ r" using 1 3 by (rule mp)
  have 5: "q" using 2 3 by (rule mp)
  show "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_3_1:
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows "r"
proof -
  have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
  moreover have "q" using `p ⟶ q` `p` by (rule mp)
  ultimately show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     p ⟶ q, q ⟶ r ⊢ p ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon josgomrom4 cammonagu*)
lemma ejercicio_4:
  assumes 1: "p ⟶ q" and
          2: "q ⟶ r" 
  shows "p ⟶ r"
proof -
  { assume 3: "p"
    have 4: "q" using 1 3 by (rule mp) 
    have 5: "r" using 2 4 by (rule mp)}
  thus "p ⟶ r" by (rule impI)
qed

(* benber *)
lemma ejercicio_4_1:
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows "p ⟶ r"
proof
  assume p
  with `p ⟶ q` have "q" by (rule mp)
  with `q ⟶ r` show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon  *)
lemma ejercicio_5:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "q"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q ⟶ r" using 1 3 by (rule mp)
    show "r" using 4 2 by (rule mp)
  qed
qed

(* benber josgomrom4 *)
lemma ejercicio_5_1:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof
  assume "q"
  show "p ⟶ r"
  proof
    assume "p"
    with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
    thus "r" using `q` by (rule mp)
  qed
qed

(* pabalagon *)
lemma ejercicio_5_2:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof -
  { assume 2: "q"
    { assume 3: "p"
      have 4: "q ⟶ r" using 1 3 by (rule mp)
      have 5: "r" using 4 2 by (rule mp)}
    hence "p ⟶ r" by (rule impI)
  }
  thus "q ⟶ (p ⟶ r)" by (rule impI)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_6:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "p ⟶ q"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q ⟶ r" using 1 3 by (rule mp)
    have 5: "q" using 2 3 by (rule mp)
    show "r" using 4 5 by (rule mp)
  qed
qed

(* benber josgomrom4 *)
lemma ejercicio_6_1:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof
  assume "p ⟶ q"
  show "p ⟶ r"
  proof
    assume "p"
    with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
    moreover from `p ⟶ q` `p` have "q" by (rule mp)
    ultimately show "r" by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     p ⊢ q ⟶ p
  ------------------------------------------------------------------ *}

(* pabalagon  josgomrom4 *)
lemma ejercicio_7:
  assumes 1: "p"  
  shows   "q ⟶ p"
proof (rule impI)
  assume 2: "q"
  show "p" using 1 by this
qed

(* benber *)
lemma ejercicio_7_1:
  assumes "p"  
  shows   "q ⟶ p"
proof
  show "p" using `p` .
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ⊢ p ⟶ (q ⟶ p)
  ------------------------------------------------------------------ *}

(* pabalagon josgomrom4 *)
lemma ejercicio_8:
  "p ⟶ (q ⟶ p)"
proof (rule impI)
  assume 1: "p"
  show "q ⟶ p"
  proof (rule impI)
    assume 2: "q"
    show "p" using 1 by this
  qed
qed

(* benber *)
lemma ejercicio_8_1:
  "p ⟶ (q ⟶ p)"
  using ejercicio_7_1 by (rule impI)


text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_9:
  assumes 1: "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "q ⟶ r"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q" using 1 3 by (rule mp)
    show "r" using 2 4 by (rule mp)
  qed
qed

(* benber josgomrom4 *)
lemma ejercicio_9_1:
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
proof
  assume "q ⟶ r"
  show "p ⟶ r"
  proof
    assume "p"
    with `p ⟶ q` have "q" by (rule mp)
    with `q ⟶ r` show "r" by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_10:
  assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
  assume 2: "r"
  show "q ⟶ (p ⟶ s)"
  proof (rule impI)
    assume 3: "q"
    show "p ⟶ s"
    proof (rule impI)
      assume 4: "p"
      have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
      have 6: "r ⟶ s" using 5 3 by (rule mp)
      show "s" using 6 2 by (rule mp)
    qed
  qed
qed

(* benber josgomrom4 *)
lemma ejercicio_10_1:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof
  assume "r"
  show "q ⟶ (p ⟶ s)"
  proof
    assume "q"
    show "p ⟶ s"
    proof
      assume "p"
      with `p ⟶ (q ⟶ (r ⟶ s))`
        have "q ⟶ (r ⟶ s)" by (rule mp)
      hence "r ⟶ s" using `q` by (rule mp)
      thus "s" using `r` by (rule mp)
    qed
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
  ------------------------------------------------------------------ *}

(* pabalagon josgomrom4 *)
lemma ejercicio_11:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
  assume 1: "p ⟶ (q ⟶ r)"
  show "(p ⟶ q) ⟶ (p ⟶ r)" using 1 ejercicio_6 by simp
qed

(* pabalagon *)
lemma ejercicio_11_2:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
  assume 1: "p ⟶ (q ⟶ r)"
  show "(p ⟶ q) ⟶ (p ⟶ r)"
  proof (rule impI)
    assume 2: "p ⟶ q"
    show "p ⟶ r"
    proof (rule impI)
      assume 3: "p"
      have 4: "q ⟶ r" using 1 3 by (rule mp)
      have 5: "q" using 2 3 by (rule mp)
      show "r" using 4 5 by (rule mp)
    qed
  qed
qed

(* benber *)
lemma ejercicio_11_1:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
  assume "p ⟶ (q ⟶ r)"
  show "(p ⟶ q) ⟶ (p ⟶ r)"
  proof
    assume "p ⟶ q"
    show "p ⟶ r"
    proof
      assume p
      with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
      moreover have "q" using `p ⟶ q` `p` by (rule mp)
      ultimately show r by (rule mp)
    qed
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_12:
  assumes 1: "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume 2: "p"
  show "q ⟶ r"
  proof (rule impI)
    assume 3: "q"
    have 4: "p ⟶ q"
    proof (rule impI)
      assume 5: "p"
      show "q" using 3 by this
    qed
    show "r" using 1 4 by (rule mp)
  qed
qed

(* benber  josgomrom4 *)
lemma ejercicio_12_1:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q ⟶ r"
  proof
    assume "q"
    hence "p ⟶ q" by (rule impI)
    with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
  qed
qed

section {* Conjunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
     p, q ⊢  p ∧ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_13:
  assumes "p"
          "q" 
  shows "p ∧ q"
using assms(1, 2) by (rule conjI)

(* benber  josgomrom4 *)
lemma ejercicio_13_1:
  assumes "p"
          "q" 
  shows "p ∧ q"
  using assms by (rule conjI)

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon  josgomrom4 *)
lemma ejercicio_14:
  assumes "p ∧ q"  
  shows   "p"
  using assms(1) by (rule conjunct1)

(* benber *)
lemma ejercicio_14_1:
  assumes "p ∧ q"  
  shows   "p"
  using assms by (rule conjunct1)

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon  josgomrom4 *)
lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"
  using assms(1) by (rule conjunct2)

(* benber *)
lemma ejercicio_15_1:
  assumes "p ∧ q" 
  shows   "q"
  using assms by (rule conjunct2)

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
  ------------------------------------------------------------------ *}

(* pabalagon  josgomrom4 *)
lemma ejercicio_16:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof -
  have 1: "p" using assms(1) by (rule conjunct1)
  have 2: "q ∧ r" using assms(1) by (rule conjunct2)
  have 3: "q" using 2 by (rule conjunct1)
  have 4: "r" using 2 by (rule conjunct2)
  have 5: "p ∧ q" using 1 3 by (rule conjI)
  show "(p ∧ q) ∧ r" using 5 4 by (rule conjI)
qed

(* benber *)
lemma ejercicio_16_1:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof - (* TODO? *)
  have "q ∧ r" using assms by (rule conjunct2)

  have "p" using assms by (rule conjunct1)
  moreover have "q" using `q ∧ r` by (rule conjunct1)
  ultimately have "p ∧ q" by (rule conjI)
  moreover have "r" using `q ∧ r` by (rule conjunct2)
  ultimately show "(p ∧ q) ∧ r" by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
     (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
  ------------------------------------------------------------------ *}

(* pabalagon  josgomrom4 *)
lemma ejercicio_17:
  assumes 1: "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
proof -
  have 2: "r" using 1 by (rule conjunct2)
  have 3: "p ∧ q" using 1 by (rule conjunct1)
  have 4: "p" using 3 by (rule conjunct1)
  have 5: "q" using 3 by (rule conjunct2)
  have 6: "q ∧ r" using 5 2 by (rule conjI)
  show ?thesis using 4 6 by (rule conjI)
qed

(* benber *)
lemma ejercicio_17_1:
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
proof -
  have "p ∧ q" using assms by (rule conjunct1)

  have "p" using `p ∧ q` by (rule conjunct1)
  moreover have "q ∧ r"
  proof (rule conjI)
    show "q" using `p ∧ q` by (rule conjunct2)
  next
    show "r" using assms by (rule conjunct2)
  qed
  ultimately show ?thesis by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
     p ∧ q ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_18:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  show "q" using assms(1) by (rule conjunct2)
qed

(* benber  josgomrom4 *)
lemma ejercicio_18_1:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof
  show "q" using assms by (rule conjunct2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
     (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r   
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_19:
  assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof (rule impI)
  assume 2: "p"
  have 3: "p ⟶ q" using 1 by (rule conjunct1)
  have 4: "p ⟶ r" using 1 by (rule conjunct2)
  have 5: "q" using 3 2 by (rule mp)
  have 6: "r" using 4 2 by (rule mp)
  show "q ∧ r" using 5 6 by (rule conjI)
qed

(* benber *)
lemma ejercicio_19_1:
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof
  assume p
  show "q ∧ r"
  proof
    have "p ⟶ q" using assms by (rule conjunct1)
    thus "q" using `p` by (rule mp)
  next
    have "p ⟶ r" using assms by (rule conjunct2)
    thus "r" using `p` by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 20. Demostrar
     p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_20:
  assumes 1: "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
  show "p ⟶ q"
  proof (rule impI)
    assume 2: "p"
    have 3: "q ∧ r" using 1 2 by (rule mp)
    show 4: "q" using 3 by (rule conjunct1)
  qed
  show "p ⟶ r"
  proof (rule impI)
    assume 2: "p"
    have 3: "q ∧ r" using 1 2 by (rule mp)
    show 4: "r" using 3 by (rule conjunct2)
  qed
qed

(* benber *)
lemma ejercicio_20_1:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof
  show "p ⟶ q"
  proof
    assume "p"
    with assms have "q ∧ r" by (rule mp)
    thus "q" by (rule conjunct1)
  qed
next
  show "p ⟶ r"
  proof
    assume "p"
    with assms have "q ∧ r" by (rule mp)
    thus "r" by (rule conjunct2)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_21:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p" using 2 by (rule conjunct1)
  have 4: "q ⟶ r" using 1 3 by (rule mp)
  have 5: "q" using 2 by (rule conjunct2)
  show "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_21_1:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof
  assume "p ∧ q"
  hence "p" by (rule conjunct1)
  with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
  moreover from `p ∧ q` have "q" by (rule conjunct2)
  ultimately show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_22:
  assumes 1: "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume 2: "p"
  show "q ⟶ r"
  proof (rule impI)
    assume 3: "q"
    have 4: "p ∧ q" using 2 3 by (rule conjI)
    show "r" using 1 4 by (rule mp)
  qed
qed

(* benber *)
lemma ejercicio_22_1:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q ⟶ r"
  proof
    assume "q"
    with `p` have "p ∧ q" by (rule conjI)
    with `p ∧ q ⟶ r` show "r" by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_23:
  assumes 1: "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p ⟶ q"
  proof (rule impI)
    assume "p"
    show "q" using 2 by (rule conjunct2)
  qed
  show "r" using 1 3 by (rule mp)
qed

(* benber *)
lemma ejercicio_23_1:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof
  assume "p ∧ q"
  hence "q" by (rule conjunct2)
  hence "p ⟶ q" by (rule impI)
  with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_24:
  assumes 1: "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof (rule impI)
  assume 2: "p ⟶ q"
  have 3: "p" using 1 by (rule conjunct1)
  have 4: "q ⟶ r" using 1 by (rule conjunct2)
  have 5: "q" using 2 3 by (rule mp)
  show 6: "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_24_1:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof
  have "q ⟶ r" using assms by (rule conjunct2)

  assume "p ⟶ q"
  moreover have "p" using assms by (rule conjunct1)
  ultimately have "q" by (rule mp)
  with `q ⟶ r` show r by (rule mp)
qed

section {* Disyunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(* pabalagon benber *)
lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
  using assms(1) by (rule disjI1)

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(* pabalagon benber *)
lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
  using assms(1) by (rule disjI2)

text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_27:
  assumes 1: "p ∨ q"
  shows   "q ∨ p"
using 1 proof (rule disjE)
  assume 2: "p" thus "q ∨ p" by (rule disjI2)
next
  assume 3: "q" thus "q ∨ p" by (rule disjI1)
qed

(* benber *)
lemma ejercicio_27_1:
  assumes "p ∨ q"
  shows   "q ∨ p"
proof -
  have "p ∨ q" using assms .
  moreover have "p ⟹ q ∨ p" by (rule disjI2)
  moreover have "q ⟹ q ∨ p" by (rule disjI1)
  ultimately show "q ∨ p" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_28:
  assumes 1: "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume 2: "p ∨ q" show "p ∨ r" using 2
  proof (rule disjE)
    assume 3: p thus "p ∨ r" by (rule disjI1)
  next
    assume 4: q have r using 1 4 by (rule mp)
    thus "p ∨ r" by (rule disjI2)
  qed
qed

(* benber *)
lemma ejercicio_28_1:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof
  assume "p ∨ q"
  moreover have "p ⟹ p ∨ r" by (rule disjI1)
  moreover have "q ⟹ p ∨ r"
  proof (rule disjI2)
    assume "q"
    with `q ⟶ r` show "r" by (rule mp)
  qed
  ultimately show "p ∨ r" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_29:
  assumes 1: "p ∨ p"
  shows   "p"
using 1 proof (rule disjE)
  assume "p" thus "p" .
next
  assume "p" thus "p" .
qed

(* benber *)
lemma ejercicio_29_1:
  assumes "p ∨ p"
  shows   "p"
  using assms by (rule disjE)

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ *}

(* pabalagon benber *)
lemma ejercicio_30:
  assumes "p"
  shows   "p ∨ p"
  using assms(1) by (rule disjI1)

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_31:
  assumes 1: "p ∨ (q ∨ r)"
  shows   "(p ∨ q) ∨ r" (is "?R")
using 1 proof (rule disjE)
  assume "p" hence "p ∨ q" by (rule disjI1)
  thus ?R by (rule disjI1)
next
  assume "q ∨ r" thus ?R
  proof (rule disjE)
    assume "q" hence "p ∨ q" by (rule disjI2)
    thus "(p ∨ q) ∨ r" by (rule disjI1)
  next
    assume "r" thus ?thesis by (rule disjI2)
  qed
qed

(* benber *)
lemma ejercicio_31_1:
  assumes "p ∨ (q ∨ r)"
  shows   "(p ∨ q) ∨ r"
proof -
  have "p ∨ (q ∨ r)" using assms .
  moreover {
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    hence "(p ∨ q) ∨ r" by (rule disjI1)
  }
  moreover {
    assume "q ∨ r"
    moreover {
      assume "q"
      hence "p ∨ q" by (rule disjI2)
      hence "(p ∨ q) ∨ r" by (rule disjI1)
    }
    moreover {
      assume "r"
      hence "(p ∨ q) ∨ r" by (rule disjI2)
    }
    ultimately have "(p ∨ q) ∨ r" by (rule disjE)
  }
  ultimately show "(p ∨ q) ∨ r" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_32:
  assumes 1: "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
using 1 proof (rule disjE)
  assume "p ∨ q" thus ?thesis
  proof (rule disjE)
    assume p thus ?thesis by (rule disjI1)
  next
    assume q hence "q ∨ r" by (rule disjI1)
    thus ?thesis by (rule disjI2)
  qed
next
  assume r hence "q ∨ r" by (rule disjI2)
  thus ?thesis by (rule disjI2)
qed

(* benber *)
lemma ejercicio_32_1:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
proof -
  have "(p ∨ q) ∨ r" using assms .
  moreover {
    assume "p ∨ q"
    moreover {
      assume "p"
      hence ?thesis by (rule disjI1)
    }
    moreover {
      assume "q"
      hence "q ∨ r" by (rule disjI1)
      hence ?thesis by (rule disjI2)
    }
    ultimately have ?thesis by (rule disjE)
  }
  moreover {
    assume "r"
    hence "q ∨ r" by (rule disjI2)
    hence ?thesis by (rule disjI2)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_33:
  assumes 1: "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have 2: p using 1 by (rule conjunct1)
  show ?thesis
  proof (rule disjE)
    assume 3: q have "p ∧ q" using 2 3 by (rule conjI)
    thus ?thesis by (rule disjI1)
  next
    assume 4: r have "p ∧ r" using 2 4 by (rule conjI)
    thus ?thesis by (rule disjI2)
  next
    show "q ∨ r" using 1 by (rule conjunct2)
  qed
qed

(* benber *)
lemma ejercicio_33_1:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have "p" using assms by (rule conjunct1)

  have "q ∨ r" using assms by (rule conjunct2)
  moreover {
    assume "q"
    with `p` have "p ∧ q" by (rule conjI)
    hence ?thesis by (rule disjI1)
  }
  moreover {
    assume "r"
    with `p` have "p ∧ r" by (rule conjI)
    hence ?thesis by (rule disjI2)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_34:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
using assms(1) proof (rule disjE)
  assume 2: "p ∧ q" hence q by (rule conjunct2)
  hence 3: "q ∨ r" by (rule disjI1)
  have p using 2 by (rule conjunct1)
  thus ?thesis using 3 by (rule conjI)
next
  assume 4: "p ∧ r" hence r by (rule conjunct2)
  hence 5: "q ∨ r" by (rule disjI2)
  have p using 4 by (rule conjunct1)
  thus ?thesis using 5 by (rule conjI)
qed

(* benber *)
lemma ejercicio_34_1:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
proof -
  have "(p ∧ q) ∨ (p ∧ r)" using assms .
  moreover {
    assume "p ∧ q"
    hence "p" by (rule conjunct1)
    moreover {
      have "q" using `p ∧ q` by (rule conjunct2)
      hence "q ∨ r" by (rule disjI1)
    }
    ultimately have ?thesis by (rule conjI)
  }
  moreover {
    assume "p ∧ r"
    hence "p" by (rule conjunct1)
    moreover {
      have "r" using `p ∧ r` by (rule conjunct2)
      hence "q ∨ r" by (rule disjI2)
    }
    ultimately have ?thesis by (rule conjI)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_35:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
using assms(1) proof (rule disjE)
  assume 1: p hence 2: "p ∨ r" by (rule disjI1)
  have "p ∨ q" using 1 by (rule disjI1)
  thus ?thesis using 2 by (rule conjI)
next
  assume 3: "q ∧ r" hence r by (rule conjunct2)
  hence 4: "p ∨ r" by (rule disjI2)
  have q using 3 by (rule conjunct1)
  hence "p ∨ q" by (rule disjI2)
  thus ?thesis using 4 by (rule conjI)
qed

(* benber *)
lemma ejercicio_35_1:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
proof -
  have "p ∨ (q ∧ r)" using assms .
  moreover {
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    moreover have "p ∨ r" using `p` by (rule disjI1)
    ultimately have ?thesis by (rule conjI)
  }
  moreover {
    assume "q ∧ r"
    {
      have "q" using `q ∧ r` by (rule conjunct1)
      hence "p ∨ q" by (rule disjI2)
    }
    moreover {
      have "r" using `q ∧ r` by (rule conjunct2)
      hence "p ∨ r" by (rule disjI2)
    }
    ultimately have ?thesis by (rule conjI)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_36:
  assumes 1: "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have 2: "p ∨ q" using 1 by (rule conjunct1)
  have 3: "p ∨ r" using 1 by (rule conjunct2)
  show ?thesis using 2
  proof (rule disjE)
    assume p thus ?thesis by (rule disjI1)
  next
    assume 4: q show ?thesis using 3
    proof (rule disjE)
      assume p thus ?thesis by (rule disjI1)
    next
      assume 5: r have "q ∧ r" using 4 5 by (rule conjI)
      thus ?thesis by (rule disjI2)
    qed
  qed
qed

(* benber *)
lemma ejercicio_36_1:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have "p ∨ q" using assms by (rule conjunct1)
  moreover {
    assume "p"
    hence ?thesis by (rule disjI1)
  }
  moreover {
    assume "q"
    have "p ∨ r" using assms by (rule conjunct2)
    moreover {
      assume "p"
      hence ?thesis by (rule disjI1)
    }
    moreover {
      assume "r"
      with `q` have "q ∧ r" by (rule conjI)
      hence ?thesis by (rule disjI2)
    }
    ultimately have ?thesis by (rule disjE)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar
     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_37:
  assumes 1: "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  have 2: "p ⟶ r" using 1 by (rule conjunct1)
  have 3: "q ⟶ r" using 1 by (rule conjunct2)
  assume 4: "p ∨ q" show "r" using 4
  proof (rule disjE)
    assume 5: "p" show "r" using 2 5 by (rule mp)
  next
    assume 6: "q" show "r" using 3 6 by (rule mp)
  qed
qed

(* benber *)
lemma ejercicio_37_1:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof
  assume "p ∨ q"
  moreover {
    have "p ⟶ r" using assms by (rule conjunct1)
    moreover assume "p"
    ultimately have "r" by (rule mp)
  }
  moreover {
    have "q ⟶ r" using assms by (rule conjunct2)
    moreover assume "q"
    ultimately have "r" by (rule mp)
  }
  ultimately show "r" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_38:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
  show "p ⟶ r"
  proof (rule impI)
    assume "p" hence 1: "p ∨ q" by (rule disjI1)
    show "r" using assms(1) 1 by (rule mp)
  qed
next
  show "q ⟶ r"
  proof (rule impI)
    assume q hence 2: "p ∨ q" by (rule disjI2)
    show r using assms(1) 2 by (rule mp)
  qed
qed

(* benber *)
lemma ejercicio_38_1:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof
  show "p ⟶ r"
  proof
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    with assms show "r" by (rule mp)
  qed
next
  show "q ⟶ r"
  proof
    assume "q"
    hence "p ∨ q" by (rule disjI2)
    with assms show "r" by (rule mp)
  qed
qed

section {* Negaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ *}

(* pabalagon benber *)
lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
  using assms(1) by (rule notnotI)

text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_40:
  assumes 1: "¬p"
  shows   "p ⟶ q"
proof (rule impI)
  assume 2: p show q using 1 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_40_1:
  assumes "¬p" 
  shows   "p ⟶ q"
proof
  assume "p"
  with `¬p` show "q" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_41:
  assumes 1: "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof (rule impI)
  assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
qed

(* benber *)
lemma ejercicio_41_1:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof
  assume "¬q"
  with `p ⟶ q` show "¬p" by (rule mt)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p∨q, ¬q ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
using assms(1) proof (rule disjE)
  assume "p" thus "p" .
next
  assume 2: "q" show "p" using assms(2) 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_42_1:
  assumes "p∨q"
          "¬q" 
  shows   "p"
proof -
  note `p ∨ q`
  moreover have "p ⟹ p" .
  moreover {
    assume "q"
    with `¬q` have "p" by (rule notE)
  }
  ultimately show "p" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
using assms(1) proof (rule disjE)
  assume 1: "p" show "q" using assms(2) 1 by (rule notE)
next
  assume "q" thus "q" .
qed

(* benber *)
lemma ejercicio_43_1:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
proof -
  note `p ∨ q`
  moreover {
    assume "p"
    with `¬p` have "q" by (rule notE)
  }
  moreover have "q ⟹ q" .
  ultimately show "q" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof (rule notI)
  assume 1: "¬p ∧ ¬q" hence 2: "¬p" by (rule conjunct1)
  have 3: "¬q" using 1 by (rule conjunct2)
  show "False"
  using assms(1) proof (rule disjE)
    assume 4: "p" show ?thesis using 2 4 by (rule notE)
  next
    assume 5: "q" show ?thesis using 3 5 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_44_1:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof
  assume "¬p ∧ ¬q"

  note `p ∨ q`
  moreover {
    from `¬p ∧ ¬q` have "¬p" by (rule conjunct1)
    moreover assume "p"
    ultimately have "False" by (rule notE)
  }
  moreover {
    from `¬p ∧ ¬q` have "¬q" by (rule conjunct2)
    moreover assume "q"
    ultimately have "False" by (rule notE)
  }
  ultimately show "False" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_45:
  assumes 1: "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof (rule notI)
  assume 2: "¬p ∨ ¬q" have 3: "p" using 1 by (rule conjunct1)
  have 4: "q" using 1 by (rule conjunct2)
  show "False" using 2
  proof (rule disjE)
    assume "¬p" thus ?thesis using 3 by (rule notE)
  next
    assume "¬q" thus ?thesis using 4 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_45_1:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof
  assume "¬p ∨ ¬q"
  moreover {
    assume "¬p"
    moreover have "p" using `p ∧ q` by (rule conjunct1)
    ultimately have "False" by (rule notE)
  }
  moreover {
    assume "¬q"
    moreover have "q" using `p ∧ q` by (rule conjunct2)
    ultimately have "False" by (rule notE)
  }
  ultimately show False by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 46. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_46:
  assumes 1: "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
  proof (rule notI)
    assume p hence 2: "p ∨ q" by (rule disjI1)
    show False using 1 2 by (rule notE)
  qed
  show "¬q"
  proof (rule notI)
    assume q hence 3: "p ∨ q" by (rule disjI2)
    show False using 1 3 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_46_1:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof
  show "¬p"
  proof (rule ccontr)
    assume "¬¬p"
    hence "p" by (rule notnotD)
    hence "p ∨ q" by (rule disjI1)
    with assms show "False" by (rule notE)
  qed
next
  show "¬q"
  proof (rule ccontr)
    assume "¬¬q"
    hence "q" by (rule notnotD)
    hence "p ∨ q" by (rule disjI2)
    with assms show "False" by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 47. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_47:
  assumes 1: "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof (rule notI)
  have 2: "¬p" using 1 by (rule conjunct1)
  have 3: "¬q" using 1 by (rule conjunct2)
  assume 4: "p ∨ q"
  show False
  using 4 proof (rule disjE)
    assume 5: p show ?thesis using 2 5 by (rule notE)
  next
    assume 6: q show ?thesis using 3 6 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_47_1:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof
  assume "p ∨ q"
  hence "¬(¬p ∧ ¬q)" by (rule ejercicio_44_1)
  thus "False" using assms by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 48. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_48:
  assumes 1: "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule notI)
  assume 2: "p ∧ q" hence 3: p by (rule conjunct1)
  have 4: q using 2 by (rule conjunct2)
  show False
  using 1 proof (rule disjE)
    assume "¬p" thus ?thesis using 3 by (rule notE)
  next
    assume "¬q" thus ?thesis using 4 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_48_1:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof
  assume "p ∧ q"
  hence "¬(¬p ∨ ¬q)" by (rule ejercicio_45_1)
  thus "False" using assms by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_49:
  "¬(p ∧ ¬p)"
proof (rule notI)
  assume 1: "p ∧ ¬p" hence 2: p by (rule conjunct1)
  have "¬p" using 1 by (rule conjunct2)
  thus "False" using 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_49_1:
  "¬(p ∧ ¬p)"
proof
  assume "p ∧ ¬p"
  hence "¬p" by (rule conjunct2)
  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
  ultimately show "False" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_50:
  assumes 1: "p ∧ ¬p"
  shows   "q"
proof (rule notE)
  show p using 1 by (rule conjunct1)
  show "¬p" using 1 by (rule conjunct2)
qed

(* benber *)
lemma ejercicio_50_1:
  assumes "p ∧ ¬p" 
  shows   "q"
proof -
  have "¬p" using `p ∧ ¬p` by (rule conjunct2)
  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
  ultimately show "q" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon benber *)
lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"
  using assms(1) by (rule notnotD)

text {* --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_52:
  "p ∨ ¬p"
proof (rule ccontr)
  assume 1: "¬(p ∨ ¬p)"
  have 2: "¬p" proof (rule notI)
    assume p hence 3: "p ∨ ¬p" by (rule disjI1)
    show "False" using 1 3 by (rule notE)
  qed
  have 4: "p ∨ ¬p" using 2 by (rule disjI2)
  show "False" using 1 4 by (rule notE)
qed

(* benber *)
lemma ejercicio_52_1:
  "p ∨ ¬p"
proof (rule ccontr)
  assume "¬ (p ∨ ¬ p)"
  hence "¬p ∧ ¬¬p" by (rule ejercicio_46_1)
  hence "¬p" by (rule conjunct1)
  moreover {
    have "¬¬p" using `¬p ∧ ¬¬p` by (rule conjunct2)
    hence "p" by (rule notnotD)
  }
  ultimately show "False" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 53. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume 1: "(p ⟶ q) ⟶ p"
  show p proof (rule ccontr)
    assume 2: "¬p"
    have 3: "¬(p ⟶ q)" using 1 2 by (rule mt)
    have 4: "p ⟶ q" proof (rule impI)
      assume 5: p show q using 2 5 by (rule notE)
    qed
    show False using 3 4 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_53_1:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof
  assume "(p ⟶ q) ⟶ p"
  have "p ∨ ¬p" by (rule ejercicio_52_1)
  moreover have "p ⟹ p" .
  moreover {
    assume "¬ p"
    hence "p ⟶ q" by (rule ejercicio_40_1)
    with `(p ⟶ q) ⟶ p` have "p" by (rule mp)
  }
  ultimately show "p" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 54. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_54:
  assumes 1: "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof (rule impI)
  assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
  have "¬¬q" using 1 3 by (rule mt)
  thus "q" by (rule notnotD)
qed

(* benber *)
lemma ejercicio_54_1:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof
  assume "p"
  hence "¬¬p" by (rule notnotI)
  with assms have "¬¬q" by (rule mt)
  thus "q" by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_55:
  assumes 1: "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule ccontr)
  assume 2: "¬(p ∨ q)"
  have 3: "p"
  proof (rule ccontr)
    assume 4: "¬p"
    have 5: "q"
    proof (rule ccontr)
      assume 6: "¬q" have 7: "¬p ∧ ¬q" using 4 6 by (rule conjI)
      show False using 1 7 by (rule notE)
    qed
    have 8: "p ∨ q" using 5 by (rule disjI2)
    show False using 2 8 by (rule notE)
  qed
  have 9: "p ∨ q" using 3 by (rule disjI1)
  show False using 2 9 by (rule notE)
qed

(* benber *)
lemma ejercicio_55_1:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule ccontr)
  assume "¬(p ∨ q)"
  hence "¬p ∧ ¬q" by (rule ejercicio_46_1)
  with assms show False by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_56:
  assumes 1: "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof (rule conjI)
  show 3: p
  proof (rule ccontr)
    assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
    show False using 1 4 by (rule notE)
  qed
  show 5: q
  proof (rule ccontr)
    assume "¬q" hence 6: "¬p ∨ ¬q" by (rule disjI2)
    show False using 1 6 by (rule notE)
  qed
qed

(* benber *)
lemma ejercicio_56_1:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof -
  have "¬¬p ∧ ¬¬q" using assms by (rule ejercicio_46_1)
  hence "¬¬p" by (rule conjunct1)
  hence "p" by (rule notnotD)
  moreover {
    have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
    hence "q" by (rule notnotD)
  }
  ultimately show "p ∧ q" by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_57:
  assumes 1: "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof (rule ccontr)
  assume 2: "¬(¬p ∨ ¬q)"
  show False using 1
  proof (rule notE)
    show 3: "p ∧ q"
    proof (rule conjI)
      show p
      proof (rule ccontr)
        assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
        show False using 2 4 by (rule notE)
      qed
    next
      show q
      proof (rule ccontr)
        assume "¬q" hence 5: "¬p ∨ ¬q" by (rule disjI2)
        show False using 2 5 by (rule notE)
      qed
    qed
  qed
qed

(* benber *)
lemma ejercicio_57_1:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof (rule ccontr)
  assume "¬(¬p ∨ ¬q)"
  hence "p ∧ q" by (rule ejercicio_56_1)
  with assms show "False" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 58. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "(p ⟶ q) ∨ ¬(p ⟶ q)" proof (rule ccontr)
    assume 1: "¬((p ⟶ q) ∨ ¬(p ⟶ q))"
    have 2: "¬(p ⟶ q)" proof (rule notI)
      assume "p ⟶ q" 
      hence 3: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI1)
      show False using 1 3 by (rule notE)
    qed
    hence 4: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI2)
    show "False" using 1 4 by (rule notE)
  qed
  thus ?thesis proof (rule disjE)
    assume "p ⟶ q" thus ?thesis by (rule disjI1)
  next
    assume 1: "¬(p ⟶ q)"
    have "q ⟶ p" proof (rule impI)
      assume 2: q
      have 3: "p ⟶ q" proof (rule impI)
        assume p show q using 2 .
      qed
      show p using 1 3 by (rule notE)
    qed
    thus ?thesis by (rule disjI2)
  qed
qed

(* pabalagon *)
lemma ejercicio_58_2:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
  assume 1: "¬((p ⟶ q) ∨ (q ⟶ p))"
  hence 1: "(p ∧ ¬q) ∧ (q ∧ ¬p)" by simp
  hence "p ∧ ¬q" ..
  hence 2: p ..
  have "q ∧ ¬p" using 1 ..
  hence 3: "¬p" ..
  show False using 3 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_58_1:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
  assume "¬ ((p ⟶ q) ∨ (q ⟶ p))"
  hence 1: "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule ejercicio_46_1)

  have "p ∨ ¬p" by (rule ejercicio_52_1)
  moreover {
    assume "p"
    hence "q ⟶ p" by (rule ejercicio_7_1)

    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
    hence "False" using `q ⟶ p` by (rule notE)
  }
  moreover {
    assume "¬p"
    hence "p ⟶ q" by (rule ejercicio_40_1)

    have "¬(p ⟶ q)" using 1 by (rule conjunct1)
    hence "False" using `p ⟶ q` by (rule notE)
  }
  ultimately show "False" by (rule disjE)
  moreover {
    assume "p"
    hence "q ⟶ p" by (rule ejercicio_7_1)

    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
    hence "False" using `q ⟶ p` by (rule notE)
  }
qed

end
Obtenido de «https://www.glc.us.es/~jalonso/RA2018/index.php?title=Relación_6&oldid=260»