Deep inference and symmetry in classical proofs
In this thesis we see deductive systems for classical propositionaland predicate logic which use deep inference, i.e. inferencerules apply arbitrarily deep inside formulas, and a certainsymmetry, which provides an involution on derivations. Likesequent systems, they have a cut rule which is admissible. Unlikesequent systems, they enjoy various new interesting properties. Notonly the identity axiom, but also cut, weakening and even contractionare reducible to atomic form. This leads to inference rules that arelocal, meaning that the effort of applying them is bounded, andfinitely generating, meaning that, given a conclusion, there is only afinite number of premises to choose from. The systems also enjoy newnormal forms for derivations and, in the propositional case, a cutelimination procedure that is drastically simpler than the ones forsequent systems.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Alessio Guglielmi Apply the induction atomic cut rule atomic form atomic identity Briinnler calculus of structures classical logic co-weakening conclusion conjunction Corollary Craig interpolation cut admissibility cut elimination procedure cut formula cut-free decomposition theorems deduction theorem deductive systems deep inference Deep Symmetric System denoted disjunctive normal form duality Dually equivalence rule finite number finitely generating rules finitely generating system formula context identity and cut identity axiom induction hypothesis inference rules infinite choice instances of aw intuitionistic logic KSgq Lemma linear logic multiset natural deduction negation notion occur permutes predicate logic proof normalisation proof search proof theory propositional logic provable in system proviso reduced to atomic rule instance RV rule semantic sequent calculus sequent systems shown in Figure SKSgq SKSq soundness and completeness strongly equivalent switch rule symmetry system for predicate system GSlp system SKS system SKSg systems for classical up-rules vacuous quantifier variables