Katsuhiko Sano and Jonni Virtema: Characterizing Frame Definability in Team Semantics via The Universal Modality

A. Carbone developed in her work in 1999 a combinatorial model to study the evolution of proofs during the procedure of cut elimination. She defined an operation called duplication and worked with the logical flow graphs extracted from sequent calculus proofs in order to propose a purely combinatorial analysis of cut elimination. Here we develop a modification of the combinatorial model defined by Carbone to study the normalization of N-Graphs. The system, proposed by de Oliveira in 2001, is a multiple conclusion natural deduction with proofs as directed graphs. N-Graphs were motivated by the idea of proofs as geometric objects and aimed towards the study of the geometry of Natural Deduction systems. Following that line of research, we propose a normalization procedure defined as a set of combinatorial operations on graphs and present upper and lower bounds for the size of normalized proofs. The normalization we present in this paper also works as an extension of the normalization defined by Prawitz, i.e. it has the separation and subformula properties.