Foundations of mathematics , proof theory and analogies with internal mechanism of programming language

Question

All of the mathematics that I know are founded on set theory ,i.e., high school mathematics , calculus and real analysis , little of group theory and topology .But I have gotten to know that there are alternate foundations of mathematics (or maybe some branches of mathematics) like category theory,type theory etc . Some sources mention these foundations of mathematics as programming languages of mathematics.

Programming languages differ from each other in their internal mechanism ,i.e. , the way the compiler written for them generates machine code ,the way their compiler allocates memory and some other things like linking .The machine code generation on matching with the simplest code to accomplish a particular operation yields faster performance and similarly the memory management affects the addressing of the variables , their manipulation etc .

As such every language have their own merits and demerits in terms of speed and ease of tasks.

(please read the above paragraph without subjecting it to detailed theoretical and technical scrutiny as this is a very rough and sketchy idea )

Are there any analogous comparisons between these different programming languages of mathematics or foundations of mathematics . What can be analogous to the process of compiling or linking or what can be analogous to memory allocation ? If yes then ,Are there any such instances of proofs which are very hard to do in one foundation of mathematics but are conjured marvelously in an alternate foundation of mathematics and the differences in the difficulty of the proofs being explained in the manner of programming languages ?

Similarly , even without going to other foundations of mathematics , we can see that there are many instances where theorems are proved in many different ways . Like , infinitude of prime numbers , one having proof by contradiction by gauss and the other in the language of topology by Furstenberg (although this one is also a proof by contradiction). A better example might be Fermat's last theorem which is proved in combinatorial way , group theoretic way ,through dynamic systems . And similarly , there is a Fermat's theorem on sum of squares , which has one long proof by Euler to a one sentence proof by Zagier.

In all these instances , we can see that the same process is being accomplished in different languages , some in the languages of topology , some in the languages of group theory, some in the language of dynamic systems etc . Do we have any analogous parameters like memory management of the compiler of the language , by which we can explain why some of these proofs were easier than the other ones or like we can say some settings or languages allowed better expressions or better access to somethings which were difficult in another language .

(There's a heavy chance that this question might be flagged as unclear about what it demands . Basically , I want to know whether there have been instances where proving something turned out to be very easy in one foundation of mathematics but impossibly difficult in another .Can we do an comparison in such cases between these foundations analogous to comparing internal mechanism of programming languages to reason the difference between them in various aspects .In such cases , what parameters or factors can be analogous to factors like memory allocation ,optimized machine code ,etc.)

Answer 1

Things like memory usage and "speed" are not properties of programming languages; they are properties of implementations. The "compiler" is not part of a definition of a programming language. If we wanted to consider the analogue to a programming language implementation, it would be something like automated theorem provers, proof assistants, and, well, programming language implementations. Agda, for example, is presented as a programming language, and Idris is completely intended for programming.

I'm going to focus on proof assistants, since there is no expectation that a practical automated theorem prover can be made for systems that can address "all of mathematics". Freek Wiedijk has an (old) comparison of many proof assistants and page 11 describes some of the aspects that differentiate them. Some of the aspects are similar to aspects that differentiate programming languages, such as size of the libraries. Others are more fundamental such as whether they are based on ZFC or a HOL. In a different paper he focuses on the "complexity" of formalizing various foundational systems Pages 15 and 16 have tables comparing them. That said, this says nothing about how simple these systems are to use, and, as before, it compares systems that can have quite different properties. For example, Martin-Löf type theory does relatively poorly by this metric, but it's the only constructive system capable of supporting "all math" described. So it's the only such system that (directly) has a computational interpretation.

There's a major difference between constructive and non-constructive foundations. Superficially this impacts what you can prove, though, at least for first-order statements, if $P$ is provable classically, then $\neg\neg P$ is provable constructively. However, if you want to constructively prove $P$ it may not be possible, and even when it is possible, it may take much more work. This isn't surprising because a constructive proof provides much more information. For example, a constructive proof of $\forall x:\!X.\exists y:\!Y.P(x,y)$ means providing a program that will take values of type $X$ and produce values of type $Y$ and a concrete proof object for $P(x,y)$. In other words, (some forms of) constructivism requires that if you claim something exists, you can compute it. Classically, you can prove something "exists" that is provably impossible to compute. There are connections between the law of excluded middle and continuations in programming. This suggests a difference in expressiveness a la Felleisen.

Another major dividing line is analogous to that between typed and untyped programming languages. Many set theories look and behave rather like untyped versions of higher order logic. The impact of this is more ambiguous and has some of the same dynamics as in programming languages. For example, most type theories require you to explicitly inject $A$ into $A+B$ (the "disjoint union" of $A$ and $B$). This makes sense because the situation really is ambiguous in e.g. the $A+A$ case, but it can be tedious and type theories usually don't have a primitive notion of $A\cup B$. On the other hand, much of mathematics that is nominally operating in a set theory tends to make distinctions that align well with types. Distinctions that are automatic in type theory may require explicit encodings in set theory. For example, $\{(x,x^2)\mid x\in\mathbb R\}$ is a function in set theory, but whether it's a function $\mathbb R \to \mathbb R$ or $\mathbb R \to \mathbb{R}^+$ or $\mathbb R \to \mathbb C$ is not part of the information contained in its definition and so we must explicitly add in the codomain when it matters as in the category of sets.

There isn't a comparable "language" of group theory, topology, dynamical systems (or at best they are akin to embedded domain specific languages). These would be more akin to libraries. While there is, say, a first-order theory of groups, most results in group theory are not results in that theory but rather results about that theory. For example, $\forall n\in\mathbb{N}.(ab)^n = a^nb^n$ is not a formula (let alone theorem) of the first-order theory of commutative groups, but it is a meta-theorem about the first-order theory of commutative groups. (It's usually presented, though, as a theorem about the class of models of the theory of commutative groups.) Group theory nominally happens in ZF(C) for most mathematicians, though in practice group theorists are working at a level where many foundations would work with little or no changes.

Differences in proofs are very similar to differences in programs. They may reflect the libraries available, the knowledge and skill of the implementer, the goals of the implementer, and the perspective taken as well as the language used. Zagier's proof isn't really leveraging an advance in the language or even existing results though it's explicitly inspired by proof techniques from other areas of mathematics and is a refinement of work specifically done on this problem. One might also want an algorithm (better than brute force enumeration) to produce the $m$ and $n$ such that $p = m^2 + n^2$ which Zagier's result doesn't even implicitly provide.