# [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!

```

• Follow-Ups:

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