Relación 7

chapter {* R7: Deducción natural en lógica de primer orden *}

theory R7
imports Main 
begin

text {*
  Demostrar o refutar los siguientes lemas usando sólo las reglas
  básicas de deducción natural de la lógica proposicional, de los
  cuantificadores y de la igualdad: 
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · 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
  · excluded_middel:(¬P ∨ P) 

  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y
*}

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

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_1a: carmarria
  assumes 1: "∀x. P x ⟶ Q x"
  shows   "(∀x. P x) ⟶ (∀x. Q x)"
proof -
  {assume 2: "! x. P x"
    {fix a
    have 3: "P a ⟶ Q a" using 1 by (rule allE)
    have 4: "P a" using 2 by (rule allE)
    have 5: "Q a" using 3 4 by (rule mp)
  }
  hence 6: "! x. Q x" by (rule allI)
}
  thus "(! x. P x) ⟶ (! x. Q x)" by (rule impI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       ∃x. ¬(P x) ⊢ ¬(∀x. P x)
  ------------------------------------------------------------------ *}

lemma ejercicio_2a: carmarria
  assumes 1: "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof -
  obtain a where 2: "¬(P a)" using 1 by (rule exE)
  {assume 3: "! x. P x"
    have 4: "P a" using 3 by (rule allE)
    have 5: False using 2 4 by (rule notE)
  }
  thus "¬(! x. P x)" by (rule notI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
       ∀x. P x ⊢ ∀y. P y
  ------------------------------------------------------------------ *}

lemma ejercicio_3a: carmarria
  assumes 1: "∀x. P x"
  shows   "∀y. P y"
proof -
  {fix a
    have 2: "P a" using 1 by (rule allE)
  }
  thus "! y. P y" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
  ------------------------------------------------------------------ *}

lemma ejercicio_4: carmarria
  assumes 1: "∀x. P x ⟶ Q x"
  shows   "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof -
  {assume 2: "!x. ¬(Q x)"
      {fix a
    have 3: "¬(Q a)" using 2 by (rule allE)
    have 4: "P a ⟶ Q a" using 1 by (rule allE)
    have 5: "¬(P a)" using 4 3 by (rule mt)
  }
  hence 6: "!x. ¬ (P x)" by (rule allI)
}
  thus "(!x. ¬(Q x)) ⟶ (!x. ¬ (P x))" by (rule impI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
       ∀x. P x  ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_5: carmarria
  assumes 1: "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof -
  {assume 2: "? x. P x & Q x"
    obtain a where 3: "P a & Q a" using 2 by (rule exE)
    have 4: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
    have 5: "P a" using 3 by (rule conjunct1)
    have 6: "Q a" using 3 by (rule conjunct2)
    have 7: "¬(Q a)" using 4 5 by (rule mp)
    have 8: False using 7 6 by (rule notE)
  }
  thus "¬(? x. P x & Q x)" by (rule notI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
       ∀x y. P x y ⊢ ∀u v. P u v
  ------------------------------------------------------------------ *}

lemma ejercicio_6: carmarria
  assumes 1: "∀x y. P x y"
  shows   "∀u v. P u v"
proof -
  {fix a
    have 2: "! y. P a y" using 1 by (rule allE)
    {fix b
      have 3: "P a b" using 2 by (rule allE)
    }
    hence 4: "!v. P a v" by (rule allI)
  }
  thus "!u v. P u v" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
       ∃x y. P x y ⟹ ∃u v. P u v
  ------------------------------------------------------------------ *}

lemma ejercicio_7: carmarria
  assumes 1: "∃x y. P x y"
  shows   "∃u v. P u v"
proof -
  obtain a where 2: "? y. P a y" using 1 by (rule exE)
  obtain b where 3: "P a b" using 2 by (rule exE)
  have 4: "? v. P a v" using 3 by (rule exI)
  show 5: "? u v. P u v" using 4 by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
       ∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
  ------------------------------------------------------------------ *}

lemma ejercicio_8: carmarria
  assumes 1: "∃x. ∀y. P x y"
  shows   "∀y. ∃x. P x y"
proof -
  obtain a where 2: "! y. P a y" using 1 by (rule exE)
  {fix b
    have 3: "P a b" using 2 by (rule allE)
    have 4: "? x. P x b" using 3 by (rule exI)
  }
  thus "! y. ? x. P x y" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
       ∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_9: carmarria
  assumes 1: "∃x. P a ⟶ Q x"
  shows   "P a ⟶ (∃x. Q x)"
proof -
  {assume 2: "P a"
    obtain b where 3: "P a ⟶ Q b" using 1 by (rule exE)
    have 4: "Q b" using 3 2 by (rule mp)
    have 5: "? x. Q x" using 4 by (rule exI)
  }
  thus "P a ⟶ (? x. Q x)" by (rule impI)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

lemma ejercicio_10a: carmarria
  fixes P Q :: "'b ⇒ bool" 
  assumes 1: "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have 2: "¬(P a) ∨ (P a)" by (rule excluded_middle)
  moreover {assume 3: "¬(P a)" 
    {assume 4: "P a"
      have 5: False using 3 4 by (rule notE)
      have 6: "Q b" using 5 by (rule FalseE)
    }
    hence 7: "P a ⟶Q b" by (rule impI)
    have 8: "? x. P a ⟶ Q x" using 7 by (rule exI)
  }
  moreover {assume 9: "P a"
    have 10: "? x. Q x" using 1 9 by (rule mp)
    obtain b where 11: "Q b" using 10 by (rule exE)
    {assume 12: "P a"
      have 13: "Q b" using 11 by this
    }
    hence 13: "P a ⟶ Q b" by (rule impI)
    have 14: "? x. P a ⟶ Q x" using 13 by (rule exI)
  }
  ultimately show "? x. P a ⟶ Q x" by (rule disjE)
qed 


text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
       (∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
  ------------------------------------------------------------------ *}

lemma ejercicio_11a: carmarria
  assumes 1:"(∃x. P x) ⟶ Q a"
  shows   "∀x. P x ⟶ Q a"
  proof-
  {fix b
    {assume 2: "P b"
      have 3: "? x. P x" using 2 by (rule exI)
      have 4: "Q a" using 1 3 by (rule mp)
    }
    hence 5: "P b ⟶ Q a" by (rule impI)
  }
  thus "! x. P x ⟶ Q a" by (rule allI)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
       ∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
  ------------------------------------------------------------------ *}

lemma ejercicio_12a: carmarria
  assumes 1: "∀x. P x ⟶ Q a"
  shows   "∃x. P x ⟶ Q a"
proof -
  have 2: "P b ⟶ Q a" using 1 by (rule allE)
  show 3: "? x. P x ⟶ Q a" using 2 by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
       (∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
  ------------------------------------------------------------------ *}

lemma ejercicio_13a: carmarria
  assumes 1: "(∀x. P x) ∨ (∀x. Q x)"
  shows   "∀x. P x ∨ Q x"
proof -
  {fix a
    have 2: "(! x. P x) ∨ (! x. Q x)" using 1 by this
    moreover {assume 3:"! x. P x"
      have 4: "P a" using 3 by (rule allE)
      have 5: "P a | Q a" using 4 by (rule disjI1)
    }
    moreover {assume 6: "! x. Q x" 
      have 7: "Q a" using 6 by (rule allE)
      have 8: "P a | Q a" using 7 by (rule disjI2)
    }
    ultimately have 9: "P a | Q a" by (rule disjE)
  }
  thus "! x. P x | Q x" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
       ∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_14a: carmarria
  assumes 1: "∃x. P x ∧ Q x"
  shows   "(∃x. P x) ∧ (∃x. Q x)"
proof -
  obtain a where 2: "P a & Q a" using 1 by (rule exE)
  have 3: "P a" using 2 by (rule conjunct1)
  have 4: "Q a" using 2 by (rule conjunct2)
  have 5: "? x. P x" using 3 by (rule exI)
  have 6: "? x. Q x" using 4 by (rule exI)
  show "(? x. P x) ∧ (? x. Q x)" using 5 6 by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
       ∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_15a: carmarria
  assumes 1: "∀x y. P y ⟶ Q x"
  shows   "(∃y. P y) ⟶ (∀x. Q x)"
proof -
  {assume 2: "? y. P y"
    {fix a
      have 3: "! y. P y ⟶ Q a" using 1 by (rule allE)
      obtain b where 4: "P b" using 2 by (rule exE)
      have 5: "P b ⟶ Q a" using 3 by (rule allE)
      have 6: "Q a" using 5 4 by (rule mp)
    }
    hence 7: "! x. Q x" by (rule allI)
  }
  thus "(? y. P y) ⟶ (! x. Q x)" by (rule impI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
       ¬(∀x. ¬(P x)) ⊢ ∃x. P x
  ------------------------------------------------------------------ *}

lemma ejercicio_16a: carmarria
  assumes 1: "¬(∀x. ¬(P x))"
  shows   "∃x. P x"
proof -
    {assume 2: "¬(? x. P x)"
      {fix b
        {assume 3: "P b"
          have 4: "? x. P x" using 3 by (rule exI)
          have 5: False using 2 4 by (rule notE)
        }
        hence 6: "¬(P b)" by (rule notI)
      }
      hence 7: "! x. ¬(P x)" by (rule allI)
      have 8: False using 1 7 by (rule notE)
    }
    hence 9: "¬¬(? x. P x)" by (rule notI)
    show "? x. P x" using 9 by (rule notnotD)
  qed

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
       ∀x. ¬(P x) ⊢ ¬(∃x. P x)
  ------------------------------------------------------------------ *}

lemma ejercicio_17a: carmarria
  assumes 1: "∀x. ¬(P x)"
  shows   "¬(∃x. P x)"
proof -
  {assume 2: "? x. P x"
    obtain a where 3: "P a" using 2 by (rule exE)
    have 4: "¬(P a)" using 1 by (rule allE)
    have 5: False using 4 3 by (rule notE)
  }
  thus "¬(? x. P x)" by (rule notI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
       ∃x. P x ⊢ ¬(∀x. ¬(P x))
  ------------------------------------------------------------------ *}

lemma ejercicio_18a: carmarria
  assumes 1: "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
proof-
  {assume 2: "! x. ¬(P x)"
    obtain a where 3: "P a" using 1 by (rule exE)
    have 4: "¬(P a)" using 2 by (rule allE)
    have 5: False using 4 3 by (rule notE)
  }
  thus "¬(! x. ¬(P x))" by (rule notI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
       P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
  ------------------------------------------------------------------ *}

lemma ejercicio_19a: carmarria
  assumes 1: "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
proof -
  {fix b
    {assume 2: "P a"
      have 3: "! x. Q x" using 1 2 by (rule mp)
      have 4: "Q b" using 3 by (rule allE)
    }
    hence 5: "P a ⟶ Q b" by (rule impI)
  }
  thus "! x. P a ⟶ Q x" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 20. Demostrar
       {∀x y z. R x y ∧ R y z ⟶ R x z, 
        ∀x. ¬(R x x)}
       ⊢ ∀x y. R x y ⟶ ¬(R y x)
  ------------------------------------------------------------------ *}

lemma ejercicio_20a: 
  assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
          "∀x. ¬(R x x)" 
  shows   "∀x y. R x y ⟶ ¬(R y x)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     {∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
  ------------------------------------------------------------------ *}

lemma ejercicio_21a:
  assumes "∀x. P x ∨ Q x" 
          "∃x. ¬(Q x)" 
          "∀x. R x ⟶ ¬(P x)"
  shows   "∃x. ¬(R x)" 
oops

text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     {∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
  ------------------------------------------------------------------ *}

lemma ejercicio_22a:
  assumes "∀x. P x ⟶ Q x ∨ R x" 
          "¬(∃x. P x ∧ R x)"
  shows   "∀x. P x ⟶ Q x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     ∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
  ------------------------------------------------------------------ *}

lemma ejercicio_23a:
  assumes "∃x y. R x y ∨ R y x"
  shows   "∃x y. R x y"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
       (∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
  ------------------------------------------------------------------ *}

lemma ejercicio_24a: 
  "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
       (∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
  ------------------------------------------------------------------ *}

lemma ejercicio_25a: 
  "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
       ((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_26a: 
  "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar o refutar
       ((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_27a: 
  "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops


text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar o refutar
       ((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_28a: 
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}

lemma ejercicio_29: 

  "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar o refutar
       (¬(∀x. P x)) ⟷ (∃x. ¬P x)
  ------------------------------------------------------------------ *}

lemma ejercicio_30a: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
oops

section {* Ejercicios sobre igualdad *}

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar o refutar
       P a ⟹ ∀x. x = a ⟶ P x
  ------------------------------------------------------------------ *}

lemma ejercicio_31a:
  assumes "P a"
  shows   "∀x. x = a ⟶ P x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar o refutar
       ∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
  ------------------------------------------------------------------ *}

lemma ejercicio_32a:
  fixes R :: "'c ⇒ 'c ⇒ bool"
  assumes "∃x y. R x y ∨ R y x"
          "¬(∃x. R x x)"
  shows   "∃(x::'c) y. x ≠ y"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)} 
     ⊢ P (f a) a (f a)
  ------------------------------------------------------------------ *}

lemma ejercicio_33a:
  assumes "∀x. P a x x"
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows   "P (f a) a (f a)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
     ⊢ ∃z. P (f a) z (f (f a))
  ------------------------------------------------------------------ *}

lemma ejercicio_34a:
  assumes "∀x. P a x x" 
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows   "∃z. P (f a) z (f (f a))"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar o refutar
     {∀y. Q a y, 
      ∀x y. Q x y ⟶ Q (s x) (s y)} 
     ⊢ ∃z. Qa z ∧ Q z (s (s a))
  ------------------------------------------------------------------ *}

lemma ejercicio_35a:
  assumes "∀y. Q a y" 
          "∀x y. Q x y ⟶ Q (s x) (s y)" 
  shows   "∃z. Q a z ∧ Q z (s (s a))"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar o refutar
     {x = f x, odd (f x)} ⊢ odd x
  ------------------------------------------------------------------ *}

lemma ejercicio_36a:
  assumes "x = f x" and
          "odd (f x)"
  shows "odd x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar o refutar
     {x = f x, triple (f x) (f x) x} ⊢ triple x x x
  ------------------------------------------------------------------ *}

lemma ejercicio_37a:
  assumes "x = f x" and
          "triple (f x) (f x) x"
  shows "triple x x x"
oops


end