*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*: Wed, 23 May 2012 08:23:31 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <87bolf26jq.fsf@desktop.home.int>*References*: <87havcyn5p.fsf@desktop.home.int> <CANofLe+qNjhzCpQP41OE+dLh8LLPAZpXRN8YezngkygnoOWL+Q@mail.gmail.com> <87bolia9gu.fsf@desktop.home.int> <055B1615-BF79-4F6E-A706-11EF2B6DC4AA@cam.ac.uk> <87bolf26jq.fsf@desktop.home.int>

Almost certainly, you should be formalising these deductive formalisms inductively in Isabelle/HOL, not in Pure. Then you will be able to prove their meta-theoretic properties (their proof theory) straightforwardly. The deduction theorem inspires the sequent calculus, but it doesn't give you the sequent calculus. The sequent calculus is a formalism in its own right and should be formalised as such directly. Larry Paulson On 22 May 2012, at 23:29, Oleksandr Gavenko wrote: > On 2012-05-21, Lawrence Paulson wrote: > >> Normally, if you want to perform deductions that involve a set of >> assumptions, as the deduction theorem allows, you formalise a sequent >> calculus or alternatively a natural deduction system, of which several >> examples are already distributed with Isabelle. >> >> Most of our recent documentation focuses on how to use Isabelle/HOL, which >> is possibly not relevant to your application. What sort of calculus do you >> want to formalise, > > Sequent calculus. > >> And with what application in mind? > > There are many propositional logic axiom sets (and most uses Modus Ponens as > deduction rule) for which stated that they lie in specified type of logic but > proofs are lost or unaccessible. For example (if I am correct) this paper > > Łukasiewicz, Jan; Tarski, Alfred, "Untersuchungen über den Aussagenkalkül" > > (I read English translation in "Logic, Semantics, Metamathematics: Papers from > 1923 to 1938" by Alfred Tarski) state that these axioms: > > CCpqCCqrCpr > CCNppp > CpCNpq > > with MP allow to proof any true propositional sentence (without presenting > proof). This was shown during seminars at 1920-1930. > > My goal is to prove theorems in this system which have well known properties. > That shown that original axiom set have same properties... > > I decide use 'Pure' logic to record proofs in propositional logic by using MP > and substitution rules. This may be wrong decision but this solution is easy > to find in Isabelle sources (I use 'src/FOL/IFOL.thy' as start point). > > After some time of work I explore that I make many routine work. For example > if I prove this statement: > > A --> (B --> A) > A --> (B --> C)) --> ((A --> B) --> (A --> C)) > > I can use deduction theorem in human proofs to simplify my work. But how tell > to Isabelle that if I prove: > > A ==> B > > then it is possible to prove "A --> B" by modifying "A ==> B" proof? > > -- > Best regards! > >

**References**:**[isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Oleksandr Gavenko

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

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

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

*From:*Oleksandr Gavenko

- Previous by Date: [isabelle] jEdit: cursor movement and goal display
- Next by Date: Re: [isabelle] jEdit: cursor movement and goal display
- 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