I think questions like these are often asked by people who don't have a clear/coherent idea of what foundations are and what purpose they serve. This isn't meant as some kind of insult. I think many, ...

In formal language theory (most relevantly, context-free languages), there is the notion of an abstract syntax tree. A decent chunk of formal language theory is figuring out how to turns flat, linear ...

In my opinion, what's "really happening" with category theory is that it is the model theory of type theory. On the type theory Wikipedia page just linked John Lane Bell is quoted as saying "Roughly ...

tl;dr Types only have meaning within type systems. There is no stand-alone definition of "type" except vague statements like "types classify terms". The notion of type in programming languages and ...

I'm going to answer your title question but not the two questions in the body. As the comments correctly point out, doing so well could fill a book. That said, I think there are a few technical ...

To provide a new answer to the new question (as opposed to all the merged in answers to a very old question): there is no inherent reason. Presumably it is mostly an artifact of the fact that we can ...

Well, the obvious reason is that such a definition would lack the properties of continuous maps that we'd expect. For example, for the Sierpiński space consisting of $\{\bot,\top\}$ with open sets $\{... View answer Accepted answer 13 votes It is called the core of$\mathcal C$. View answer Accepted answer 12 votes First-order logic can be defined with or without equality. If you are working in a first-order logic with equality, which is the typical case, then stating that$X = Y \iff \forall x.x\in X\...

Computer scientists do use quite a few algebraic structures, they are just slightly different from the ones mathematicians usually focus on. Computer scientists tend to care about monoids, semigroups,...

If you convert the number to the complex exponential form, the solution is easy. Let $s = \alpha + \beta i = r e^{\theta i}$, then $z = s^{-\frac{1}{2}} = r^{-\frac{1}{2}} e^{-\frac{\theta}{2}i}$. ...

Many of the issues I described here are on display in this Q&A. First, let's be clear about what we're talking about. There are two rules that are often called "proof by contradiction". The first,...

I'll take a swing at answering the question that I think you are trying to ask. I'll formulate it as follows: If foundations are important as the name suggests and the so-called "foundational ...

Before focusing on the specific question, I'd like to provide some context. First, every (non-trivial) topos has a Boolean subtopos. This is essentially what you say, and it roughly corresponds to ...

There are axioms and then there axioms. Most of the time mathematicians use the word "axiom" they mean it in a definitional sense. Instead of "An equality is a relation satisfying the reflexivity, ...

The distinction the author is making is between formal proofs and informal proofs. Most of mathematics is done informally. Informal proofs are just persuasive arguments written in natural language. ...

tl;dr There is little reason to make paper-and-pencil formal proofs other than learning about formal logic. Machine-checked proofs take less effort to produce and are more valuable than paper-and-...

It sounds like the way it was presented makes it seem tautological. Let's put it slightly differently. Any topological space $Z$ equipped with maps $p:Z\to X$ and $q:Z\to Y$ has the universal ...

The elements of $RG$ are linear combinations of elements of $G$ with coefficients in $\mathbb Z$. More compactly, this is called $\mathbb Z$-linear combinations of elements of $G$. The construction as ...

Multiplication of integers. This takes distributivity as discussed in Ethan Bolker's example in a slightly different direction. I'm pretty sure this idea is in Mathematics Made Difficult, which ...

The answer is in the name of the book. The system described is equivalent to a particular (monadic) second-order theory using Henkin semantics. Instead of talking about "sets", Simpson could have ...

Show that $\mathsf{Nat}(\mathsf{Hom}(-_1,X)\times\mathsf{Hom}(A,-_2),P)\cong P(A,X)$ where $P:\mathcal C^{op}\times\mathcal C\to\mathbf{Set}$. You can prove this by currying and applying each ...

The first thing to be clear about is the latter two statements are statements about additive functors between Abelian categories. An arbitrary functor that satisfies those stated properties is not ...

The issue is that $a^{\frac{1}{n}}$ is multivalued. You could arguably simplify the first calculation into $1 = \sqrt{1} = -1$. Taking different branch cuts is how the "paradox" arises. Essentially,...

Write $K:\mathcal D\to\mathcal C$, for the "inverse" of $H$, i.e. $HK\cong Id_\mathcal D$ and $KH\cong Id_\mathcal C$. Now we can note, unsurprisingly, that your questions are symmetric. If one holds,...

Yes. An example is the category of presheaves over a monoidal category. The category of presheaves for any (small) category is cartesian closed. If that small category has a monoidal structure, then ...

It is simply that there is no formal system that is widely accepted as representing (a least common denominator of) ultrafinitist ideas. For constructivism, we have things like intuitionistic ...

In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For ...