# 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^{1} [^{1} 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

groupis 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,^{2} [^{2} 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.

## Footnotes:

^{1}

Here I'll be specifically refering to classical first-order logic with equality.

^{2}

What percentage of mathematicians, if pressed, could come up with a non-contradictory set of axioms for set theory? We know Frege could not!