Proof Systems are Operating Systems

I met with a student recently who was a little confused by the relationship between first-order logic, ZFC, dependent types, Martin-Löf, and so on. Recalling S. Aaronson, I explained it by analogy to computers.

Proof systems, like first-order logic¹ [¹ Here I'll be specifically refering to classical first-order logic with equality.] or dependent types, are like the operating system for your computer. By themselves, they do not do much; their main goal is to run particular programs.

These programs are particular logical theories, like ZFC or System F. Different programs do different things; the theory of groups is a good program for studying group theory, while the theory of sets is a good program for studying set theory. ZFC is a popular program running on the first-order logic operating system. Naturally, programs are not always portable between operating systems; running ZFC on dependent types is a bit of a pain, and the result (ETCS) is somewhat different.

Miraculously, some programs can emulate other operating systems, just like VirtualBox lets you run Windows inside your Linux computer. For example, ZFC can emulate dependent type theory (via frames), and you can run ZFC inside Coq (which is a program running on the "dependent types" operating system).

Different operating systems run on different hardware: core mathematical structures that support inference in that operating system. First-order logic uses substitution as its core inference technique, which is why equality is built-in as part of first-order logic. Dependent type theory uses computation as its core inference technique. The difference in hardware makes using these two operating systems quite different: you can "hard-code" a system into first-order logic by simply assuming the right set of equalities, while hard-coding a system into dependent type theory requires a decision procedure, a computational step.

If you are a mathematician, you are intimately familiar with first-order logic. Programs in first-order logic are defined by listing several sets, several operators, and several relations, and in fact if you open up a book on group theory you will see,

A group is a tuple \((G, \times, ^{-1}, e)\), where \(G\) is a collection of members, \(a \times b\) is in \(G\) for all \(a, b \in G\), \(a^{-1}\) is in \(G\) for \(a \in G\), and \(e\) is a distinguished member of \(G\).

This is how you implement a program that runs on the OS of first-order logic. Groups are defined in terms of one collection and three operators (of arity 2, 1, and 0).

Mathematicians prefer to pretend that they run their programs in an emulator called ZFC, instead of directly atop atop first-order logic. This way they obscure the importance of non-formal hardware. This is analogous to teaching a class on Linux while running Linux inside an emulator, so that hardware support is not an issue. Despite this confusing myth, mathematicians by and large know little about ZFC,² [² What percentage of mathematicians, if pressed, could come up with a non-contradictory set of axioms for set theory? We know Frege could not!] because in fact they just run their theories directly atop first-order logic.