An inquiry into the Foundations of Mathematics

Starting from the question of what consequence Gödel's incompleteness theorem has on the foundations of mathematics, we argue for new foundations, and build some intuition for these new foundations in Coq.

Mathematics can be thought of as a game where you start with some objects (say, sets), some axioms on the objects (typically, ZFC), and use a calculus of logical deductions (such as classical logic) to prove things. To mechanize this game in a proof assistant, one would either use a proof-search or tactic system, and check subject reduction. However, mechanized mathematics is done differently from classical mathematics, and we first investigate whether building new foundations is justifiable.

Gödel's second incompleteness theorem states that any formal system, that can express elementary arithmetic, cannot prove its own consistency, assuming à priori that the system is consistent. It doesn't destroy the platonic view of mathematics as such, but does destroy the view that there is only one correct foundation for mathematics. Further, one would argue that it is precisely this result that makes mathematics exciting: we can keep rewriting foundations to better suit our abstract intuitions, and build higher abstractions, without worrying about whether there is "one true foundation".

Departing from ZFC foundations

Some mathematicians would then argue that we've settled on ZFC and classical logic as foundations, but this is only true of 80% of recent mathematical literature. Category theory, in particular, breaks away from set-theoretic foundations; objects and morphisms aren't sets. Indeed, set-theoretic questions about categories are ill-formed, although one can encode boolean algebras using topoi.

Moreover, one should aim for a foundation that is conducive to mechanization, so proofs can be checked for correctness in an automated fashion. The strategy that Veovodsky et al. used was to extend Martin-Löf type theory, and build a branch of mechanized mathematics, homotopy type theory, which we will refer to henceforth as HoTT. It is formalized in Coq, whose foundations are based in Martin-Löf Type Theory.

Preliminaries

What the following proposition says, is that, for every inhabitant of that you supply, will supply an inhabitant of $𝟙$ :

Theorem f : nat -> unit.
Proof.
  intros x.
  exact tt.
Qed.

The proof is witness that we can always supply an inhabitant of the type $𝟙$ . By Curry-Howard isomorphism:

Definition f' : nat -> unit := fun _ => tt.

In type theory, a function is just a non-dependent version of the type, where the codomain is fixed:

The logical connective , which we will use in the next section, has the following definition in type theory:

𝟘

Two intuitions in classical mathematics broken

Our first example is the classic proof-by-contradiction. A proof in constructive mathematics cannot proceed in the following logical sequence for a proposition :

In other words,

This is in line with the general philosophy of constructive mathematics, where non-existence of an inhabitant of a type cannot be proved; to supply a witness is to supply a construction of the inhabitant, and indeed, no such construction might exist. Nevertheless, an axiom of excluded middle can be axiomatized and used to construct-via-contradiction, just like any other axiom:

Axiom LEM : forall (P : Prop), P \/ ~P.

To understand this better, let us take the example of the constructive equivalent of $𝟘$ in classical mathematics:

Theorem FalseImpliesAnything : forall A, False -> A.
Proof.
  intros A.
  exact (fun x : False => match x with end).
Qed.

Since $𝟘$ has no inhabitants, the construction of any inhabitant of any type can be proved from it.

It is perhaps prudent to supply another example of a classical statement to illustrate Coq's typechecker:

Theorem TrueDoesNotImplyFalse : True -> False.
Proof.
  (* Due to enforced exhaustive pattern-matching on inhabitants of the LHS,
   * we'd need to match up an inhabitant of True (there is only I)
   * to some inhabitant of False, but there are no inhabitants of False.
   *)
Abort.

In category theory, $𝟘$ would be the initial object, and there is at most one arrow from the initial object to every other object in the category; $𝟙$ would be the final object, and there is at most one arrow from every other object in the category to it. The above theorem hypothesizes the existence of a morphism from the final object to the initial object, which of course, cannot exist.

𝟘 𝟙 𝟘 𝟙

For the second example, let us investigate the classical notion of proof irrelevance. In ZFC, sets and propositions are in different universes of discourse, as opposed to type theory, where proofs objects are first-class. Over the course of its development, the question of proof relevance was raised in type theory. In the following example, and are inhabitants of the type , and the question is whether is different from :

The answer, as supplied by HoTT, is: yes, proofs are relevant, and is different from ; a proof is viewed as a homotopy path between two homotopy types, and there is a notion of homotopy equivalence between homotopy paths. In classical mathematics, would always be equal to .