Infinitary logic with infinite sequents: syntactic investigations

The present paper deals with a purely syntactic analysis of infinitary logic with infinite sequents. In particular, we discuss sequent calculi for classical and intuitionistic infinitary logic with good structural properties based on sequents possibly containing infinitely many formulas. A cut admissibility proof is proposed which employs a new strategy and a new inductive parameter. We conclude the paper by discussing related issues and possible themes for future research.

Automated summary

This paper presents a purely syntactic analysis of infinitary logic with infinite sequents. It discusses sequent calculi for classical and intuitionistic infinitary logic, which have good structural properties and allow sequents to possibly contain infinitely many formulas. A cut admissibility proof is proposed using a new strategy and a new inductive parameter. The paper concludes by discussing related issues and potential themes for future research.