*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*: Joao Marcos <botocudo at gmail.com>*Date*: Tue, 29 May 2012 08:29:58 -0300*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>

The question seems not to be without interest. Has anyone in the list ever proved in Isabelle the meta-deduction theorem for, say, the implicational fragment of intuitionistic Hilbert calculus? JM On Tue, May 22, 2012 at 7:29 PM, Oleksandr Gavenko <gavenkoa at gmail.com> 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! > > -- http://sequiturquodlibet.googlepages.com/

**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: Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features
- Next by Date: Re: [isabelle] Isabelle/jEdit: Multiline Comments/Reparsing
- Previous by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Next by Thread: [isabelle] RC3 startup problem on Scientific Linux
- 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