*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*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Sun, 20 May 2012 14:22:26 -0400*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <87havcyn5p.fsf@desktop.home.int>*References*: <87havcyn5p.fsf@desktop.home.int>*Sender*: rpollack0 at gmail.com

You can do meta logic of "deeply embedded" formal systems. Define the syntax and derivations of your object system as datatypes and inductive relations in (for example) isabelle HOL. Then you have the power of induction over these representations. However reasoning _within_ such deeply embedded systems is not vey convenient unless you put effort into building tools. Propositional logic should be simple. If your object system has binding, look into using nominal isabelle. There are many examples of reasoning about formalized object systems. Randy -- On Sat, May 19, 2012 at 3:40 PM, Oleksandr Gavenko <gavenkoa at gmail.com> 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! > > >

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] Display Draft in Jedit
- Next by Date: Re: [isabelle] Display Draft in Jedit
- Previous by Thread: Re: [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