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



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.