T2 - Lógica matemática y fundamentos (2012-13)

header {* T2: Deducción natural en lógica de primer orden *}

theory T2
imports Main 
begin

lemma ej_1:
  assumes "∀x. P(x) ⟶  Q(x)"
          "∀y. Q(y) ⟶ R(y)"
  shows "(∀z. P(z)) ⟶  (∀z. R(z))"
  using assms
  by auto

lemma ej_2:
  assumes "¬ (∃x y. P(x,y) ⟶ Q(x,y))"
  shows "∀x y. P(x,y) ∧ ¬Q(x,y)"
using assms
by auto


lemma ej_3:
  assumes "(∀x. P(x)) ∧ (∀y. Q(y))"
          "∀y. Q(y) ⟶ R(y)"
  shows "∀z. P(z) ∧ R(z)"
using assms
by auto


lemma ej_4:
  assumes "¬ (∃x y. P(x,y) ∧ ¬ Q(y,x))"
  shows "∀x y. P (x,y) ⟶ Q(y,x)"
using assms
by auto

lemma ej_5:
  assumes "∃x. P(x) ∧ Q(x)"
          "∀y. P(y) ⟶ R(y)" 
  shows "∃x. R(x) ∧ Q(x)"
using assms
by auto


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)"
using assms
by metis


lemma ej_7:
  assumes "∃x y. R(x,y) ∨ R(y,x)" 
  shows "∃x y. R(x,y)"
using assms
by auto


lemma ej_8:
  assumes "∀x. P(x) ⟶ (∃y. Q(y))" 
  shows "∀x. ∃y. P(x) ⟶ Q(y)"
  using assms
  by auto


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))"
using assms
by auto


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)"
using assms
by auto


lemma ej_11:
  assumes "∀x. P (x) ⟶ (R(x) ⟶ S(x))"
          "∃x. P (x) ∨ ¬R(x)" 
  shows "∃x. R(x) ⟶ S(x)"
using assms
by auto


lemma ej_12:
  assumes "(∃x. P(x)) ⟶ (∀y. Q(y))"
  shows "∃x. ∀y. P(x) ⟶ Q(y)"
using assms
by auto


lemma ej_13:
  assumes "∃y z. (∀x. ¬R(x,y)) ∨ (∀x. ¬R(x,z))"
  shows "¬ (∀y z. ∃x. R(x,y) ∧ R(x,z))"
using assms
by auto


lemma ej_14:
  assumes "∃x. P (x) ⟶ (∀y. P (y) ⟶ Q(y))"
          "¬(∃x. Q(x))"
  shows "¬(∀x. P(x))"
using assms
by auto


lemma ej_15:
  assumes "¬(∃x. P(x) ∧ ¬(∀y. Q(y) ⟶ R(x,y)))"
          "∃x. P(x) ∧ (∃y. ¬R(x,y))"
  shows "∃x. ¬Q(x)"
using assms
by auto


lemma ej_16:
  assumes "∀x y.(∃z. R(y,z)) ⟶ R(x,y)"
          "∃x y. R(x,y)"
  shows "∀x y. R(x,y)"
  using assms
  by metis


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)"
using assms
by auto


lemma ej_18: "¬(∃x. ∀y. P(y,x) ⟷ ¬P (y,y))"
by auto


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)"
using assms
by auto


lemma ej_20:
  assumes "∀x. P(x) ⟶ (∀y. Q(y) ⟶ R(x,y))"
          "∃x. P(x) ∧ (∃y. ¬R(x,y))"
  shows "¬(∀x. Q(x))"
using assms
by auto


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)"
using assms
by metis


lemma ej_22:
  assumes "∀x. P(x)"
          "∀x. P (x) ⟶ Q(x) ∨ R(x)"
          "∃x. ¬Q(x)"
  shows "∃x. R(x)"
using assms
by auto


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)"
using assms
by auto


lemma ej_24:
  assumes "∀x y. (∃z. R(y,z)) ⟶ R(x,y)"
          "∃x y. R(x,y)"
  shows "∀x y. R(x,y)"
using assms
by metis


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)"
using assms
by metis

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)"
using assms
by metis


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))"
using assms
by auto


lemma ej_28:
  assumes "¬(∃x. P(x) ∧C(x))"
          "∃x. C(x) ∧ Q(x)"
  shows "∃x. Q(x) ∧ ¬P(x)"
using assms
by auto


lemma ej_29a:
  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)"
using assms
by metis

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)"
proof -
  have "f(0,g(0)) = 0" using assms(2) ..
  hence 1:"f(g(0),0) = 0" using assms(3) by auto
  have "f(g(0),0) = g(0)" using assms(1) ..
  hence "0 = g(0)" using 1 by auto
  thus "∃x. x = g(x)" ..
qed


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"
using assms
by metis


lemma ej_31:
  assumes "∃x. H(x)"
          "∀x y. H(x) ∧ H(y) ⟶  x = y"
  shows   "∃x. H(x) ∧ (∀y. H(y) ⟶  x = y)"
using assms
by auto

lemma ej_32:
  assumes "∀x. (∃y. K(x,y)) ⟶   (∃z. K(z,x))"
          "∀x. K(x,g) ∧ x = b"
  shows   "∃z. K(z,b)"
using assms
by auto


lemma ej_33:
  assumes "∃x. W(x) ∧ (∀x y. (W(x) ∧ W(y) ⟶ x = y))" 
  shows "∃x. W(x) ∧ (∀y. W(y) ⟶ x = y)"
using assms
by auto


end
T2

De Lógica matemática y fundamentos (2012-13)
