theory Relacion_9
imports Main
begin
section {* Deducción natural proposicional *}
text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed
lemma ejercicio_1b:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed
lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed
lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed
lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed
lemma ejercicio_5:
assumes 1: "p⟶(q⟶r)"
shows "q⟶(p⟶r)"
oops
lemma ejercicio_6:
assumes 1: "p⟶(q⟶r)"
shows "(p⟶q)⟶(p⟶r)"
oops
lemma ejercicio_7:
assumes 1: "p"
shows "q⟶p"
oops
lemma ejercicio_8:
"p⟶(q⟶p)"
oops
lemma ejercicio_9:
assumes 1: "p⟶q"
shows "(q⟶r)⟶(p⟶r)"
oops
lemma ejercicio_10:
assumes 1: "p⟶(q⟶(r⟶s))"
shows "r⟶(q⟶(p⟶s))"
oops
lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops
lemma ejercicio_12:
assumes 1: "(p⟶q)⟶r"
shows "p⟶(q⟶r)"
oops
lemma ejercicio_13:
assumes 1: "p" and
2: "q"
shows "p∧q"
oops
lemma ejercicio_14:
assumes 1: "p∧q"
shows "p"
oops
lemma ejercicio_15:
assumes 1: "p∧q"
shows "q"
oops
lemma ejercicio_16:
assumes 1: "p∧(q∧r)"
shows "(p∧q)∧r"
oops
lemma ejercicio_17:
assumes 1: "(p∧q)∧r"
shows "p∧(q∧r)"
oops
lemma ejercicio_18:
assumes 1: "p∧q"
shows "p⟶q"
oops
lemma ejercicio_19:
assumes 1: "(p⟶q)∧(p⟶r)"
shows "p⟶q∧r"
oops
lemma ejercicio_20:
assumes 1: "p⟶q∧r"
shows "(p⟶q)∧(p⟶r)"
oops
lemma ejercicio_21:
assumes 1: "p⟶(q⟶r)"
shows "p∧q⟶r"
oops
lemma ejercicio_22:
assumes 1: "p∧q⟶r"
shows "p⟶(q⟶r)"
oops
lemma ejercicio_23:
assumes 1: "(p⟶q)⟶r"
shows "p∧q⟶r"
oops
lemma ejercicio_24:
assumes 1: "p∧(q⟶r)"
shows "(p⟶q)⟶r"
oops
lemma ejercicio_25:
assumes 1: "p"
shows "p∨q"
oops
lemma ejercicio_26:
assumes 1: "q"
shows "p∨q"
oops
lemma ejercicio_27:
assumes 1: "p∨q"
shows "q∨p"
oops
lemma ejercicio_28:
assumes 1: "q⟶r"
shows "p∨q⟶p∨r"
oops
lemma ejercicio_29:
assumes 1: "p∨p"
shows "p"
oops
lemma ejercicio_30:
assumes 1: "p"
shows "p∨p"
oops
lemma ejercicio_31:
assumes 1: "p∨(q∨r)"
shows "(p∨q)∨r"
oops
lemma ejercicio_32:
assumes 1: "(p∨q)∨r"
shows "p∨(q∨r)"
oops
lemma ejercicio_33:
assumes 1: "p∧(q∨r)"
shows "(p∧q)∨(p∧r)"
oops
lemma ejercicio_34:
assumes 1: "(p∧q)∨(p∧r)"
shows "p∧(q∨r)"
oops
lemma ejercicio_35:
assumes 1: "p∨(q∧r)"
shows "(p∨q)∧(p∨r)"
oops
lemma ejercicio_36:
assumes 1: "(p∨q)∧(p∨r)"
shows "p∨(q∧r)"
oops
lemma ejercicio_37:
assumes 1: "(p⟶r)∧(q⟶r)"
shows "p∨q⟶r"
oops
lemma ejercicio_38:
assumes 1: "p∨q⟶r"
shows "(p⟶r)∧(q⟶r)"
oops
lemma ejercicio_39:
assumes 1: "p"
shows "¬¬p"
oops
lemma ejercicio_40:
assumes 1: "¬p"
shows "p⟶q"
oops
lemma ejercicio_41:
assumes 1: "p⟶q"
shows "¬q⟶¬p"
oops
lemma ejercicio_42:
assumes 1: "p∨q" and
2: "¬q"
shows "p"
oops
lemma ejercicio_43:
assumes 1: "p∨q" and
2: "¬p"
shows "q"
oops
lemma ejercicio_44:
assumes 1: "p∨q"
shows "¬(¬p∧¬q)"
oops
lemma ejercicio_45:
assumes 1: "p∧q"
shows "¬(¬p∨¬q)"
oops
lemma ejercicio_46:
assumes 1: "¬(p∨q)"
shows "¬p∧¬q"
oops
lemma ejercicio_47:
assumes 1: "¬p∧¬q"
shows "¬(p∨q)"
oops
lemma ejercicio_48:
assumes 1: "¬p∨¬q"
shows "¬(p∧q)"
oops
lemma ejercicio_49:
"¬(p∧¬p)"
oops
lemma ejercicio_50:
assumes 1: "p∧¬p"
shows "q"
oops
lemma ejercicio_51:
assumes 1: "¬¬p"
shows "p"
oops
lemma ejercicio_52:
"p∨¬p"
oops
lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops
lemma ejercicio_54:
assumes 1: "¬q⟶¬p"
shows "p⟶q"
oops
lemma ejercicio_55:
assumes 1: "¬(¬p∧¬q)"
shows "p∨q"
oops
lemma ejercicio_56:
assumes 1: "¬(¬p∨¬q)"
shows "p∧q"
oops
lemma ejercicio_57:
assumes 1: "¬(p∧q)"
shows "¬p∨¬q"
oops
lemma ejercicio_58:
"(p⟶q)∨(q⟶p)"
oops
end
