El problema de los infectados

José A. Alonso

19-03-2020

Decidir si es cierto que

"Existe una persona tal que si dicha persona se infecta, entonces todas las personas se infectan."

El problema consiste en completar la siguiente teoría de Isabelle/HOL:

theory El_problema_de_los_infectados
imports Main

begin

lemma "∃x. (I x ⟶ (∀y. I y))"
  by sorry

end

en la que se ha usado I(x) para representar que la persona x está infectada.

Soluciones

theory El_problema_de_los_infectados
imports Main

begin

(* 1ª solución (automática) *)
lemma "∃x. (I x ⟶ (∀y. I y))"
  by auto

(* 2ª solución (estructurada) *)
lemma "∃x. (I x ⟶ (∀y. I y))"
proof -
  have "¬ (∀y. I y) ∨ (∀y. I y)" ..
  then show "∃x. (I x ⟶ (∀y. I y))"
  proof
    assume "¬ (∀y. I y)"
    then have "∃y. ¬(I y)" by auto
    then obtain a where "¬ I a" ..
    then have "I a ⟶ (∀y. I y)" by auto
    then show "∃x. (I x ⟶ (∀y. I y))" ..
  next
    assume "∀y. I y"
    then show "∃x. (I x ⟶ (∀y. I y))" by auto
  qed
qed

(* 3ª solución (detallada con lemas auxiliares) *)

lemma aux1:
  assumes "¬ (∀y. I y)"
  shows "∃y. ¬(I y)"
proof (rule ccontr)
  assume "∄y. ¬ I y"
  have "∀y. I y"
  proof
    fix a
    show "I a"
    proof (rule ccontr)
      assume "¬ I a"
      then have "∃y. ¬ I y" by (rule exI)
      with ‹∄y. ¬ I y› show False by (rule notE)
    qed
  qed
  with assms show False by (rule notE)
qed

lemma aux2:
  assumes "¬P"
  shows   "P ⟶ Q"
proof
  assume "P"
  with assms show "Q" by (rule notE)
qed

lemma aux3:
  assumes "∄x. P x"
  shows   "∀x. ¬ P x"
proof
  fix a
  show "¬ P a"
  proof
    assume "P a"
    then have "∃x. P x" by (rule exI)
    with assms show False by (rule notE)
  qed
qed

lemma aux4:
  assumes "Q"
  shows   "∃x. (P x ⟶ Q)"
proof (rule ccontr)
  assume "∄x. (P x ⟶ Q)"
  then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3)
  then have "¬ (P a ⟶ Q)" by (rule allE)
  moreover
  have "P a ⟶ Q"
  proof
    assume "P a"
    show "Q" using assms by this
  qed
  ultimately show False by (rule notE)
qed

lemma "∃x. (I x ⟶ (∀y. I y))"
proof -
  have "¬ (∀y. I y) ∨ (∀y. I y)" by (rule excluded_middle)
  then show "∃x. (I x ⟶ (∀y. I y))"
  proof (rule disjE)
    assume "¬ (∀y. I y)"
    then have "∃y. ¬(I y)" by (rule aux1)
    then obtain a where "¬ I a" by (rule exE)
    then have "I a ⟶ (∀y. I y)" by (rule aux2)
    then show "∃x. (I x ⟶ (∀y. I y))" by (rule exI)
  next
    assume "∀y. I y"
    then show "∃x. (I x ⟶ (∀y. I y))" by (rule aux4)
  qed
qed

end