*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?*From*: Oleksandr Gavenko <gavenkoa at gmail.com>*Date*: Wed, 23 May 2012 01:29:45 +0300*Cancel-lock*: sha1:QR9uDcbw5biKssKvpQJvMFmzuac=*Organization*: At home.*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>*User-agent*: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)

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!

**Follow-Ups**:

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

- Previous by Date: Re: [isabelle] Build LaTex document without proof checking
- Next by Date: Re: [isabelle] RC3 startup problem on Scientific Linux
- 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