Diferencia entre revisiones de «T2»
De Lógica matemática y fundamentos (2012-13)
(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)" "∀...') |
|||
| Línea 1: | Línea 1: | ||
<source lang ="isar"> | <source lang ="isar"> | ||
| − | header {* | + | header {* E2: Deducción natural en lógica de primer orden *} |
| − | theory | + | theory E2 |
imports Main | imports Main | ||
begin | begin | ||
| Línea 11: | Línea 11: | ||
"∀y. Q(y) ⟶ R(y)" | "∀y. Q(y) ⟶ R(y)" | ||
shows "(∀z. P(z)) ⟶ (∀z. R(z))" | shows "(∀z. P(z)) ⟶ (∀z. R(z))" | ||
| − | + | oops | |
| − | |||
lemma ej_2: | lemma ej_2: | ||
assumes "¬ (∃x y. P(x,y) ⟶ Q(x,y))" | assumes "¬ (∃x y. P(x,y) ⟶ Q(x,y))" | ||
shows "∀x y. P(x,y) ∧ ¬Q(x,y)" | shows "∀x y. P(x,y) ∧ ¬Q(x,y)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_3: | lemma ej_3: | ||
| Línea 25: | Línea 22: | ||
"∀y. Q(y) ⟶ R(y)" | "∀y. Q(y) ⟶ R(y)" | ||
shows "∀z. P(z) ∧ R(z)" | shows "∀z. P(z) ∧ R(z)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_4: | lemma ej_4: | ||
assumes "¬ (∃x y. P(x,y) ∧ ¬ Q(y,x))" | assumes "¬ (∃x y. P(x,y) ∧ ¬ Q(y,x))" | ||
shows "∀x y. P (x,y) ⟶ Q(y,x)" | shows "∀x y. P (x,y) ⟶ Q(y,x)" | ||
| − | + | oops | |
| − | |||
lemma ej_5: | lemma ej_5: | ||
| Línea 39: | Línea 33: | ||
"∀y. P(y) ⟶ R(y)" | "∀y. P(y) ⟶ R(y)" | ||
shows "∃x. R(x) ∧ Q(x)" | shows "∃x. R(x) ∧ Q(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_6: | lemma ej_6: | ||
| Línea 47: | Línea 39: | ||
"∀x y z.¬ R(x,y) ∧ ¬R(y,z) ⟶ ¬R(x,z)" | "∀x y z.¬ R(x,y) ∧ ¬R(y,z) ⟶ ¬R(x,z)" | ||
shows "∀x y. R(x,y) ∨ R(y,x)" | shows "∀x y. R(x,y) ∨ R(y,x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_7: | lemma ej_7: | ||
assumes "∃x y. R(x,y) ∨ R(y,x)" | assumes "∃x y. R(x,y) ∨ R(y,x)" | ||
shows "∃x y. R(x,y)" | shows "∃x y. R(x,y)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_8: | lemma ej_8: | ||
assumes "∀x. P(x) ⟶ (∃y. Q(y))" | assumes "∀x. P(x) ⟶ (∃y. Q(y))" | ||
shows "∀x. ∃y. P(x) ⟶ Q(y)" | shows "∀x. ∃y. P(x) ⟶ Q(y)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_9: | lemma ej_9: | ||
| Línea 69: | Línea 55: | ||
"∃x. ∀y. (∀z. B(z) ⟶ A(y,z)) ⟶ ¬S(x,y)" | "∃x. ∀y. (∀z. B(z) ⟶ A(y,z)) ⟶ ¬S(x,y)" | ||
shows "∃x. ¬(∀y. S(x,y))" | shows "∃x. ¬(∀y. S(x,y))" | ||
| − | + | oops | |
| − | + | ||
| − | |||
| − | |||
lemma ej_10: | lemma ej_10: | ||
assumes "∀x. Q(x) ⟶ ¬R(x)" | assumes "∀x. Q(x) ⟶ ¬R(x)" | ||
| Línea 78: | Línea 62: | ||
"∃x. P (x) ∧ R(x)" | "∃x. P (x) ∧ R(x)" | ||
shows "∃x. P(x) ∧ S(x)" | shows "∃x. P(x) ∧ S(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_11: | lemma ej_11: | ||
| Línea 86: | Línea 68: | ||
"∃x. P (x) ∨ ¬R(x)" | "∃x. P (x) ∨ ¬R(x)" | ||
shows "∃x. R(x) ⟶ S(x)" | shows "∃x. R(x) ⟶ S(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_12: | lemma ej_12: | ||
assumes "(∃x. P(x)) ⟶ (∀y. Q(y))" | assumes "(∃x. P(x)) ⟶ (∀y. Q(y))" | ||
shows "∃x. ∀y. P(x) ⟶ Q(y)" | shows "∃x. ∀y. P(x) ⟶ Q(y)" | ||
| − | + | oops | |
| − | + | ||
| − | |||
| − | |||
lemma ej_13: | lemma ej_13: | ||
assumes "∃y z. (∀x. ¬R(x,y)) ∨ (∀x. ¬R(x,z))" | assumes "∃y z. (∀x. ¬R(x,y)) ∨ (∀x. ¬R(x,z))" | ||
shows "¬ (∀y z. ∃x. R(x,y) ∧ R(x,z))" | shows "¬ (∀y z. ∃x. R(x,y) ∧ R(x,z))" | ||
| − | + | oops | |
| − | + | ||
| − | |||
| − | |||
lemma ej_14: | lemma ej_14: | ||
assumes "∃x. P (x) ⟶ (∀y. P (y) ⟶ Q(y))" | assumes "∃x. P (x) ⟶ (∀y. P (y) ⟶ Q(y))" | ||
"¬(∃x. Q(x))" | "¬(∃x. Q(x))" | ||
shows "¬(∀x. P(x))" | shows "¬(∀x. P(x))" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_15: | lemma ej_15: | ||
| Línea 116: | Línea 90: | ||
"∃x. P(x) ∧ (∃y. ¬R(x,y))" | "∃x. P(x) ∧ (∃y. ¬R(x,y))" | ||
shows "∃x. ¬Q(x)" | shows "∃x. ¬Q(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_16: | lemma ej_16: | ||
| Línea 124: | Línea 96: | ||
"∃x y. R(x,y)" | "∃x y. R(x,y)" | ||
shows "∀x y. R(x,y)" | shows "∀x y. R(x,y)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_17: | lemma ej_17: | ||
| Línea 133: | Línea 103: | ||
"∀x. P(x) ⟶ ¬R(x)" | "∀x. P(x) ⟶ ¬R(x)" | ||
shows "∃x. S(x) ∧ Q(x)" | shows "∃x. S(x) ∧ Q(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_18: "¬(∃x. ∀y. P(y,x) ⟷ ¬P (y,y))" | lemma ej_18: "¬(∃x. ∀y. P(y,x) ⟷ ¬P (y,y))" | ||
| − | + | oops | |
| − | |||
lemma ej_19: | lemma ej_19: | ||
| Línea 145: | Línea 112: | ||
"∃x y. R(x,y)" | "∃x y. R(x,y)" | ||
shows "∃x. ∀y. R(x,y)" | shows "∃x. ∀y. R(x,y)" | ||
| − | + | oops | |
| − | + | ||
| Línea 153: | Línea 120: | ||
"∃x. P(x) ∧ (∃y. ¬R(x,y))" | "∃x. P(x) ∧ (∃y. ¬R(x,y))" | ||
shows "¬(∀x. Q(x))" | shows "¬(∀x. Q(x))" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_21: | lemma ej_21: | ||
| Línea 161: | Línea 126: | ||
"∀x y z. ¬R(x,y) ∧ ¬R(y,z) ⟶ ¬R(x,z)" | "∀x y z. ¬R(x,y) ∧ ¬R(y,z) ⟶ ¬R(x,z)" | ||
shows "∀x y. R(x,y) ∨ R(y,x)" | shows "∀x y. R(x,y) ∨ R(y,x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_22: | lemma ej_22: | ||
| Línea 170: | Línea 133: | ||
"∃x. ¬Q(x)" | "∃x. ¬Q(x)" | ||
shows "∃x. R(x)" | shows "∃x. R(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_23: | lemma ej_23: | ||
| Línea 178: | Línea 139: | ||
"∀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)" | shows "∀x y z. ¬R(x,y) ∧ ¬R(y,z) ⟶¬R(x,z)" | ||
| − | + | oops | |
| − | + | ||
| − | |||
| − | |||
lemma ej_24: | lemma ej_24: | ||
assumes "∀x y. (∃z. R(y,z)) ⟶ R(x,y)" | assumes "∀x y. (∃z. R(y,z)) ⟶ R(x,y)" | ||
"∃x y. R(x,y)" | "∃x y. R(x,y)" | ||
shows "∀x y. R(x,y)" | shows "∀x y. R(x,y)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_25: | lemma ej_25: | ||
| Línea 194: | Línea 151: | ||
"¬(∃x. R(x,x))" | "¬(∃x. R(x,x))" | ||
shows "∀x y. ¬R(y,x) ⟶ ¬R(x,y)" | shows "∀x y. ¬R(y,x) ⟶ ¬R(x,y)" | ||
| − | + | oops | |
| − | |||
lemma ej_26: | lemma ej_26: | ||
| Línea 201: | Línea 157: | ||
"∀x. ∃y. P (x,y)" | "∀x. ∃y. P (x,y)" | ||
shows "∀x. ∃y. R(x,y)" | shows "∀x. ∃y. R(x,y)" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_27: | lemma ej_27: | ||
| Línea 210: | Línea 164: | ||
"¬(∃x. Q(x,x))" | "¬(∃x. Q(x,x))" | ||
shows "∀x. P(x) ⟶ (∀y. ¬Q(x,y))" | shows "∀x. P(x) ⟶ (∀y. ¬Q(x,y))" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_28: | lemma ej_28: | ||
| Línea 218: | Línea 170: | ||
"∃x. C(x) ∧ Q(x)" | "∃x. C(x) ∧ Q(x)" | ||
shows "∃x. Q(x) ∧ ¬P(x)" | shows "∃x. Q(x) ∧ ¬P(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
lemma ej_29: | lemma ej_29: | ||
| Línea 235: | Línea 177: | ||
"∀x y. f(x,y) = f(y,x)" | "∀x y. f(x,y) = f(y,x)" | ||
shows "∃x. x = g(x)" | shows "∃x. x = g(x)" | ||
| − | + | oops | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
lemma ej_30: | lemma ej_30: | ||
| Línea 249: | Línea 184: | ||
"∀x y. f(x,y) = f(y,x)" | "∀x y. f(x,y) = f(y,x)" | ||
shows "∃x. f(x,x) = x" | shows "∃x. f(x,x) = x" | ||
| − | + | oops | |
| − | |||
| − | |||
lemma ej_31: | lemma ej_31: | ||
| Línea 257: | Línea 190: | ||
"∀x y. H(x) ∧ H(y) ⟶ x = y" | "∀x y. H(x) ∧ H(y) ⟶ x = y" | ||
shows "∃x. H(x) ∧ (∀y. H(y) ⟶ x = y)" | shows "∃x. H(x) ∧ (∀y. H(y) ⟶ x = y)" | ||
| − | + | oops | |
| − | |||
lemma ej_32: | lemma ej_32: | ||
| Línea 264: | Línea 196: | ||
"∀x. K(x,g) ∧ x = b" | "∀x. K(x,g) ∧ x = b" | ||
shows "∃z. K(z,b)" | shows "∃z. K(z,b)" | ||
| − | + | oops | |
| − | + | ||
| − | |||
| − | |||
lemma ej_33: | lemma ej_33: | ||
assumes "∃x. W(x) ∧ (∀x y. (W(x) ∧ W(y) ⟶ x = y))" | assumes "∃x. W(x) ∧ (∀x y. (W(x) ∧ W(y) ⟶ x = y))" | ||
shows "∃x. W(x) ∧ (∀y. W(y) ⟶ x = y)" | shows "∃x. W(x) ∧ (∀y. W(y) ⟶ x = y)" | ||
| − | + | oops | |
| − | + | ||
| − | |||
| − | |||
end | end | ||
</source> | </source> | ||
Revisión del 09:41 10 abr 2013
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