https://www.glc.us.es/~jalonso/LMF2015/index.php?action=history&feed=atom&title=Ejercicio_5_%28b%29
Ejercicio 5 (b) - Historial de revisiones
2026-07-20T15:59:29Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/LMF2015/index.php?title=Ejercicio_5_(b)&diff=344&oldid=prev
WikiSysop: Texto reemplazado: «isar» por «isabelle»
2018-07-16T12:27:08Z
<p>Texto reemplazado: «isar» por «isabelle»</p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 12:27 16 jul 2018</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td>
<td colspan="2" class="diff-lineno">Línea 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><source lang="<del class="diffchange diffchange-inline">isar</del>"></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><source lang="<ins class="diffchange diffchange-inline">isabelle</ins>"></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
</table>
WikiSysop
https://www.glc.us.es/~jalonso/LMF2015/index.php?title=Ejercicio_5_(b)&diff=340&oldid=prev
Jalonso en 17:54 3 jun 2015
2015-06-03T17:54:10Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="es">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 17:54 3 jun 2015</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td>
<td colspan="2" class="diff-lineno">Línea 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><source lang="isar></div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><source lang="isar<ins class="diffchange diffchange-inline">"</ins>></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
</table>
Jalonso
https://www.glc.us.es/~jalonso/LMF2015/index.php?title=Ejercicio_5_(b)&diff=339&oldid=prev
Jalonso: Página creada con '<source lang="isar> header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *} theory e5_2_sol imports Main begin text {* Apellidos: Nombre: *} text...'
2015-06-03T17:53:49Z
<p>Página creada con '<source lang="isar> header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *} theory e5_2_sol imports Main begin text {* Apellidos: Nombre: *} text...'</p>
<p><b>Página nueva</b></p><div><source lang="isar><br />
header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}<br />
<br />
theory e5_2_sol<br />
imports Main <br />
begin<br />
<br />
text {*<br />
Apellidos:<br />
Nombre: <br />
*} <br />
<br />
text {* Sustituye la palabra uvus por tu usuario de la Universidad de<br />
Sevilla y graba el fichero con dicho usuario .thy<br />
*} <br />
<br />
text {*<br />
Demostrar o refutar los siguientes lemas usando sólo las reglas<br />
básicas de deducción natural de la lógica proposicional, de los<br />
cuantificadores y de la igualdad: <br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
. excluded_middle:(¬P ∨ P) <br />
<br />
· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R<br />
· allI: (⋀x. P x) ⟹ ∀x. P x<br />
· exI: P x ⟹ ∃x. P x<br />
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q<br />
<br />
· refl: t = t<br />
· subst: ⟦s = t; P s⟧ ⟹ P t<br />
· trans: ⟦r = s; s = t⟧ ⟹ r = t<br />
· sym: s = t ⟹ t = s<br />
· not_sym: t ≠ s ⟹ s ≠ t<br />
· ssubst: ⟦t = s; P s⟧ ⟹ P t<br />
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d<br />
· arg_cong: x = y ⟹ f x = f y<br />
· fun_cong: f = g ⟹ f x = g x<br />
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y<br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación.<br />
*}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
lemma Ejercicio5: <br />
shows "(∀x. P(x) ⟶ R(x,x)) ⟶ (∀x. ∃y. R(x,y) ∨ ¬P(y))"<br />
proof (rule impI)<br />
assume "∀x. P(x) ⟶ R(x,x)"<br />
show "∀x. ∃y. R(x,y) ∨ ¬P(y)"<br />
proof (rule allI)<br />
fix a<br />
have "¬P(a) ∨ P(a)" ..<br />
then show "∃y. R(a,y) ∨ ¬P(y)"<br />
proof (rule disjE)<br />
assume "¬P(a)"<br />
then have "R(a,a) ∨ ¬P(a)" by (rule disjI2)<br />
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)<br />
next<br />
assume "P(a)" <br />
have "P(a) ⟶ R(a,a)" using `∀x. P(x) ⟶ R(x,x)` by (rule allE)<br />
then have "R(a,a)" using `P(a)` by (rule mp)<br />
then have "R(a,a) ∨ ¬P(a)" by (rule disjI1)<br />
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)<br />
qed <br />
qed<br />
qed<br />
<br />
end<br />
</source></div>
Jalonso