Aspects of an internal logic for persistence arXiv 1409.3762

João Pita Costa, Primož Škraba, Mikael Vejdemo-Johansson

Abstract. The foundational character of certain algebraic structures as Boolean algebras and Heyting algebras is rooted in their potential to model classical and constructive logic, respectively. In this paper we discuss the contributions of algebraic logic to the study of persistence based on a new operation on the ordered structure of the input diagram of vector spaces and linear maps given by a filtration. Within the context of persistence theory, we give an analysis of the underlying algebra, derive universal properties and discuss new applications. We highlight the definition of the implication operation within this construction, as well as interpret its meaning within persistent homology, multidimensional persistence and zig-zag persistence.

Topological data analysis has been a vibrant area of research a lot due to the developments in applied and computational algebraic topology. It applies the qualitative methods of topology to problems of machine learning, data mining and computer vision. Persistent homology, as the most widely applied tool from computational algebraic topology has been applied to problems in machine learning, data mining, robotics, social media, large scale data, natural image statistics, nonlinear systems, medicine and cancer research, and development of more accurate models. In the past years several extensions of persistence were proposed, including zig-zag persistence, and multidimensional persistence. Recently, persistent homology has been studied using techniques from lattice theory with several algorithmic applications and structural consequences. This is of particular interest for diagrams of vector spaces of different shapes. With the appropriate definitions, such diagrams form lattices: partially ordered sets (posets) with uniquely determined greatest lower bounds and least upper bounds, encoded as additional binary operations named meet and join. These lattices are equipped with the structure of a Heyting algebra: in addition to meet and join acting as conjunctive and disjunctive operators, they also admit an implication operator allowing them to serve as algebraic models of constructive logic in the same way as Boolean algebras model classical logic.

Constructive logic replaces the traditional concept of truth with the concept of constructive provability and is associated with a transition from the proof to model theory of abstract truth where semantics mirrors classical Boolean-valued semantics using Heyting algebras in place of Boolean algebras. The proofs produced by constructive logic have the existence property, making it suitable for the algorithmic construction of examples from a constructive proof of the existence of certain object. Already Markov expresses that the significance for mathematics of rendering more precise the concept of algorithm emerges in connection with a certain constructive foundation for mathematics, and the further applications of such work. Heyting algebras are presented in \ref{Heyting algebras and Boolean algebras} and their associated constructive logic will be briefly discussed in this paper. Due to its constructive nature, this logic presents a different perspective. The relevance of Heyting algebras for the study of persistent homology is further clarified in this paper, in a wider context of the unification by topos theory.

In this paper we also present a further step in this direction of research towards such topos theoretical foundations. Our main contribution is the definition and interpretation of the implication operation over the underlying Heyting algebra. In particular, we analyze the implication between two vector spaces of a given diagram in the context of standard, multidimensional and zig-zag persistence. The latter case is motivated by the lattice construction for zig-zag persistence. Furthermore, we will give an interpretation of the implication operation and discuss aspects of the correspondent internal logic given by the underlying algebra.

JOÃO PITA COSTA 2014