26
$\begingroup$

Most proof assistants (with some exceptions like Isabelle/ZF or the B method) rely on type theory.

See also the MathOverflow question What makes dependent type theory more suitable than set theory for proof assistants?

Next, formalizing mathematics is one of the main use cases of an interactive proof assistant.
But many pen-and-paper mathematical proofs are written in a set-theoretic fashion (e.g., in ZFC).

Finally, there are many different type theories (first-order, higher-order, dependently-typed or not, intuitionistic or not, etc.)

So, formalizing existing set-theoretic results typically involves some formal hindrances.

Keeping the constructiveness issue apart, and focusing on the definability of mathematical objects:

  1. what mathematical concepts can't typically be "formalized as is", within the main proof-assistants / type-theories?
    (e.g., we can think about matrices in a non-dependently-typed theory…)
  2. is a "workaround" possible, to still be able to formally deal with this mathematical concept in the considered theory? (if yes, feel free to cite a formalization example)
$\endgroup$
4
  • 3
    $\begingroup$ You might be interested in this: An initial algebra of a complete sup-lattice equipped with an endofunction is exactly a model of IZF... This can be formalized in type theories with HITs. $\endgroup$
    – Trebor
    Feb 9, 2022 at 5:16
  • $\begingroup$ Thanks @Trebor (I guess we could say your answer refer to some "deep embedding"; while "shallow embedding"-like answers could be interesting as well) $\endgroup$
    – ErikMD
    Feb 9, 2022 at 12:25
  • $\begingroup$ I wasn't the close voter, but I presume the close vote was because this question seems to ask two questions instead of one, and most sites have a one-question-per-post policy. $\endgroup$ Feb 9, 2022 at 22:52
  • 1
    $\begingroup$ Notably, even Isabelle/ZF shares with Isabelle/HOL a common root Pure that is a very weak type theory. $\endgroup$ Feb 12, 2022 at 14:12

2 Answers 2

30
$\begingroup$

Almost no pen-and-paper mathematics is written in ZFC. The vast majority of mathematical texts is actually written in something that resembles structural set theory and is closer to type theory than to ZFC.

Most mathematics can be formulated in type theory in a fairly straightforward manner. However, not every brand of type theory is equally good for formalization of mathematics. Some type theories are more like programming languages, and others are geared towards formalization of mathematics.

Here are some features that make it easier to formalize mathematics in type theory:

  1. Quotients: it is annoying to not be able to form quotients by equivalence relations. In type theories without quotients people use setoids (types equipped with equivalence relations) – and those who worked with setoids sometimes refer to the activity as "setoid hell".

  2. Impredicativity: often a type theory does not have a type of truth values, but instead has a whole hierarchy of them (one in each universe). This leads to various complications because one has to keep track of universes.

  3. Extensional equality: In type theory equality is represented by identity types. These may behave in unusual ways, unless we adopt some principles (such as Uniqueness of identity proofs or equality reflection).

  4. Function extensionality: this principle states that $f, g : A \to B$ are equal if $f(x) = g(x)$ for all $x : A$. It seems quite hard to do mathematics without this principle.

  5. Other extensionality principles: these are principles like "equivalent propositions are equal" and "pairs are equal if their first and second components are equal".

  6. Excluded middle and the axiom of choice are needed to a much lesser degree than one might expect.

Some type theories have all of the above constructions and principles, for instance the type theory of Lean. By doing so they sacrifice some good computational properties that "pure" type theories have (by this I mean that the type theory can be used a programming language as well as a foundation of mathematics). And there are alternatives which keep the good computational properties but require one to rethink how mathematics is done (such as cubical type theories).

$\endgroup$
19
  • 2
    $\begingroup$ @M.Lonardi They can be added to a proof assistant. It might not be clear from the way it was written but lean has all of 1-6. HoTT also has quotient types, but without proof irrelevance I would argue that they don't act in the way one would normally expect, and I'm not sure if they are actually strong enough to escape "setoid hell". $\endgroup$ Feb 10, 2022 at 8:54
  • 7
    $\begingroup$ @MarioCarneiro: setoid hell arises because one has to verify that a map respects equivalences all the time, even when no quotients are really involved. The HoTT quotients are like any other quotients: you only need to check that something is being preserved when you map out of a quotient type. So I'd say it's not really setoid hell. $\endgroup$ Feb 10, 2022 at 14:36
  • 1
    $\begingroup$ Maybe worth noting that there are different kinds of impredicativity. The propositional-resizing sort of impredicativity is indeed very helpful for formalizing mathematics (which sounds like what you were referring to), but impredicative quantification for a non-propositional universe is not really very relevant for mathematics. $\endgroup$ Feb 10, 2022 at 18:35
  • 3
    $\begingroup$ @MarioCarneiro HoTT quotients do act the way you would expect when you talk only about types that are sets, because in that case you do have "local" proof-irrelevance. It's best to think about HoTT not as saying that "the types you're used to act in weird ways" but rather that "in addition to the types you're familiar with that act in the usual way, there are also higher types that act in different ways". $\endgroup$ Feb 10, 2022 at 18:36
  • 1
    $\begingroup$ Paragraph number 2, about Basic Law V. Be careful: sometimes the proofs are hidden by a link, you have to click on it. $\endgroup$
    – M. Lonardi
    Feb 11, 2022 at 13:25
11
$\begingroup$

Andrej's answer that "Almost no pen-and-paper mathematics is written in ZFC" is correct. But it's perhaps also worth noting that some pen-and-paper mathematics is written in ZFC (or, at least, something closer to ZFC than to type theory), such as much of the mathematics done by set theorists (in which phrase, of course, "set" refers traditionally to a ZFC-set).

A good deal of set theory can be rephrased more structurally to make sense in type theory, but this would be a rephrasing, and the amount of work that would be required is, I think, variable. For instance, set theorists work with ordinals defined in the von Neumann way, with $\in$ as the well-founded relation. This in particular implies that ordinals are literally unique representatives of isomorphism classes of well-ordered sets. In type theory it is more natural to work "structurally" with arbitrary well-ordered sets rather than with von Neumann ordinals. This makes some things more cumbersome because of isomorphisms that get carried around (although under univalence, these isomorphisms become equalities), but probably doesn't change things a whole lot.

On the other hand, as far as I know, no one has ever come up with a convincing structural presentation of Godel's constructible universe $L$. The only structural approaches to $L$ that I know of essentially involve building a model of ZF(C) in some way and then constructing $L$ inside that model. Note that $L$ is, as far as I know, still the only way to prove the relative consistency of the Axiom of Choice, so it is of interest even to mathematicians who don't care about ZF for its own sake. (In contrast, the symmetric/permutation methods used to prove relative consistency of not-AC, and the forcing methods that can be used to prove consistency of other properties such as GCH and not-GCH, seem much more amenable to structuralization.) [Note: this paragraph was edited to remove a false claim that GCH is not forceable; see comments.]

As another example, Scott's trick is a method used in pen-and-paper mathematics that is of interest beyond set theory, but relies on the axiom of foundation from ZFC, and so is not obviously formalizable in type theory.

$\endgroup$
19
  • $\begingroup$ You can force GCH using Easton (class) forcing. That’s essentially the same as good old forcing, but the poset used is a definable class instead of an element of the ground model. $\endgroup$ Mar 5, 2022 at 2:05
  • $\begingroup$ Has there been a non-convincing strutural presenrtation of $L$? $\endgroup$ Mar 5, 2022 at 7:27
  • 1
    $\begingroup$ I had the same thought as PMP but I gave up on it because the construction of L is throwing in rather specific sets (the definable ones, in a suitable sense), whereas an inductive-recursive definition of U throws in functions A → U from the ambient type theory. I am afraid this won't give enough control over what lands in U. $\endgroup$ Mar 6, 2022 at 7:43
  • 1
    $\begingroup$ @PedroSánchezTerraf Thanks. I would actually be interested already in a reference for how to force ordinary CH. Why is this not better known? Everyone always cites L as the reason why (G)CH is consistent but forcing as the reason why not-(G)CH is consistent. $\endgroup$ Mar 6, 2022 at 17:38
  • 1
    $\begingroup$ @PedroSánchezTerraf Most uses of ordinals can be easily rephrased structurally in terms of arbitrary well-founded relations. $\endgroup$ Mar 15, 2022 at 16:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.