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



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





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