Razonamiento automático (2010-11) Razonamiento automático (2010-11)

header {* 2ª relación de ejercicios *}

theory Relacion_2
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 y de la lógica
  de predicados (allI, allE, exI y exE). 
*}

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
  proof (rule impI)
    assume 1: "∃x. ∀y. P x y"
    show "∀y. ∃x. P x y"
      proof (rule allI)
        from 1 obtain "x" where 2: "∀y. P x y" by (rule exE)
        fix y
        from 2 have 3: "P x y" by (rule allE)
        from 3 show 4: "∃x. P x y" by (rule exI)
     qed
  qed




lemma "(∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)"
proof
 { assume 1: "∀x. P x ⟶ Q"
   show "(∃x. P x) ⟶ Q"
   proof
     assume "∃x. P x"
     then obtain a where "P a" by (rule exE)
     have "P a ⟶ Q" using 1 by (rule allE)
     thus "Q" using `P a` by (rule mp)
   qed }
next
 { assume 2: "(∃x. P x) ⟶ Q"
   show "∀x. P x ⟶ Q"
   proof
     fix a
     show "P a ⟶ Q"
     proof
       assume "P a"
       hence 3: "∃x. P x" by (rule exI)
       from 2 and 3 show "Q" by (rule mp)
     qed
   qed }
qed




lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
proof
{ assume 1: "(∀ x. P x) ∧ (∀ x. Q x)"
  show "(∀ x. (P x ∧ Q x))"
    proof (rule allI)
      from 1 have 2: "(∀ x. P x)" by (rule conjE)
      from 1 have 3: "(∀ x. Q x)" by (rule conjE)
      fix a
      from 2 have 4: "P a" by (rule allE)
      from 3 have 5: "Q a" by (rule allE)
      from 4 and 5 show 6: "(P a) ∧ (Q a)" by (rule conjI)
    qed }
next
{ assume 7: "∀ x. (P x ∧ Q x)"
  show "(∀ x. P x) ∧ (∀ x. Q x)"
    proof
      { show "(∀ x. P x)"
        proof (rule allI)
          fix a
          from 7 have 8: "P a ∧ Q a" by (rule allE)
          from 8 show "P a" by (rule conjE)
        qed }
      
      { show "(∀ x. Q x)"
        proof (rule allI)
          fix a
          from 7 have 9: "P a ∧ Q a" by (rule allE)
          from 9 show "Q a" by (rule conjE)
        qed }
   qed }
qed



lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
oops
-- "Esta fórmula de la lógica de predicados es falsa.
    La implicación de izquierda a derecha sí es cierta
    y a continuación la probamos:"
lemma "((∀ x. P x) ∨ (∀ x. Q x)) ⟶ (∀ x. (P x ∨ Q x))"
proof (rule impI)
  assume 1: "(∀ x. P x) ∨ (∀ x. Q x)"
  show "∀ x. (P x ∨ Q x)"
    proof (rule allI)
      fix x
      note 1
      moreover{
       assume 11: "∀ x. P x"   
       from 11 have 111: "P x" by (rule allE)
       from 111 have "P x ∨ Q x" by (rule disjI1)}
      moreover{  
       assume 12: "∀ x. Q x"
       from 12 have 121: "Q x" by (rule allE)
       from 121 have "P x ∨ Q x" by (rule disjI2)}
      ultimately show "(P x ∨ Q x)" by (rule disjE)
    qed
qed

-- "La implicación de derecha a izquierda es falsa
    y a continuación construimos un contraejemplo.
    Supongamos un modelo en el que fuese verdadera:
    (∀ x. (P x ∨ Q x)) ∧ (∃x. ¬P x ) ∧ (∃x. ¬Q x),
    lo cual equivale a 
    (∀ x. (P x ∨ Q x)) ∧ ¬(∀ x. P x ) ∧ ¬(∀ x. Q x)
    y esto es contradictorio con 
    (∀ x. P x) ∨ (∀ x. Q x). Un ejemplo en lenguaje
    natural que ilustra esto es el siguiente:todos 
    los números reales son algebraicos o trascendentes,
    pero de ello no podemos concluir que o bien todos
    los números reales son algebraicos o bien todos los
    números reales son trascendentes."




lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
proof
  {assume 1:"((∃ x. P x) ∨ (∃ x. Q x))"
   show "(∃ x. (P x ∨ Q x))"
   proof -
     note 1
     moreover
     { assume 2: "(∃ x. P x)"
       obtain a where 3: "P a" using 2 by (rule exE)
       from 3 have 4: "P a ∨ Q a" .. 
       from 4 have "(∃ x. (P x ∨ Q x))" by (rule exI) }
     moreover
     { assume 2: "(∃ x. Q x)"
       obtain a where 3: "Q a" using 2 by (rule exE)
       from 3 have 4: "P a ∨ Q a" .. 
       from 4 have "(∃ x. (P x ∨ Q x))" by (rule exI) }
     ultimately show "(∃ x. (P x ∨ Q x))" by (rule disjE)  
   qed}
next
  {assume 1:"(∃ x. (P x ∨ Q x))"
   obtain a where 2: "P a ∨ Q a" using 1 by (rule exE)
   show "((∃ x. P x) ∨ (∃ x. Q x))" using 2
   proof 
     { assume 3: "P a"
       from 3 have 4: "(∃ x. P x)" by (rule exI)
       from 4 show "((∃ x. P x) ∨ (∃ x. Q x))" .. }
     { assume 3: "Q a"
       from 3 have 4: "(∃ x. Q x)" by (rule exI)
       from 4 show "((∃ x. P x) ∨ (∃ x. Q x))" .. }
   qed }
qed





lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
-- "Esta fórmula de la lógica de predicados es falsa
    y a continuación construimos un contraejemplo.
    Supongamos un modelo en el que fuese verdadera:
    (∀x. ∃y. P x y) ∧ (∀x. (P x x)) ∧ (∀x. ∀y. ((¬( x = y)) ⟶ ¬(P y x))) ∧ 
    ∧ (∃x. ∃y. (¬(x = y))) 
    y esto es contradictorio con (∃y. ∀x. P x y).
    Si interpretamos P como <<tener exactamente los 
    mismos padres y los mismos hermanos que>> es obvio
    que la implicación es falsa. Un contraejemplo más 
    conocido se obtiene interpretando P como la
    relación <<menor o igual que>> sobre los números
    reales, de modo que el antecedente indicaría que
    dichos números no están acotados superiormente,
    mientras que el consecuente indicaría que el
    conjunto de los reales tiene al menos una cota superior."
 


-- "La forma más corta y más automática es la que sigue"
lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
by auto



-- "Ésta es una demostración detallada del anterior lema"

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
proof (rule iffI)
  assume 11: "(¬ (∀ x. P x))"
  show "∃ x. ¬ P x"
  proof (rule ccontr)
    assume 12: "¬ (∃ x. ¬ P x)"
    note 11
    thus False
    proof (rule notE)
      show "∀ x. P x"
      proof (rule allI)
        fix x
        show "P x"
        proof (rule ccontr)
          assume 13: "¬ P x"
          from 13 have 14: "∃ x. ¬ P x " by (rule exI)
          from 12 and 14 show False by (rule notE)
        qed
      qed
    qed
  qed
next
  assume 21: "∃ x. ¬ P x" 
  show "(¬ (∀ x. P x))"
  proof (rule ccontr)
    assume 22: "¬(¬ (∀ x. P x))"
    from 22 have 23: "∀ x. P x" by (rule notnotD)
    from 21 obtain x where 24: "¬ P x" by (rule exE) 
    from 23 have 25: "P x" by (rule allE)
    from 24 and 25 show False by (rule notE)
  qed
qed 


-- "RELACIÓN DE EJERCICIOS COMPLETADA"
end