Rel 10 - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-16T07:47:34Z

Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Protegió «Rel 10» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2011-03-15T05:14:13Z

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

Jalonso en 05:13 15 mar 2011

2011-03-15T05:13:56Z

Jalonso en 05:13 15 mar 2011

2011-03-15T05:13:09Z

Jalonso: Página creada con ' theory Relacion_10 imports Main begin section {* Deducción natural de primer orden } text { Los ejercicios de esta relación deben de resolverse usan...'

2011-03-15T05:11:42Z

Página creada con '<source lang="isar"> theory Relacion_10 imports Main begin section {* Deducción natural de primer orden *} text {* Los ejercicios de esta relación deben de resolverse usan...'

Página nueva

<source lang="isar">
theory Relacion_10
imports Main
begin

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
y se primer orden
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
assumes "∃x. ¬P x"
shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
oops

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬Q x"
shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
assumes "∀x. ∀y. P x y"
shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
assumes "∃x. ∃y. P x y"
shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
assumes "∀x.∀y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
assumes "¬(∀x. ¬P x)"
shows "∃x. P x"
oops

lemma ejercicio_17:
assumes "∀x. ¬P x"
shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
"∀x. ¬R x x"
shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
assumes "∀x. P x ∨ Q x" and
"∃x. ¬Q x" and
"∀x. R x ⟶ ¬P x"
shows "∃x. ¬R x"
oops

lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x" and
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
assumes "∃x.∃y. R x y ∨ R y x"
shows "∃x.∃y. R x y"
oops

end
</source>

@@ Línea 1: / Línea 1: @@
-<source lang="isar">
+<source lang="isabelle">
 theory Relacion_10
 imports Main

← Revisión anterior	Revisión del 05:14 15 mar 2011
(Sin diferencias)

@@ Línea 7: / Línea 7: @@
 text {* Los ejercicios de esta relación deben de resolverse usando sólo
-   las reglas básicas de la deducción natural proposicional y de primer orden:
+   las reglas básicas de la deducción natural proposicional y de primer
    · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
    · conjunct1:  P ∧ Q ⟹ P

@@ Línea 7: / Línea 7: @@
 text {* Los ejercicios de esta relación deben de resolverse usando sólo
-   las reglas básicas de la deducción natural proposicional:
+   las reglas básicas de la deducción natural proposicional y de primer orden:
    · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
    · conjunct1:  P ∧ Q ⟹ P
@@ Línea 26: / Línea 26: @@
    · iffD2:      ⟦P = Q; Q⟧ ⟹ P
    · ccontr:     (¬P ⟹ False) ⟹ P
    · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
    · allE:       (⋀x. P x) ⟹ ∀x. P x

Rel 10 - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Protegió «Rel 10» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 05:13 15 mar 2011

Jalonso en 05:13 15 mar 2011

Jalonso: Página creada con ' theory Relacion_10 imports Main begin section {* Deducción natural de primer orden *} text {* Los ejercicios de esta relación deben de resolverse usan...'

Jalonso: Página creada con ' theory Relacion_10 imports Main begin section {* Deducción natural de primer orden } text { Los ejercicios de esta relación deben de resolverse usan...'