Mjoseh: Protegió «T2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2013-04-10T07:41:49Z

Protegió «T2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Mjoseh en 07:41 10 abr 2013

2013-04-10T07:41:23Z

Mjoseh: Página creada con ' 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)" "∀...'

2013-04-09T16:17:29Z

Página creada con '<source lang ="isar"> 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)" "∀...'

Página nueva

<source lang ="isar">

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
</source>

← Revisión anterior	Revisión del 07:41 10 abr 2013
(Sin diferencias)

T2 - Historial de revisiones

Mjoseh: Protegió «T2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Mjoseh en 07:41 10 abr 2013

Mjoseh: Página creada con ' 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)" "∀...'