# Can all classical math proofs be represented in type theory?

The curry howard isomorphism states that proofs in intuitionist logic can be represented as terms, and theorems as types.

However, I'm wondering: if we add the classical logical axioms like LEM (and the axiom of choice?), is it then possible to do all classical proofs in type theory?

Or are only theorems that are provable from intuitionist logic, provable in type theory?

• "Type theory" is not a single thing, but a loosely-related family of foundational proposals. Your answer might well be different between them. Are you talking about Russell-Whitehead PM? Church's simple types? Martin-Löf type theory? Homotopy type theory? – Henning Makholm Jul 14 '18 at 17:45
• @HenningMakholm, I am talking about type theory in general, and in particular proof-assistants. So an answer to my question could be: "It is possible in type theory X because of reason Y, but not in type theory Z because of reason W" – user56834 Jul 14 '18 at 18:07
• For an exposition on curry howard for classical logic, see homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf – spaceisdarkgreen Jul 14 '18 at 18:08
• Actually, now that I think of it, I am primarily interested in the answer with respect to dependent type theory based on the CoC, as used in the proof assistant Lean or Coq – user56834 Jul 14 '18 at 18:09
• @spaceisdarkgreen, thanks! – user56834 Jul 14 '18 at 18:09

With both LEM and a type theoretic analogue of the Axiom of Choice, you do end up with a system at least as strong as ZFC. A Coq development demonstrating this is here, created by the author of Sets in types, types in sets. That paper actually claims even more, namely that ZFC+$n$ inaccessible cardinals is encodable into the Calculus of Inductive Constructions (plus the above axioms) with $n+1$ universes. It also goes the other way and encodes CIC with $n$ universes into ZFC + $n$ inaccessible cardinals.
The Coq development actually proves all of the axioms of ZFC except replacement and choice without assuming any axioms (not even LEM). That is, it shows that Coq can encode an intuitionistic variant $Z$ and classical $Z$ if you do include LEM, though CIC(+LEM) is likely quite a bit stronger than $Z$ due to its higher order features. If we assume a type theoretic Axiom of Choice but not LEM, we can prove the Axiom Schema of Collection which is equivalent to the Axiom Schema of Replacement when we add LEM.