*To*: Oleksandr Gavenko <gavenkoa at gmail.com>*Subject*: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 20 May 2012 17:39:35 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <87havcyn5p.fsf@desktop.home.int>*References*: <87havcyn5p.fsf@desktop.home.int>

Isabelle is not a “meta-logical-framework". So you cannot perform induction over an inference system you introduce to it. Larry Paulson On 19 May 2012, at 20:40, Oleksandr Gavenko wrote: > 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! > >

**References**:

- Previous by Date: Re: [isabelle] RC3 startup problem on Scientific Linux
- Next by Date: Re: [isabelle] Display Draft in Jedit
- Previous by Thread: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Next by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list