Acciones

Usuario discusión

Diferencia entre revisiones de «Jgiraldez»

De Razonamiento automático (2010-11)

(RA_Relacion_1)
 
(Nueva sección: →‎RA_Relacion_2)
Línea 1: Línea 1:
 
== RA_Relacion_1 ==
 
== RA_Relacion_1 ==
 +
 +
theory Relacion_2
 +
imports Main
 +
begin
 +
 +
(* 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
 +
      fix a
 +
      from 7 have 8: "P a ∧ Q a" by (rule allE)
 +
      from 8 have 9: "P a" by (rule conjE)
 +
      (* seguir... *)
 +
      from 8 have 11: "Q a" by (rule allE)
 +
      (* seguir... *)
 +
    qed
 +
}
 +
qed     
 +
     
 +
oops
 +
 +
lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
 +
oops
 +
 +
lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
 +
oops
 +
 +
lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
 +
oops
 +
(*
 +
proof (rule impI)
 +
  assume 1: "∀x. ∃y. P x y"
 +
  show "∃y. ∀x. P x y"
 +
    proof (rule exI)
 +
      show " ∀x. P x y"
 +
        proof (rule allI)
 +
          fix x
 +
          from 1 have 2: "∃y. P x y" by (rule allE)
 +
          from 2 obtain y where 3: "P x y" by (rule exE)
 +
          thus ?thesis ..
 +
        qed
 +
*)
 +
 +
lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
 +
proof
 +
{
 +
  assume 1: "¬ (∀ x. P x)"
 +
  show "∃ x. ¬ P x"
 +
    proof
 +
     
 +
 +
    qed
 +
}
 +
next
 +
{
 +
  assume 2: "∃ x. ¬ P x"
 +
  show "¬ (∀ x. P x)"
 +
    proof
 +
     
 +
    qed
 +
}
 +
qed
 +
 +
end
 +
 +
== RA_Relacion_2 ==
  
 
theory Relacion_2
 
theory Relacion_2

Revisión del 17:36 3 feb 2011

RA_Relacion_1

theory Relacion_2 imports Main begin

(* 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
     fix a
     from 7 have 8: "P a ∧ Q a" by (rule allE)
     from 8 have 9: "P a" by (rule conjE)
     (* seguir... *)
     from 8 have 11: "Q a" by (rule allE)
     (* seguir... *)
   qed

} qed

oops

lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))" oops

lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))" oops

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)" oops (* proof (rule impI) 

 assume 1: "∀x. ∃y. P x y"
 show "∃y. ∀x. P x y"
   proof (rule exI)
     show " ∀x. P x y"
       proof (rule allI)
         fix x
         from 1 have 2: "∃y. P x y" by (rule allE)
         from 2 obtain y where 3: "P x y" by (rule exE)
         thus ?thesis ..
       qed
  • )

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)" proof { 

 assume 1: "¬ (∀ x. P x)" 
 show "∃ x. ¬ P x"
   proof
     

   qed

} next { 

 assume 2: "∃ x. ¬ P x"
 show "¬ (∀ x. P x)"
   proof
     
   qed

} qed

end

RA_Relacion_2

theory Relacion_2 imports Main begin

(* 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
     fix a
     from 7 have 8: "P a ∧ Q a" by (rule allE)
     from 8 have 9: "P a" by (rule conjE)
     (* seguir... *)
     from 8 have 11: "Q a" by (rule allE)
     (* seguir... *)
   qed

} qed

oops

lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))" oops

lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))" oops

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)" oops (* proof (rule impI) 

 assume 1: "∀x. ∃y. P x y"
 show "∃y. ∀x. P x y"
   proof (rule exI)
     show " ∀x. P x y"
       proof (rule allI)
         fix x
         from 1 have 2: "∃y. P x y" by (rule allE)
         from 2 obtain y where 3: "P x y" by (rule exE)
         thus ?thesis ..
       qed
  • )

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)" proof { 

 assume 1: "¬ (∀ x. P x)" 
 show "∃ x. ¬ P x"
   proof
     

   qed

} next { 

 assume 2: "∃ x. ¬ P x"
 show "¬ (∀ x. P x)"
   proof
     
   qed

} qed

end

Obtenido de «https://www.glc.us.es/~jalonso/RA2010/index.php?title=Usuario_discusión:Jgiraldez&oldid=62»