Jgiraldez
De Razonamiento automático (2010-11)
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