Geometric Rules in Infinitary Logic

Several mathematical theories - such as the theory of torsion abelian groups, of Archimedean ordered fields, and of connected graphs - are axiomatized by infinitary geometric implications. Proof analysis is extended to all such theories by augmenting an infinitary classical sequent calculus with a rule scheme for infinitary geometric implications. The calculus is designed in such a way as to have all the rules invertible and all the structural rules (weakening, contraction, and cut) admissible. An intuitionistic infinitary multisuccedent sequent calculus is also introduced, and is shown to enjoy the same structural properties. Finally, bringing the classical and intuitionistic calculi close to each other yields the infinitary Barr theorem without any further ado. [This is talk is based on unpublished joint work with the late Roy Dyckhoff.]

Contact person: Peter Schuster