Relación 4

header {* R4: Argumentación proposicional *}

theory R4
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación formalizar y demostrar la corrección de
  los argumentos 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

text {* --------------------------------------------------------------- 
  Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Cuando tanto la temperatura como la presión atmosférica permanecen
     contantes, no llueve. La temperatura permanece constante. Por lo
     tanto, en caso de que llueva, la presión atmosférica no permanece
     constante. 
  Usar T para "La temperatura permanece constante",
       P para "La presión atmosférica permanece constante" y
       L para "Llueve".
  ------------------------------------------------------------------ *}
-- "Pedro Ros"

lemma ejercicio_1:
  assumes "T ∧ P ⟶ ¬L" and
          "T"
  shows   "L ⟶ ¬P"
proof
  assume "L"
  show "¬P"
  proof
    assume "P"
    have "T ∧ P" using `T` `P` ..
    have "¬L" using assms(1) `T ∧ P` ..
    thus "False" using `L` .. 
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Siempre que un número x es divisible por 10, acaba en 0. El número
     x no acaba en 0. Por lo tanto, x no es divisible por 10. 
  Usar D para "el número es divisible por 10" y
       C para "el número acaba en cero".
  ------------------------------------------------------------------ *}
-- "Pedro Ros"

lemma ejercicio_2:
  assumes "D⟶ C" and
          "¬C"
  shows   "¬D"
proof -
show "¬D" using assms(1) assms(2) by (rule mt)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     En cierto experimento, cuando hemos empleado un fármaco A, el
     paciente ha mejorado considerablemente en el caso, y sólo en el
     caso, en que no se haya empleado también un fármaco B. Además, o se
     ha empleado el fármaco A o se ha empleado el fármaco B. En
     consecuencia, podemos afirmar que si no hemos empleado el fármaco
     B, el paciente ha mejorado considerablemente. 
  Usar A: Hemos empleado el fármaco A.
       B: Hemos empleado el fármaco B.
       M: El paciente ha mejorado notablemente.
  ------------------------------------------------------------------ *}
text {* Pedro Ros. Si alguien consigue una demostración sin usar or1 e igual de corta,
 por favor que la ponga, aunque luego lo 
uso otra vez *}
lemma or1:
  assumes "p∨q"
          "¬q" 
  shows   "p"
proof -
  note `p∨q`
  moreover
  {assume "p"
    hence "p" by this}
  moreover
  {assume "q"
    with assms (2) have "p" ..}
  ultimately show "p" ..
qed

lemma ejercicio_3a:
  assumes 1:"A⟶ (M⟷ ¬B)" and
          2:"A ∨ B"  
  shows "¬B⟶ M"
proof
  assume "¬B"
  have "A" using 2 `¬B` by (rule or1)
  have "(M⟷ ¬B)" using 1 `A`..
  hence "(¬B⟶ M)" ..
  thus "M" using `¬B` ..
qed

-- "Raúl Montes Pajuelo"

lemma ejercicio_3b:
assumes "A ∧ M ⟷ ¬B ∧ A"
        "A ∨ B"
shows   "¬B ⟶ M"
using assms (2) 
proof
  assume "A"
   {assume "¬B"
    have "¬B ∧ A" using `¬B` `A`..
    with assms(1) have "A ∧ M"..
    hence "M"..}
  thus "¬B ⟶ M"..
  next
  assume "B"
   {assume "¬B"
    have "M" using `¬B` `B`..}
  thus "¬B ⟶ M"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente
  argumento
     Si no está el mañana ni el ayer escrito, entonces no está el mañana
     escrito. 
  Usar M: El mañana está escrito.
       A: El ayer está escrito.
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_4a: 
"(¬M ∧ ¬A)⟶ ¬ M"
proof
  assume "(¬M ∧ ¬A)"
  thus "¬M" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Me matan si no trabajo y si trabajo me matan. Me matan siempre me
     matan. 
  Usar M: Me matan.
       T: Trabajo.
  ------------------------------------------------------------------ *}
 
text {* Pedro Ros. Defino la ley del tercero exluido demostrada en la relación 3 ya. *}
lemma LEM: "P ∨ ¬P"
by auto
 
 
lemma ejercicio_5a:
assumes 1:"¬T ⟶ M" and
        2: "T ⟶ M"
shows "M"
using LEM
proof
  assume "T" 
  show "M" using 2 `T` by (rule mp)
  next
  assume "¬T"
  show "M" using 1 `¬T` ..
qed

-- "Raúl Montes Pajuelo"

lemma ejercicio_5b:
assumes "¬T ⟶ M" 
        "T ⟶ M"
shows "M"
proof (rule ccontr)
assume 1:"¬M"
with assms(1) have 2:"¬¬T" by (rule mt)
have 3: "¬T" using assms(2) 1 by (rule mt)
show False using 2 3..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si te llamé por teléfono, entonces recibiste mi llamada y no es
     cierto que no te avisé del peligro que corrías. Por consiguiente,
     como te llamé, es cierto que te avisé del peligro que corrías.
  Usar T: Te llamé por teléfono.
       R: Recibiste mi llamada.
       P: Te avisé del peligro que corrías.
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_6:
assumes "T⟶ (R∧ ¬¬P)"
shows "T⟶ P"
proof 
  assume "T"
  have "R∧ ¬¬P" using assms `T` ..
  hence "¬¬P" ..
  thus "P" by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si no hay control de nacimientos, entonces la población crece
     ilimitadamente; pero si la población crece ilimitadamente,
     aumentará el índice de pobreza. Por consiguiente, si no hay control
     de nacimientos, aumentará el índice de pobreza. 
  Usar N: Hay control de nacimientos. 
       P: La población crece ilimitadamente,
       I: Aumentará el índice de pobreza. 
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_7a:
assumes 1:"¬N⟶ P" and
        2:"P⟶ I"
shows "¬N⟶ I"
proof 
  assume "¬N"
  have "P" using 1 `¬N` ..
  with 2 show "I" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si el general era leal, hubiera obedecido las órdenes, y si era
     inteligente las hubiera comprendido. O el general desobedeció las
     órdenes o no las comprendió. Luego, el general era desleal o no era
     inteligente. 
  Usar L: El general es leal.
       O: El general obedece las órdenes.
       I: El general es inteligente.
       C: El general comprende las órdenes.
  ------------------------------------------------------------------ *}
text {* Pedro. Por alguna razón he tenido que cambiar O por P para que funcione *}
lemma ejercicio_8a:
assumes 1: "L⟶ P" and
        2: "I⟶  C" and
        3: "¬P ∨ ¬C"
shows "¬L ∨ ¬I"
 
using assms(3)
proof 
  assume "¬P"
  show "¬L ∨ ¬I"
  proof 
    show "¬L" using 1 `¬P` by (rule mt)
  qed
next
  assume "¬C"
  show "¬L ∨ ¬I"
  proof -
    have "¬I" using 2 `¬C` by (rule mt)
    show "¬L ∨ ¬I" using `¬I` by (rule disjI2)
  qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
     haría. Si Dios fuera incapaz de evitar el mal, no sería
     omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
     evita el mal. Si Dios existe, es omnipotente y no es
     malévolo. Luego, Dios no existe. 
  Usar C: Dios es capaz de evitar el mal.
       Q: Dios quiere evitar el mal.
       O: Dios es omnipotente.
       M: Dios es malévolo.
       P: Dios evita el mal.
       E: Dios existe.
  ------------------------------------------------------------------ *}
text {* Pedro. Cambio O por W para que me funcione. Y defino otra regla básica *}
lemma negconj:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p∨p"..
  moreover
   {assume "¬p"
    hence "¬p∨¬q"..}
  moreover
   {assume "p"
    have "¬q∨q"..
    moreover
    {assume "¬q"
     hence "¬p∨¬q"..}
    moreover
    {assume "q"
     with `p`have "p∧q"..
     with `¬(p∧q)` have "¬p∨¬q"..}
    ultimately have "¬p∨¬q"..}
  ultimately show "¬p∨¬q"..
qed
 
lemma ejercicio_10:
assumes 1:"(C∧Q)⟶ P" and
        2:"¬C ⟶ ¬W" and
        3:"¬Q ⟶ M" and
        4: "¬P" and
        5: "E ⟶ (W ∧ ¬M)"
shows "¬E"
proof 
  have 6: "¬(C∧Q)" using 1 4 by (rule mt)
  hence 7: "¬C ∨ ¬Q" by (rule negconj)
  assume "E"
  show "False"
  proof -
    have 8: "W∧ ¬M" using 5 `E`..
    hence "W" ..
    have "¬M" using 8 ..
    have 9: "¬¬Q" using 3 `¬M` by (rule mt)
    hence "Q" by (rule notnotD)
    have 10: "¬C" using 7 9 by (rule or1)
    have "¬W" using 2 10 ..
    thus "False" using `W` ..
  qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Nadie más que Pedro, Quintín y Raúl están bajo sospecha y al menos
     uno es traidor. Pedro nunca trabaja sin llevar al menos un cómplice
     (que puede ser Quintín o Raúl). Raúl es leal. Por lo tanto,
     Pedro es traidor.
  Usar p: Pedro es traidor.
       q : Quintín es traidor.
       r : Raúl es traidor. 
  ------------------------------------------------------------------ *}
text {* No es cierto como se demuestra con {¬p,q,¬r}. Además isabelle me dice que es mentira al 
hacerlo con auto, podemos hacer que Pedro sea traidor (p) pero no es siempre cierto, puede serlo 
Quintín sólo, o Quintín y Pedro, lo que está claro que el traidor es Quintín siempre. aun así lo 
formalizo y con quickcheck (para que los usuarios de jedit, puedan verlo) *}
 
lemma ejercicio_10a:
assumes 1:"p∨q∨r" and
        2:"p⟶ (q∨r)" and
        3:"¬r"  
shows "p"
quickcheck
oops

text {* --------------------------------------------------------------- 
  Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si la válvula está abierta o la monitorización está preparada,
     entonces se envía una señal de reconocimiento y un mensaje de
     funcionamiento al controlador del ordenador. Si se envía un mensaje 
     de funcionamiento al controlador del ordenador o el sistema está en 
     estado normal, entonces se aceptan las órdenes del operador. Por lo
     tanto, si la válvula está abierta, entonces se aceptan las órdenes
     del operador. 
  Usar A: La válvula está abierta.
       P : La monitorización está preparada.
       R : Envía una señal de reconocimiento.
       F : Envía un mensaje de funcionamiento.
       N : El sistema está en estado normal.
       O : Se aceptan órdenes del operador.
  ------------------------------------------------------------------ *}
text {* Pedro Ros. Cambio W por O *}
 
lemma ejercicio_11:
assumes 1:"(A∨P)⟶ (R∧F)" and
        2:"F∨N ⟶ W"
shows "A⟶ W"
proof
  assume "A"
  show "W"
    proof -
      have 3:"A∨P" using `A` by (rule disjI1)
      have 4:"R∧F" using 1 3 ..
      hence 5: "F" ..
      hence 6: "F∨N" ..
      show "W" using 2 6 ..
    qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
     embargo, si trabajo no gozo de la vida, mientras que si no trabajo
     no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
  dinero. 
  Usar p: Trabajo
       q: Gano dinero.
       r: Gozo de la vida.
  ------------------------------------------------------------------ *}
-- "Pedro Ros"

lemma ejercicio_12: 
assumes 1:"(p⟶q)∧(¬p⟶r)" and
        2:"(p⟶¬r)∧(¬p⟶¬q)"
shows   "r ⟷¬q"
proof
assume r
show "¬q"
  proof -
  have 3:"p⟶¬r" using 2 ..
  have "¬¬r" using `r` by (rule notnotI)
  with 3 have 4: "¬p" by (rule mt)
  have 5:"¬p⟶¬q" using 2 ..
  show "¬q" using 5 4 by (rule mp)
  qed
next
assume "¬q"
show "r"
  proof -
  have 3:"p⟶q" using 1 ..
  have 4: "¬p" using 3 `¬q` by (rule mt)
  have 5: "¬p⟶r" using 1 ..
  show "r" using 5 4 ..
  qed
qed

end