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
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.
What the following proposition says, is that, for every 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
Definition f' : nat -> unit := fun _ => tt.
In type theory, a function is just a non-dependent version of the
The logical connective
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
Theorem FalseImpliesAnything : forall A, False -> A. Proof. intros A. exact (fun x : False => match x with end). Qed.
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,
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,
The answer, as supplied by HoTT, is: yes, proofs are relevant, and