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



On 2012-05-20, Randy Pollack wrote:

> 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.
>
Firstly thanks to Larry Paulson and Randy Pollack for answer...

I understand idea about "induction over these representations", and will try
to learn more on Isabelle to realise this idea...

> However reasoning _within_ such deeply embedded systems is not vey
> convenient unless you put effort into building tools.
>
I want to notice that proofs in 'Pure' also is not convenient.
For example without deduction theorem I need make a lot of rut work...

I as say that I am newbie for Isabelle and so I do not understand what you
mean by saying "building tools"... Can you explain more? Is this mean to write
some SML support code?

> 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.
>
By saying "nominal isabelle" do you mean:

  http://isabelle.in.tum.de/nominal/  ??

I would glad if someone point me for examples of "reasoning about formalized
object systems" as I new to this field and don't know from what to start...

-- 
Best regards!






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