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



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/





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