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

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:


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.