header {* Relación 4: Argumentación proposicional *}
theory R4
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación formalizar y demostrar la corrección de
los argumentos 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
text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Cuando tanto la temperatura como la presión atmosférica permanecen
contantes, no llueve. La temperatura permanece constante. Por lo
tanto, en caso de que llueva, la presión atmosférica no permanece
constante.
Usar T para "La temperatura permanece constante",
P para "La presión atmosférica permanece constante" y
L para "Llueve".
------------------------------------------------------------------ *}
lemma ejercicio_1:
assumes "T ∧ P ⟶ ¬L" and
"T"
shows "L ⟶ ¬P"
proof
assume "L"
show "¬P"
proof
assume "P"
have "T ∧ P" using `T` `P` ..
have "¬L" using assms(1) `T ∧ P` ..
thus "False" using `L` ..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
argumento
Siempre que un número x es divisible por 10, acaba en 0. El número
x no acaba en 0. Por lo tanto, x no es divisible por 10.
Usar D para "el número es divisible por 10" y
C para "el número acaba en cero".
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 3. 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 4. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no está el mañana ni el ayer escrito, entonces no está el mañana
escrito.
Usar M: El mañana está escrito.
A: El ayer está escrito.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
argumento
Me matan si no trabajo y si trabajo me matan. Me matan siempre me
matan.
Usar M: Me matan.
T: Trabajo.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
argumento
Si te llamé por teléfono, entonces recibiste mi llamada y no es
cierto que no te avisé del peligro que corrías. Por consiguiente,
como te llamé, es cierto que te avisé del peligro que corrías.
Usar T: Te llamé por teléfono.
R: Recibiste mi llamada.
P: Te avisé del peligro que corrías.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no hay control de nacimientos, entonces la población crece
ilimitadamente; pero si la población crece ilimitadamente,
aumentará el índice de pobreza. Por consiguiente, si no hay control
de nacimientos, aumentará el índice de pobreza.
Usar N: Hay control de nacimientos.
P: La población crece ilimitadamente,
I: Aumentará el índice de pobreza.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
argumento
Si el general era leal, hubiera obedecido las órdenes, y si era
inteligente las hubiera comprendido. O el general desobedeció las
órdenes o no las comprendió. Luego, el general era desleal o no era
inteligente.
Usar L: El general es leal.
O: El general obedece las órdenes.
I: El general es inteligente.
C: El general comprende las órdenes.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
argumento
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
haría. Si Dios fuera incapaz de evitar el mal, no sería
omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
evita el mal. Si Dios existe, es omnipotente y no es
malévolo. Luego, Dios no existe.
Usar C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
O: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente
argumento
Nadie más que Pedro, Quintín y Raúl están bajo sospecha y al menos
uno es traidor. Pedro nunca trabaja sin llevar al menos un cómplice
(que puede ser Quintín o Raúl). Raúl es leal. Por lo tanto,
Pedro es traidor.
Usar p: Pedro es traidor.
q : Quintín es traidor.
r : Raúl es traidor.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 11. 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.
O : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}
text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente
argumento
Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
embargo, si trabajo no gozo de la vida, mientras que si no trabajo
no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
dinero.
Usar p: Trabajo
q: Gano dinero.
r: Gozo de la vida.
------------------------------------------------------------------ *}
end
