chapter {* R7: Deducción natural de primer orden *}
theory R7_Deduccion_natural_de_primer_orden
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
· 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, mt y not_ex que demostramos a
continuación. *}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 2. 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)
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 5. 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))
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 6. 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))
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 7. (En APLI2 el ejercicio 13 de LP) Formalizar, y demostrar
la corrección, del siguiente argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
Or : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
la corrección, del siguiente argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) Formalizar, y decidir
la corrección, del siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) Formalizar, y decidir
la corrección, del siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}
end
