header {* E2: Deducción natural en lógica de primer orden *}
theory E2
imports Main
begin
lemma ej_1:
assumes "∀x. P(x) ⟶ Q(x)"
"∀y. Q(y) ⟶ R(y)"
shows "(∀z. P(z)) ⟶ (∀z. R(z))"
oops
lemma ej_2:
assumes "¬ (∃x y. P(x,y) ⟶ Q(x,y))"
shows "∀x y. P(x,y) ∧ ¬Q(x,y)"
oops
lemma ej_3:
assumes "(∀x. P(x)) ∧ (∀y. Q(y))"
"∀y. Q(y) ⟶ R(y)"
shows "∀z. P(z) ∧ R(z)"
oops
lemma ej_4:
assumes "¬ (∃x y. P(x,y) ∧ ¬ Q(y,x))"
shows "∀x y. P (x,y) ⟶ Q(y,x)"
oops
lemma ej_5:
assumes "∃x. P(x) ∧ Q(x)"
"∀y. P(y) ⟶ R(y)"
shows "∃x. R(x) ∧ Q(x)"
oops
lemma ej_6:
assumes "∀x. R(x,x)"
"∀x y z.¬ R(x,y) ∧ ¬R(y,z) ⟶ ¬R(x,z)"
shows "∀x y. R(x,y) ∨ R(y,x)"
oops
lemma ej_7:
assumes "∃x y. R(x,y) ∨ R(y,x)"
shows "∃x y. R(x,y)"
oops
lemma ej_8:
assumes "∀x. P(x) ⟶ (∃y. Q(y))"
shows "∀x. ∃y. P(x) ⟶ Q(y)"
oops
lemma ej_9:
assumes "∃x. ∀y. B(y) ⟶ A(x,y)"
"∃x. ∀y. (∀z. B(z) ⟶ A(y,z)) ⟶ ¬S(x,y)"
shows "∃x. ¬(∀y. S(x,y))"
oops
lemma ej_10:
assumes "∀x. Q(x) ⟶ ¬R(x)"
"∀x. P (x) ⟶ Q(x) ∨ S(x)"
"∃x. P (x) ∧ R(x)"
shows "∃x. P(x) ∧ S(x)"
oops
lemma ej_11:
assumes "∀x. P (x) ⟶ (R(x) ⟶ S(x))"
"∃x. P (x) ∨ ¬R(x)"
shows "∃x. R(x) ⟶ S(x)"
oops
lemma ej_12:
assumes "(∃x. P(x)) ⟶ (∀y. Q(y))"
shows "∃x. ∀y. P(x) ⟶ Q(y)"
oops
lemma ej_13:
assumes "∃y z. (∀x. ¬R(x,y)) ∨ (∀x. ¬R(x,z))"
shows "¬ (∀y z. ∃x. R(x,y) ∧ R(x,z))"
oops
lemma ej_14:
assumes "∃x. P (x) ⟶ (∀y. P (y) ⟶ Q(y))"
"¬(∃x. Q(x))"
shows "¬(∀x. P(x))"
oops
lemma ej_15:
assumes "¬(∃x. P(x) ∧ ¬(∀y. Q(y) ⟶ R(x,y)))"
"∃x. P(x) ∧ (∃y. ¬R(x,y))"
shows "∃x. ¬Q(x)"
oops
lemma ej_16:
assumes "∀x y.(∃z. R(y,z)) ⟶ R(x,y)"
"∃x y. R(x,y)"
shows "∀x y. R(x,y)"
oops
lemma ej_17:
assumes "(∃x. P(x) ∧ ¬Q(x)) ⟶ (∀y. P(y) ⟶ R(y))"
"∃x. P(x) ∧ S(x)"
"∀x. P(x) ⟶ ¬R(x)"
shows "∃x. S(x) ∧ Q(x)"
oops
lemma ej_18: "¬(∃x. ∀y. P(y,x) ⟷ ¬P (y,y))"
oops
lemma ej_19:
assumes "∀x. (∃y. R(x,y)) ⟶ (∃y. ∀z. R(y,z) ∧ R(x,y))"
"∃x y. R(x,y)"
shows "∃x. ∀y. R(x,y)"
oops
lemma ej_20:
assumes "∀x. P(x) ⟶ (∀y. Q(y) ⟶ R(x,y))"
"∃x. P(x) ∧ (∃y. ¬R(x,y))"
shows "¬(∀x. Q(x))"
oops
lemma ej_21:
assumes "∀x. R(x,x)"
"∀x y z. ¬R(x,y) ∧ ¬R(y,z) ⟶ ¬R(x,z)"
shows "∀x y. R(x,y) ∨ R(y,x)"
oops
lemma ej_22:
assumes "∀x. P(x)"
"∀x. P (x) ⟶ Q(x) ∨ R(x)"
"∃x. ¬Q(x)"
shows "∃x. R(x)"
oops
lemma ej_23:
assumes "∀x y. R(x,y) ⟶ R(y,x)"
"∀x y. R(x,y) ∨ R(y,x)"
shows "∀x y z. ¬R(x,y) ∧ ¬R(y,z) ⟶¬R(x,z)"
oops
lemma ej_24:
assumes "∀x y. (∃z. R(y,z)) ⟶ R(x,y)"
"∃x y. R(x,y)"
shows "∀x y. R(x,y)"
oops
lemma ej_25:
assumes "∀x y. (∃z. R(z,y) ∧ ¬R(x,z)) ⟶ R(x,y)"
"¬(∃x. R(x,x))"
shows "∀x y. ¬R(y,x) ⟶ ¬R(x,y)"
oops
lemma ej_26:
assumes "∀x y z. P(x,y) ∧ P (y,z) ⟶ R(x,z)"
"∀x. ∃y. P (x,y)"
shows "∀x. ∃y. R(x,y)"
oops
lemma ej_27:
assumes "∀x. P(x) ⟶ ((∃y. Q(x,y)) ⟶ (∃y. Q(y,x)))"
"∀x. (∃y. Q(y,x)) ⟶ Q(x,x)"
"¬(∃x. Q(x,x))"
shows "∀x. P(x) ⟶ (∀y. ¬Q(x,y))"
oops
lemma ej_28:
assumes "¬(∃x. P(x) ∧C(x))"
"∃x. C(x) ∧ Q(x)"
shows "∃x. Q(x) ∧ ¬P(x)"
oops
lemma ej_29:
assumes "∀x. f(x,0) = x"
"∀x. f(x,g(x)) = 0"
"∀x y. f(x,y) = f(y,x)"
shows "∃x. x = g(x)"
oops
lemma ej_30:
assumes "∀x. f(x,0) = x"
"∀x. f(x,g(x)) = 0"
"∀x y. f(x,y) = f(y,x)"
shows "∃x. f(x,x) = x"
oops
lemma ej_31:
assumes "∃x. H(x)"
"∀x y. H(x) ∧ H(y) ⟶ x = y"
shows "∃x. H(x) ∧ (∀y. H(y) ⟶ x = y)"
oops
lemma ej_32:
assumes "∀x. (∃y. K(x,y)) ⟶ (∃z. K(z,x))"
"∀x. K(x,g) ∧ x = b"
shows "∃z. K(z,b)"
oops
lemma ej_33:
assumes "∃x. W(x) ∧ (∀x y. (W(x) ∧ W(y) ⟶ x = y))"
shows "∃x. W(x) ∧ (∀y. W(y) ⟶ x = y)"
oops
end