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



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






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