# [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
*From*: Oleksandr Gavenko <gavenkoa at gmail.com>
*Date*: Sat, 19 May 2012 22:40:50 +0300
*Cancel-lock*: sha1:b4B/KMx+EIQ4aRzNYRvGQNLgI80=
*Organization*: At home.
*User-agent*: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)

I am newbie to Isabelle and I have hobby interest to make proofs in different
propositional deduction systems (sorry if my English too bad).
I start from 'src/FOL/IFOL.thy' and make such code:
theory mylogic
imports Pure
begin
typedecl o
judgment
Trueprop :: "o => prop" ("(_)" 5)
consts
Imp :: "o \<Rightarrow> o \<Rightarrow> o" ("_ --> _" 40)
axiomatization where
ax1: "A --> (B --> A)" and
ax2: "(A --> (B --> C)) --> ((A --> B) --> (A --> C))"
axiomatization where
mp: "\<lbrakk>P; P-->Q\<rbrakk> \<Longrightarrow> Q"
lemma imp_refl: "A --> A"
apply(rule_tac P = "A-->(B-->A)" in mp)
apply(rule ax1)
apply(rule_tac P = "A-->((B-->A)-->A)" in mp)
apply(rule ax1)
apply(rule ax2)
done
lemma impI_from_assumption: "P ==> (Q --> P)"
apply(rule_tac P = "P" in mp)
apply(assumption)
apply(rule ax1)
done
lemma anything_imp_true: "B --> (A --> A)"
apply(rule impI_from_assumption)
apply(rule imp_refl)
done
lemma deduction_thm: "(P \<Longrightarrow> Q) \<Longrightarrow> (P --> Q)"
oops
end
Set of axioms take straight possibility to prove deduction theorem like this
done in any textbook for math logic and it can be formalised in Isabelle (see
'deduction_thm').
Lemma 'impI_from_assumption' shown that simple meta-theorem can be proved and
can be used in next proofs.
Is it possible to prove 'deduction_thm' and how to do this?
--
Best regards!

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*