A language for mathematical knowledge management

TL;DR

This paper advocates using Zermelo Fraenkel set theory with definitions as a foundational language for mathematical knowledge management, introducing a more readable syntax and analyzing the complexity of formalized definitions.

Contribution

It introduces a syntactic sugar for set-theoretic language that enhances readability and provides empirical data on the complexity of formalized mathematical definitions.

Findings

The proposed language improves readability of formal assertions.

Formalized definitions vary in complexity across different measures.

The set-theoretic framework effectively supports mathematical knowledge sharing.

Abstract

We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity measures.