Relación 2

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)"
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. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
oops

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
oops

end