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



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






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