Deep Inference and Symmetry in Classical Proofs
Kai Brünnler
ISBN 978-3-8325-0448-9
101 Seiten, Erscheinungsjahr: 2004
Preis: 40.50 €
In this thesis we see deductive systems for classical propositional
and predicate logic which use deep inference, i.e. inference
rules apply arbitrarily deep inside formulas, and a certain
symmetry, which provides an involution on derivations. Like
sequent systems, they have a cut rule which is admissible. Unlike
sequent systems, they enjoy various new interesting properties. Not
only the identity axiom, but also cut, weakening and even contraction
are reducible to atomic form. This leads to inference rules that are
local, meaning that the effort of applying them is bounded, and
finitely generating, meaning that, given a conclusion, there is only a
finite number of premises to choose from. The systems also enjoy new
normal forms for derivations and, in the propositional case, a cut
elimination procedure that is drastically simpler than the ones for
sequent systems.