Tools and techniques for formalising structural proof theory
Abstract
Whilst results from Structural Proof Theory can be couched in many formalisms, it is
the sequent calculus which is the most amenable of the formalisms to metamathematical
treatment. Constructive syntactic proofs are filled with bureaucratic details; rarely are
all cases of a proof completed in the literature. Two intermediate results can be used to
drastically reduce the amount of effort needed in proofs of Cut admissibility: Weakening
and Invertibility. Indeed, whereas there are proofs of Cut admissibility which do not use
Invertibility, Weakening is almost always necessary. Use of these results simply shifts the
bureaucracy, however; Weakening and Invertibility, whilst more easy to prove, are still not
trivial. We give a framework under which sequent calculi can be codified and analysed,
which then allows us to prove various results: for a calculus to admit Weakening and for a
rule to be invertible in a calculus. For the latter, even though many calculi are investigated,
the general condition is simple and easily verified. The results have been applied to G3ip,
G3cp, G3s, G3-LC and G4ip.
Invertibility is important in another respect; that of proof-search. Should all rules in
a calculus be invertible, then terminating root-first proof search gives a decision procedure
for formulae without the need for back-tracking. To this end, we present some results
about the manipulation of rule sets. It is shown that the transformations do not affect the
expressiveness of the calculus, yet may render more rules invertible. These results can guide
the design of efficient calculi.
When using interactive proof assistants, every case of a proof, however complex, must be
addressed and proved before one can declare the result formalised. To do this in a human readable
way adds a further layer of complexity; most proof assistants give output which is
only legible to a skilled user of that proof assistant. We give human-readable formalisations
of Cut admissibility for G3cp and G3ip, Contraction admissibility for G4ip and Craig's
Interpolation Theorem for G3i using the Isar vernacular of Isabelle. We also formalise the
new invertibility results, in part using the package for reasoning about first-order languages,
Nominal Isabelle. Examples are given showing the effectiveness of the formalisation. The
formal proof of invertibility using the new methods is drastically shorter than the traditional,
direct method.
Type
Thesis, PhD Doctor of Philosophy
Rights
Creative Commons Attribution-ShareAlike 3.0 Unported
http://creativecommons.org/licenses/by-sa/3.0/
Collections
Except where otherwise noted within the work, this item's licence for re-use is described as Creative Commons Attribution-ShareAlike 3.0 Unported
Items in the St Andrews Research Repository are protected by copyright, with all rights reserved, unless otherwise indicated.