Mathematical Language and Soft Type Systems

1. After writing some thoughts about the next generation of provers, I'd like to draw your attention to a couple papers:

1. F. Wiedijk,
   "Mizar's Soft Type System."
   In: K. Schneider & J. Brandt (eds.), Theorem Proving in Higher Order Logics 2007, LNCS 4732, 383-399, 2007; pdf
2. Cezary Kaliszyk, Florian Rabe,
   "A Survey of Languages for Formalizing Mathematics".
   arXiv:2005.12876, 19 pages

I mention these papers as worth reading, for a couple reasons: first, they discuss an example of what a "higher level of abstraction" actually looks like; second, Kaliszyk and Rabe's paper complements Avigad's paper quite well.

2. Definition. Recall that type theory works by making typing judgements part of the metalanguage. A Soft Type System introduces typing judgements as propositions (and types as predicates) in the object language.

2.1. Example. For a concrete example of soft types in predicate logic, a dependent type with $n$ parameters is represented as an $n+1$-ary predicate $T(x, c_{1}, \dots, c_{n})$ interpreted as $x : T~c_{1}\dots c_{n}$. Subtyping is interpreted as $\forall x, S(x)\implies T(x)$ to assert $S$ is a subtype of $T$, and so on.

2.2. Remark (Soft Types in Type Theory). This is not limited to "non-type theoretic foundations". For example C-Corn in Coq uses a version of a soft type system, as a means to increase the level of abstraction.

2.3. I bring this up because soft types increase the level of abstraction for formalizing mathematics. It's a non-obvious step, which approximates mathematical practice, and demonstrates the sort of "extensibility" I think the next generation of provers may need. Amazingly enough, it can encode the axiom of choice (see, e.g., slides about the [type] usage in Mizar for encoding choice).

3. Mathematical Language. The only addendum I have to add from my last post is just a reference to Kaliszyk and Rabe's paper. It works in a "dual" manner to Avigad's paper, trying to think about a "pseudocode" for formalizing mathematics by surveying what different provers do.

The only qualm I have with their paper is precisely addressed by Avigad's paper: it's useful to give a lot of "small snippets" when trying to think about designing a language. Working in the abstract is, well, abstract. And hard.