7
$\begingroup$

As a personal project, I decided to prove everything I learned in mathematics using formal proofs. The difference between informal proof, which is commonly used by mathematicians, and formal proof is shown in Chapter 3 of the book "Logic, Mathematics, and Computer Science" by Yves Nievergelt.

During the course of this project, I encountered a problem that I will attempt to illustrate below. Let's consider the axiom of pairing:

$$\vdash \forall x\forall y\exists z\forall w(w\in z\leftrightarrow w=x\vee w=y)$$

You can prove that there's only one set $z$ satisfying the previous axiom, that is, you can prove that

$$\vdash \forall x\forall y\exists \color{red}{!}z\forall w(w\in z\leftrightarrow w=x\vee w=y)\,\,\color{red}{(1)}$$

Because of this, it's conventional to denote the set $z$ by $\{x,y\}$. However, according to the book "Set Theory" by András Hajnal (see page 115), an additional axiom is required to formalize this convention. The approach given in this book with regard to the axiom of pairing is as follows:

First you define $\phi(x,y,z):=\forall w(w\in z\leftrightarrow w=x\vee w=y)$. The book calls this the defining postulate of the operator $\{\,,\}$.

According to $(1)$, we have $\vdash \forall x\forall y\exists !z\phi (x,y,z)$. Then we add the following axiom: $\vdash \forall x \forall y\phi(x,y,\{x,y\})$. This extension is an effective strict conservative extension (see the Theorem A2.1 of the book).

My question is: does type theory help us avoid the need to add more axioms for each new definition?

I am looking for a formal language that can express, for example, the axiom of pairing and introduce the set builder notation $\{\,,\}$ without requiring an additional axiom.

Having skimmed through "Type Theory and Formal Proof” by Rob Nederpelt, I have the impression that it's possible to achieve this using an extension of Calculus of Constructions denoted by $\lambda D$ in this book. However, since I know nothing about type theory, it's possible that I am misinterpreting its usage.

Thank you for your attention!

Improve this question
$\endgroup$
2
  • 6
    $\begingroup$ The relevant keyword for the process you describe is: definitional expansion. It is a general fact that every definitional expansion of a theory is a conservative extension, proving no new assertions expressible in the original language, and furthermore, every assertion in the new language is provably equivalent to one in the original language. So another way to express your question is: how does type theory handle definitional expansions? $\endgroup$
    – Joel David Hamkins
    Commented Apr 7, 2023 at 16:13
  • 2
    $\begingroup$ Isn't introducing a type to represent the term basically analogous to introducing a definitional expansion? To introduce a new notation, one seems to need somehow to define what it is or how it functions. It seems to me that any manner of introducing a term will involve something essentially analogous to the definitional expansion. $\endgroup$
    – Joel David Hamkins
    Commented Apr 7, 2023 at 17:49

1 Answer 1

Reset to default
5
$\begingroup$

Indeed, type theory does not need to add new axioms to represent definitions. The basic idea is that the formal language of type theory contains a binding form for terms -- something like:

$\mathsf{let}\; x = e_1 \;\mathsf{in}\; e_2$

This introduces the name $x$ for the expression $e_1$ within the scope of the expression $e_2$. The judgmental equality rule for this construct is also very simple: we say that $\mathsf{let}\; x = e_1 \;\mathsf{in}\; e_2$ is judgementally equal to $[e_1/x]e_2$ (i.e., substituting $e_1$ for $x$ everywhere in $e_2$).

This corresponds to writing something like "Let $x$ be $e_1$. Now, $e_2$" in mathematical vernacular. Furthermore, when we introduce such a construction, we feel to switch between writing $x$ and $e_1$ without comment (unless it is somehow instructive to note) -- this corresponds to the judgemental equality rule.

One thing to watch out for is that the type-theoretic approach to definitions mimics how the mathematical vernacular uses definitions. However, it is not precisely the same thing as what you describe in your post (what Joel calls "definitional expansion").

There you prove the logical proposition $\exists! y \in A.\; P(y)$, and use that to postulate an object-language term $t$ which is in $A$ and satisfies $P(t)$.

This conjuration of an object from a logical fact is essentially an example of a definite description, or the principle of unique choice. This is an extremely powerful operation, and off-the-shelf dependent type theory was not designed to support it because it handled logic differently.

There is a very interesting design landscape here, but for most people the high-order bit is that unique choice is a really useful thing to have if you want your type theory to be the internal language of a topos (which is a pretty good benchmark for "most of mathematics can be formalised in this system").

Improve this answer
$\endgroup$
10
  • 1
    $\begingroup$ Are you saying that one doesn't need to add the axiom because type theory is seen as already having specified all possible types/terms? That would seem to make the type theory situation analogous to what in the first-order logic setting is called the full definitional expansion, where one has added terms for every possible definition--one has closed the language under all possible definitional expansions. In this case, one wouldn't need to "add" any axioms for defined terms, since there is already such a term in the full definitional expansion. $\endgroup$
    – Joel David Hamkins
    Commented Apr 11, 2023 at 16:22
  • 1
    $\begingroup$ I think let-binding is not so much the point. As Joel says, I would argue the point is rather that type theory, unlike set theory, actually has terms that already denote all the objects we can construct, so there is no need for definitional expansion. Let-binding is just introducing an abbreviation for a term that already exists. $\endgroup$
    – Mike Shulman
    Commented Apr 11, 2023 at 16:27
  • 1
    $\begingroup$ It's true that some versions of dependent type theory don't satisfy the axiom of unique choice unless you postulate it. But "modern" type theories (if you'll permit that word) do automatically satisfy it, if they follow homotopy type theory in taking the "propositions" to be the subsingleton types. $\endgroup$
    – Mike Shulman
    Commented Apr 11, 2023 at 16:28
  • 1
    $\begingroup$ @JoelDavidHamkins: if I understand you correctly, you have in mind the introduction of a bunch of constants $c_\phi$ with axioms $\phi(c_\phi)$, one for every formula $\phi(x)$ satisfying $\exists! \phi(x)$. If that's true, then the answer is: that's not an appropriate analogy because it completely obliterates the structure of terms, but type theory thrives on such structure. Let-binding is precisely and only a mechanism for introducing abbreviations. You could add it to ZFC, but it would be useless, since ZFC does not have any term formers, apart from variables. $\endgroup$
    – Andrej Bauer
    Commented Apr 11, 2023 at 17:55
  • 3
    $\begingroup$ @JoelDavidHamkins: One key difference is that in the first-order setting, definitional expansion is a genuine, if minor, change of language and theory the theory, while in type theories with let-binding, you’re always still working within a fixed base theory. Of course since definitional expansions are so strongly equivalent to their original theory, it’s very mathematically inconsequential — but from a foundational point of view, it feels nice to have statements like “we develop mathematics within this fixed theory” a little closer to genuinely true. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Apr 11, 2023 at 20:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .