Lógica matemática y fundamentos (2017-18) - Contribuciones del usuario [es]

Relación 11

2018-05-14T09:06:17Z

Mjoseh: Página creada con '=== Relación 11: Resolución en Lógica de primer orden === ---- '''Ejercicio 1.''' Se consideran las siguientes fórmulas: reflexiva: ∀x R(x,x) simétrica: ∀x ∀y (...'

=== Relación 11: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)

simétrica: ∀x ∀y (R(x,y) → R(y,x))

transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))

notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:

∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))

∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))

∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas

S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}.

En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

R11

2018-05-14T09:06:05Z

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

R11

2018-05-14T09:05:31Z

Mjoseh:

R11

2018-05-14T09:04:58Z

Mjoseh:

=== Relación 11: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)

simétrica: ∀x ∀y (R(x,y) → R(y,x))

transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))

notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:

∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))

∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))

∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}. En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

R11

2018-05-14T09:04:32Z

Mjoseh:

=== Relación 11: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)

simétrica: ∀x ∀y (R(x,y) → R(y,x))

transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))

notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}. En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

R11

2018-05-14T09:04:11Z

Mjoseh:

=== Relación 11: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}. En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

R11

2018-05-14T09:03:55Z

Mjoseh:

=== Relación 11: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:
reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}. En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

R11

2018-05-14T09:03:09Z

=== Relación 11: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:
reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}. En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

Lógica matemática y fundamentos (2017-18)

2018-05-14T09:02:50Z

Mjoseh:

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos. ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Resolución proposicional. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución en lógica de primer orden. ([[R11 |Enunciado]] y [[Relación 11 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].

Relación 10

2018-05-07T14:18:00Z

Mjoseh: Página creada con ' === Relación 10: Cuestiones === ---- '''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación: Sea T un tablero de S₁, I un modelo de una hoja abierta de T y S₂ ...'

=== Relación 10: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

Sea T un tablero de S₁, I un modelo de una hoja abierta de T y S₂ ⊆ S₁. Entonces,
I ⊧ S₂.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguientes afirmaciones:

* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, D ⊂ C₁ y D ≠ C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂ y D = C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, C₁ ⊂ D y C₂ no es una tautología

----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes proposiciones:
* Para todo conjunto de fórmula S y para toda fórmula F se verifica que si S ̸⊧ F, entonces S ⊧ ¬ F.
* Para toda fórmula F se tiene que si G es una forma de Skolem de F entonces ⊧ F ↔ G.

----

'''Solución:'''

----
'''Ejercicio 4.''' Hallar las formas prenexa, de Skolem y clausal de la fórmula: ¬∃ x ∀ z [ P ( x ) → ¬ Q ( z )] ∨ ∃ z (A ( y, z) → ∃ u B ( y, u ))

----

'''Solución:'''

----
'''Ejercicio 5.''' Demostrar o refutar las siguientes sentencias:

* Existe un conjunto finito de cláusulas S que es inconsistente y tiene un conjunto infinito de resolventes; es decir, existe una sucesión infinita de cláusulas C₁ , C₂ , ... tal que para todo i se tiene que Cᵢ ∈ S o existen j, k < i tales que Cᵢ es una resolvente de Cⱼ y Cₖ.

* Todo conjunto inconsistente de cláusula tiene una refutación por resolución positiva.

----

'''Solución:'''

R10

2018-05-07T14:17:21Z

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

R10

2018-05-07T14:16:59Z

Mjoseh:

R10

2018-05-07T14:16:33Z

=== Relación 10: Cuestiones ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

Sea T un tablero de S₁, I un modelo de una hoja abierta de T y S₂ ⊆ S₁. Entonces,
I ⊧ S₂.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguientes afirmaciones:

* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, D ⊂ C₁ y D ≠ C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂ y D = C₁.
* Existen cláusulas C₁, C₂ y D tales que D es una resolvente de C₁ y C₂, C₁ ⊂ D y C₂ no
es una tautología

----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar o refutar las siguientes proposiciones:
* Para todo conjunto de fórmula S y para toda fórmula F se verifica que si S ̸⊧ F, entonces S ⊧ ¬ F.
* Para toda fórmula F se tiene que si G es una forma de Skolem de F entonces ⊧ F ↔ G.

----

'''Solución:'''

----
'''Ejercicio 4.''' Hallar las formas prenexa, de Skolem y clausal de la fórmula: ¬∃ x ∀ z [ P ( x ) → ¬ Q ( z )] ∨ ∃ z (A ( y, z) → ∃ u B ( y, u ))

----

'''Solución:'''

----
'''Ejercicio 5.''' Demostrar o refutar las siguientes sentencias:

* Existe un conjunto finito de cláusulas S que es inconsistente y tiene un conjunto infinito de resolventes; es decir, existe una sucesión infinita de cláusulas C₁ , C₂ , ... tal que para todo i se tiene que Cᵢ ∈ S o existen j, k < i tales que Cᵢ es una resolvente de Cⱼ y Cₖ.

* Todo conjunto inconsistente de cláusula tiene una refutación por resolución positiva.

----

'''Solución:'''

Lógica matemática y fundamentos (2017-18)

2018-05-07T14:16:08Z

Mjoseh:

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos. ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Resolución proposicional. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].

Relación 9

2018-04-27T11:00:15Z

Mjoseh: Página creada con '=== Relación 9: Resolución proposicional === ---- '''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide: * Probar que A ...'

=== Relación 9: Resolución proposicional ===

----
'''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide:
* Probar que A ⊧ B, mediante resolución proposicional.
* Describir, razonadamente, todos los modelos de A y, a continuación, probar nuevamente que A ⊧ B, utilizando la definición de consecuencia lógica.
* ¿Es ¬B → ¬A una tautología?

----

'''Solución:'''

----
'''Ejercicio 2.''' Consideremos la fórmula proposicional A : (r → p) ∧ (¬r → q ∨ s) → p ∨ q ∨ s
y el conjunto de fórmulas U = {r ⇔ p ∨ q, s → p, ¬s ∧ ¬r → s ∨ t}.
* Probar, mediante tableros semánticos, que A es una tautología.
* Probar, razonadamente, que U es consistente, mostrando para ello un modelo de U.
* Probar, mediante resolución, que U ⊧ ¬p → (q ∨ t).
* Sea B la fórmula (¬p → (q ∨ t)). ¿Podemos eliminar alguna fórmula de U de
manera que la fórmula B sea consecuencia lógica del conjunto de fórmulas restante?

----

'''Solución:'''

----
'''Ejercicio 3.'''

Decidir, mediante resolución, si r es consecuencia lógica de

{p ⇔ q, ¬p → r, ¬ s ∧ ¬ t → q, ¬ s ∧ t}

En el caso que no lo sea, construir un contramodelo a partir de la resolución.

----

'''Solución:'''

R9

2018-04-27T11:00:02Z

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

R9

2018-04-27T10:59:43Z

Mjoseh:

R9

2018-04-27T10:59:16Z

Mjoseh:

R9

2018-04-27T10:58:53Z

Mjoseh: Página creada con ' === Relación 9: Resolución proposicional === ---- '''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide: * Probar que A ...'

=== Relación 9: Resolución proposicional ===

----
'''Ejercicio 1.''' Dadas las fórmulas A : (s → p) ∨ (t → q) y B : (s → q) ∨ (t → p), se pide:
* Probar que A ⊧ B, mediante resolución proposicional.
* Describir, razonadamente, todos los modelos de A y, a continuación, probar nuevamente
que A ⊧ B, utilizando la definición de consecuencia lógica.
* ¿Es ¬B → ¬A una tautología?

----

'''Solución:'''

----
'''Ejercicio 2.''' Consideremos la fórmula proposicional A : (r → p) ∧ (¬r → q ∨ s) → p ∨ q ∨ s
y el conjunto de fórmulas U = {r ⇔ p ∨ q, s → p, ¬s ∧ ¬r → s ∨ t}.
* Probar, mediante tableros semánticos, que A es una tautología.
* Probar, razonadamente, que U es consistente, mostrando para ello un modelo de U.
* Probar, mediante resolución, que U ⊧ ¬p → (q ∨ t).
* Sea B la fórmula (¬p → (q ∨ t)). ¿Podemos eliminar alguna fórmula de U de
manera que la fórmula B sea consecuencia lógica del conjunto de fórmulas restante?

----

'''Solución:'''

----
'''Ejercicio 3.'''

Decidir, mediante resolución, si r es consecuencia lógica de

{p ⇔ q, ¬p → r, ¬ s ∧ ¬ t → q, ¬ s ∧ t}

En el caso que no lo sea, construir un contramodelo a partir de la resolución.

----

'''Solución:'''

Lógica matemática y fundamentos (2017-18)

2018-04-27T10:58:37Z

Mjoseh:

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos. ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Resolución proposicional. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].

Relación 8

2018-04-11T08:24:51Z

Mjoseh: Página creada con ' === Relación 8: Tableros semánticos === ---- '''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación: Sea T un tablero de S₁, I un modelo de una hoja abierta de ...'

=== Relación 8: Tableros semánticos ===

----
'''Ejercicio 1.''' Demostrar o refutar la siguiente afirmación:

Sea T un tablero de S₁, I un modelo de una hoja abierta de T y S₂ ⊆ S₁. Entonces,
I ⊧ S2.
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar o refutar la siguiente afirmación:

Si S es un conjunto inconsistente de fórmulas, entonces el tablero semántico cerrado de
S obtenido aplicando las reglas α antes que las reglas β tiene menos nodos que el tablero
semántico cerrado de S obtenido aplicando las reglas β antes que las reglas α.

----

'''Solución:'''

----
'''Ejercicio 3.''' Decidir por tableros semánticos, si:

∀x (P(x) → Q(x)) ⊧ (∃x P(x)) → (∃ x Q(x))

----

'''Solución:'''

----
'''Ejercicio 4.''' Decidir por tableros semánticos, si:

⊧ ∀x (P(x) → R(x,x)) → ∀x ∃ y (R(x,y) ∨ ¬ P(y))

----

'''Solución:'''

----
'''Ejercicio 5.''' Decidir por tableros semánticos, si:

∀x ∃ y (R(x,y) ∨ ¬ P(y)) ⊧ ∀x (P(x) → R(x,x))

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por tableros semánticos, si:

∀x ∀ y (R(x,y) → R(y,x)) ⊧ ∀x ∀y ∀z (R(x,y) ∧ R(x,z) → ∃u (R(y,u) ∧ R(z,u)))

----

'''Solución:'''

----
'''Ejercicio 7.''' Decidir por tableros semánticos, si:

* ⊧ (∃x P(x)) → P(a)
* {∀x(P(x) → Q(x)), ∀y(Q(a) ∨ R(y) → S(a))} ⊧ ∀x (P(x) → S(a))

----

'''Solución:'''

R8

2018-04-11T08:24:18Z

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

R8

2018-04-11T08:23:49Z

Lógica matemática y fundamentos (2017-18)

2018-04-11T08:23:33Z

Mjoseh:

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos. ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].

Relación 7

2018-04-05T10:20:05Z

Mjoseh: Página creada con '<source lang = "isar"> chapter {* R7: Deducción natural en lógica de primer orden *} theory R7 imports Main begin text {* Demostrar o refutar los siguientes lemas usando ...'

<source lang = "isar">
chapter {* R7: Deducción natural en lógica de primer orden *}

theory R7
imports Main
begin

text {*
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· 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
· excluded_middel:(¬P ∨ P)

· 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

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}

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

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

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
∃x. ¬(P x) ⊢ ¬(∀x. P x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
∀x. P x ⊢ ∀y. P y
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
∀x. P x ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
∀x y. P x y ⊢ ∀u v. P u v
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
∃x y. P x y ⟹ ∃u v. P u v
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}

lemma ejercicio_10a:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
(∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
(∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
¬(∀x. ¬(P x)) ⊢ ∃x. P x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
∀x. ¬(P x) ⊢ ¬(∃x. P x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
∃x. P x ⊢ ¬(∀x. ¬(P x))
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}

lemma ejercicio_20a:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
------------------------------------------------------------------ *}

lemma ejercicio_24a:
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
oops

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------ *}

lemma ejercicio_25a:
"(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_26a:
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar o refutar
((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_27a:
"((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar o refutar
((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_28a:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}

lemma ejercicio_29:

"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar o refutar
(¬(∀x. P x)) ⟷ (∃x. ¬P x)
------------------------------------------------------------------ *}

lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
oops

section {* Ejercicios sobre igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ *}

lemma ejercicio_31a:
assumes "P a"
shows "∀x. x = a ⟶ P x"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ *}

lemma ejercicio_32a:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)}
⊢ P (f a) a (f a)
------------------------------------------------------------------ *}

lemma ejercicio_33a:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "P (f a) a (f a)"
oops

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ *}

lemma ejercicio_34a:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
oops

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ *}

lemma ejercicio_35a:
assumes "∀y. Q a y"
"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
oops

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar o refutar
{x = f x, odd (f x)} ⊢ odd x
------------------------------------------------------------------ *}

lemma ejercicio_36a:
assumes "x = f x" and
"odd (f x)"
shows "odd x"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar o refutar
{x = f x, triple (f x) (f x) x} ⊢ triple x x x
------------------------------------------------------------------ *}

lemma ejercicio_37a:
assumes "x = f x" and
"triple (f x) (f x) x"
shows "triple x x x"
oops

end

</source>

R7

2018-04-05T10:19:41Z

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

R7

2018-04-05T10:19:32Z

Lógica matemática y fundamentos (2017-18)

2018-04-05T10:18:51Z

Mjoseh:

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].

Relación 6

2018-04-02T17:25:41Z

Mjoseh: Página creada con '=== Relación 6: Sintaxis y semántica de la Lógica de primer orden (b) === ---- '''Ejercicio 1.''' Dar una fórmula F satisfacible, tal que todos sus modelos sean necesariam...'

=== Relación 6: Sintaxis y semántica de la Lógica de primer orden (b) ===

----
'''Ejercicio 1.''' Dar una fórmula F satisfacible, tal que todos sus modelos sean necesariamante infinitos.

----

'''Solución:'''

----
'''Ejercicio 2.''' ¿Cuántos elementos han de tener los modelos de la fórmula F = ∀x f(f(x))= x ∧ ∀x f(x) ≠ x?
----

'''Solución:'''

----
'''Ejercicio 3.'''

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----

'''Solución:'''

----
'''Ejercicio 4.'''

Sea L un lenguaje de primer orden con un símbolo de predicado, Q (de aridad 2) y un símbolo de función, f (de aridad 1). Se considera la estructura I dada por: Universo: {a,b}, Qᴵ={(a,b), (b,a)}, fᴵ(a)= a y fᴵ(b)=a. Decidir cuáles de las siguientes fórmulas se satisfacen en la estructura:
* ∀x (Q(f(x),x) → Q(x,x))
* ∃x (Q(f(x),x) → Q(x,x))

----

'''Solución:'''

----
'''Ejercicio 5.'''

Sea L un lenguaje de primer orden con un símbolo de predicado P de aridad 2. Probar que las fórmulas ∀x ∃y P(x,y) y ∃x ∀y P(x,y) no son equivalentes,
dando una estructura que sea modelo de la primera pero no de la segunda.

----

'''Solución:'''

R6

2018-04-02T17:25:31Z

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

R6

2018-04-02T17:25:07Z

Mjoseh:

R6

2018-04-02T17:24:20Z

=== Relación 6: Sintaxis y semántica de la Lógica de primer orden (b) ===

----
'''Ejercicio 1.''' Dar una fórmula F satisfacible, tal que todos sus modelos sean necesariamante infinitos.

----

'''Solución:'''

----
'''Ejercicio 2.''' ¿Cuántos elementos han de tener los modelos de la fórmula F = ∀x f(f(x))= x ∧ ∀x f(x) ≠ x?
----

'''Solución:'''

----
'''Ejercicio 3.'''

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----

'''Solución:'''

----
'''Ejercicio 4.'''

Sea L un lenguaje de primer orden con un símbolo de predicado, Q (de aridad 2)
y un símbolo de función, f (de aridad 1). Se considera la estructura I dada
por: Universo: {a,b}, Qᴵ={(a,b), (b,a)}, fᴵ(a)= a y fᴵ(b)=a. Decidir cuáles
de las siguientes fórmulas se satisfacen en la estructura:
* ∀x (Q(f(x),x) → Q(x,x))
* ∃x (Q(f(x),x) → Q(x,x))

----

'''Solución:'''

----
'''Ejercicio 5.'''

Sea L un lenguaje de primer orden con un símbolo de predicado P de aridad
2. Probar que las fórmulas ∀x ∃y P(x,y) y ∃x ∀y P(x,y) no son equivalentes,
dando una estructura que sea modelo de la primera pero no de la segunda.

----

'''Solución:'''

Lógica matemática y fundamentos (2017-18)

2018-04-02T17:24:01Z

Mjoseh: /* Relaciones de ejercicios */

Relación 5

2018-03-22T17:46:07Z

Mjoseh: /* Relación 5: Sintaxis y semántica de la Lógica de primer orden */

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de
APPLI2), verificando la corrección de la solución:

* Todo aquel que entre en el país y no sea un VIP será cacheado por un aduanero.
* Hay un contrabandista que entra en el país y que solo podrá ser cacheado por contrabandistas.
* Ningún contrabandista es un VIP.
* Por lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de
APPLI2), verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de
APPLI2), verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de APPLI2), verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos.
* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. Dar un
ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una
interpretación en la que F sea falsa.

----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad
1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I )
la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P ( x ) → ∃ yQ ( y, x ) .
*. ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

Relación 5

2018-03-22T17:45:40Z

Mjoseh: /* Relación 5: Sintaxis y semántica de la Lógica de primer orden */

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de
APPLI2), verificando la corrección de la solución:

* Todo aquel que entre en el país y no sea un VIP será cacheado por un aduanero.
* Hay un contrabandista que entra en el país y que solo podrá ser cacheado por contrabandistas.
* Ningún contrabandista es un VIP.
* Por lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de
APPLI2), verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de
APPLI2), verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de
APPLI2), verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí
mismo y sólo a ellos.

* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. Dar un
ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una
interpretación en la que F sea falsa.

----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad
1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I )
la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P ( x ) → ∃ yQ ( y, x ) .
*. ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

Relación 5

2018-03-19T16:03:10Z

Mjoseh: Página creada con '=== Relación 5: Sintaxis y semántica de la Lógica de primer orden === ---- '''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de APPLI2), verificando ...'

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de
APPLI2), verificando la corrección de la solución:

* Todo aquel que entre en el país y no sea un VIP será cacheado por un aduanero.
* Hay un contrabandista que entra en el país y que solo podrá ser cacheado por contrabandistas.
* Ningún contrabandista es un VIP.
* Por lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de
APPLI2), verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de
APPLI2), verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y
entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.

* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de
APPLI2), verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí
mismo y sólo a ellos.

* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. Dar un
ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una
interpretación en la que F sea falsa.

----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad
1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I )
la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P ( x ) → ∃ yQ ( y, x ) .
*. ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

R5

2018-03-19T16:02:57Z

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

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de
APPLI2), verificando la corrección de la solución:

* Todo aquel que entre en el país y no sea un VIP será cacheado por un aduanero.
* Hay un contrabandista que entra en el país y que solo podrá ser cacheado por contrabandistas.
* Ningún contrabandista es un VIP.
* Por lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de
APPLI2), verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de
APPLI2), verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y
entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.

* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de
APPLI2), verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí
mismo y sólo a ellos.

* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. Dar un
ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una
interpretación en la que F sea falsa.

----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad
1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I )
la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P ( x ) → ∃ yQ ( y, x ) .
*. ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

R5

2018-03-19T16:02:48Z

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de
APPLI2), verificando la corrección de la solución:

* Todo aquel que entre en el país y no sea un VIP será cacheado por un aduanero.
* Hay un contrabandista que entra en el país y que solo podrá ser cacheado por contrabandistas.
* Ningún contrabandista es un VIP.
* Por lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de
APPLI2), verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de
APPLI2), verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y
entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.

* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de
APPLI2), verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí
mismo y sólo a ellos.

* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. Dar un
ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una
interpretación en la que F sea falsa.

----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad
1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I )
la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P ( x ) → ∃ yQ ( y, x ) .
*. ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

Lógica matemática y fundamentos (2017-18)

2018-03-19T16:01:16Z

Mjoseh: /* Relaciones de ejercicios */

Relación 4

2018-03-15T17:27:22Z

Mjoseh:

<source lang = "isar">

chapter {* R4: Deducción natural proposicional *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· 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
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación. *}

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

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

section {* Implicaciones *}

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_1: josrodjim2 carmarria inmbenber
assumes 1: "p ⟶ q" and
2: "p"
shows "q"

proof -
show 1: "q" using 1 2 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_2: josrodjim2 carmarria inmbenber
assumes 1: "p ⟶ q" and
2: "q ⟶ r" and
3: "p"
shows "r"

proof-
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_3: josrodjim2 carmarria inmbenber
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"

proof-
have 4: "q" using 2 3 by (rule mp)
have 5: "(q ⟶ r)" using 1 3 by (rule mp)
show "r" using 5 4 by (rule mp)

qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_4: josrodjim2
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"

proof-
{ assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)}
hence 6: "p ⟶ r" using 3 5 by (rule impI)
show "p⟶r" using 6 by this

oops

lemma ejercicio_4: carmarria
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof -
{ assume 3: p
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)
}
thus "p ⟶ r" by (rule impI)
qed
lemma ejercicio_4: inmbenber
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof -
{ assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp) }
thus "p ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_5: josrodjim2 (NO DA ERROR, PERO SI ALERTA)
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"

proof -

{ assume 2: "q"
{assume 3: "p"
have 4: "q ⟶r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp)}
hence 6: "p⟶r" using 3 5 by (rule impI)}
hence 7: "q ⟶ (p ⟶ r)" using 2 6 by (rule impI)
show "q ⟶ (p ⟶ r)" using 7 by this

oops

lemma ejercicio_5: carmarria
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"

proof -
{assume 2: q
{assume 3: p
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp)
}
hence " p ⟶ r" by (rule impI)
}
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed

lemma ejercicio_5: inmbenber
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"

proof -
{assume 2: "q"
{assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp) }
hence " p ⟶ r" by (rule impI) }
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_6:josrodjim2
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"

proof-

{assume 2: "p⟶q"
{assume 3: "p"
have 4: "q⟶r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
have 6: "r" using 4 5 by (rule mp)}
hence 7: "p⟶r" using 3 6 by (rule impI)}
hence 8: "(p ⟶ q) ⟶ (p ⟶ r)" using 2 7 by (rule impI)
show "(p ⟶ q) ⟶ (p ⟶ r)" using 8 by this
oops

lemma ejercicio_6: carmarria, inmbenber
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
{assume 2: "p ⟶ q"
{assume 3: "p"
have 4: "q" using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 3 by (rule mp)
have 6: "r" using 5 4 by (rule mp)
}
hence 7: "p ⟶ r" by (rule impI)
}
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7: (NO SE QUE ESTA MAL)
assumes "p"
shows "q ⟶ p"

proof -

{ assume 2: "q"
have 3: "p" using 1
}
hence 4: "q⟶p" using 2 3 by (rule impI)

show "q⟶p" using 4 by this

oops

lemma ejercicio_7: carmarria, inmbenber
assumes 1: "p"
shows "q ⟶ p"
proof -
{assume 2: "q"
have 3: "p" using 1 by this}
thus "q ⟶ p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8: carmarria
"p ⟶ (q ⟶ p)"

proof -
{assume 1: p
{assume 2: q
have 3: p using 1 by this
}
hence 4: "q ⟶ p" by (rule impI)
}
thus "p ⟶ (q ⟶ p)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9: carmarria
assumes 1: "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof -
{assume 2: "q ⟶ r"
{assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)
}
hence 6: "p ⟶ r" by (rule impI)
}
thus 7: "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

lemma ejercicio_10: carmarria
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"

proof-
{assume 2: r
{assume 3: q
{assume 4: p
have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
have 6: "r ⟶ s" using 5 3 by (rule mp)
have 7: s using 6 2 by (rule mp)
}
hence 8: "p ⟶ s" by (rule impI)
}
hence 9: "q ⟶ (p ⟶ s)" by (rule impI)
}
thus "r ⟶ (q ⟶ (p ⟶ s))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11: carmarria
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
{assume 1: "p ⟶ (q ⟶ r)"
{assume 2: "p ⟶ q"
{assume 3: p
have 4: q using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 3 by (rule mp)
have 6: r using 5 4 by (rule mp)
}
hence 7: "p ⟶ r" by (rule impI)
}
hence 8: "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
}
thus "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12: carmarria
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
{assume 2: p
{assume 3: q
{assume 4: p
have 5: q using 3 by this
}
hence 6: "p ⟶ q" by (rule impI)
have 7: r using 1 6 by (rule mp)
}
hence 8: "q ⟶ r" by (rule impI)
}
thus "p ⟶ (q ⟶ r)" by (rule impI)
qed

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof (rule conjI)
have "p ∧ q" using assms ..
thus "p" ..
next
show "q ∧ r"
proof (rule conjI)
have "p ∧ q" using assms ..
thus "q" ..
next
show "r" using assms ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
oops

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_52:
"p ∨ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops

end

</source>

Relación 4

2018-03-06T13:45:46Z

Mjoseh: Página creada con '<source lang = "isar"> chapter {* R4: Deducción natural proposicional *} theory R4 imports Main begin text {* ------------------------------------------------------------...'

<source lang = "isar">

chapter {* R4: Deducción natural proposicional *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· 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
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación. *}

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

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

section {* Implicaciones *}

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "p ⟶ q"
"p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
oops

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
oops

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_52:
"p ∨ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops

end

</source>

R4

2018-03-06T13:45:23Z

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

<source lang = "isar">

chapter {* R4: Deducción natural proposicional *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· 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
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación. *}

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

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

section {* Implicaciones *}

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "p ⟶ q"
"p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
oops

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
oops

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_52:
"p ∨ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops

end

</source>

R4

2018-03-06T13:45:15Z

<source lang = "isar">

chapter {* R4: Deducción natural proposicional *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· 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
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación. *}

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

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

section {* Implicaciones *}

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "p ⟶ q"
"p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
oops

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
oops

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
oops

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_52:
"p ∨ ¬p"
oops

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
oops

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
oops

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops

end

</source>

Lógica matemática y fundamentos (2017-18)

2018-03-06T13:44:02Z

Mjoseh:

Lógica matemática y fundamentos (2017-18)

2018-03-06T13:41:19Z

Mjoseh:

Relación 3

2018-02-28T11:33:47Z

Mjoseh: Página creada con ' === Relación 3: Deducción natural en lógica proposicional === ---- '''Ejercicio 1.''' Demostrar mediante deducción natural: : ( p ∨ q ) ∧ ( p ∨ r ) ⊧ p ∨ ( q ∧...'

=== Relación 3: Deducción natural en lógica proposicional ===

----
'''Ejercicio 1.''' Demostrar mediante deducción natural:
: ( p ∨ q ) ∧ ( p ∨ r ) ⊧ p ∨ ( q ∧ r )
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar mediante deducción natural:
: p ∨ q ⊧ ¬(¬ p ∧ ¬ q )
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar mediante deducción natural:
: ¬ p ∨ ¬ q ⊧ ¬( p ∧ q )
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar mediante deducción natural:
: {p → r, r → ¬ q} ⊧ ¬(p ∧ q)
----

'''Solución:'''

----
'''Ejercicio 5.''' Demostrar mediante deducción natural:
: (p → r) ∨ (q → s) ⊧ (p ∧ q) → (r ∨ s)
----

'''Solución:'''

----
'''Ejercicio 6.''' Demostrar mediante deducción natural:
: p → (q ∧ r) ⊧ (p → q) ∨ (p → r)
----

'''Solución:'''

R3

2018-02-28T11:33:35Z

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

R3

2018-02-28T11:33:25Z

Lógica matemática y fundamentos (2017-18)

2018-02-28T11:33:05Z

Mjoseh:

Relación 2

2018-02-26T08:35:04Z

Mjoseh:

=== Relación 2: Deducción natural en lógica proposicional ===

----
'''Ejercicio 0.''' Demostrar mediante deducción natural:
: {p → q, p → r} ⊧ p → r
----

'''Solución:'''

[[Archivo:R2E0a.png]]

----
'''Ejercicio 1.''' Demostrar mediante deducción natural:
: (p → q) → r ⊧ p → (q → r)
----

'''Solución:''' josrodjim2 marloppal3

[[https://i.gyazo.com/f6ad7b1deab0dd5ba927bcf0b0d73c6f.png]]

----
'''Ejercicio 2.''' Demostrar mediante deducción natural:
: (p → q) ∧ (p → r) ⊧ p → q ∧ r
----

'''Solución:''' josrodjim2 marloppal3

[[https://i.gyazo.com/cb016e19514071b5c9240f992f970f2d.png]]

----
'''Ejercicio 3.''' Demostrar mediante deducción natural:
: (p → r) ∧ (q → r) ⊧ p ∨ q → r
----

'''Solución:''' josrodjim2

[[https://i.gyazo.com/d47ef41c989cccab33908c6debdf57dc.png]]

----
'''Ejercicio 4.''' Demostrar mediante deducción natural:
: {p → r, r → ¬ q} ⊧ ¬(p ∧ q)
----

'''Solución:''' josrodjim2 marloppal3

[[https://i.gyazo.com/3c2c9799cfa2c74230d50cb0c1542281.png]]

----
'''Ejercicio 5.''' Demostrar mediante deducción natural:
: ¬p ∧ ¬q ⊧ ¬(p ∨ q)
----

'''Solución:''' josrodjim2 marloppal3

[[https://i.gyazo.com/700aa57e081894401d184f5797fb070d.png]]

----
'''Ejercicio 6.''' Demostrar mediante deducción natural:
: ⊧ ((p → q) → p)
----

'''Solución:'''

----
'''Ejercicio 7.''' Demostrar mediante deducción natural:
: (p → q) ∨ (q → p)
----

'''Solución:''' josrodjim2

[[https://i.gyazo.com/ba9485c972e0d26a49c0502ce8d307c0.png]]

----
'''Ejercicio 8.''' Demostrar mediante deducción natural:
: ¬(¬p ∧ ¬q) ⊧ p ∨ q
----

'''Solución:'''