Derek Elkins left SE
  • Member for 6 years
  • Last seen more than 2 years ago
Are category-theory and set-theory on the equal foundational footing?
42 votes

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, ...

View answer
Do we have to prove how parentheses work in the Peano axioms?
Accepted answer
35 votes

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 ...

View answer
Which insights are particularly simple to get through category theory?
Accepted answer
28 votes

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 ...

View answer
What do logicians mean by "type"?
26 votes

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 ...

View answer
Why did mathematicians choose ZFC set theory over Russell's type theory?
Accepted answer
19 votes

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 ...

View answer
Why worry about commutativity but not associativity in The Fundamental Theorem of Arithmetic?
17 votes

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 ...

View answer
Why don't we take clopen maps as morphisms of the category of topological spaces?
Accepted answer
16 votes

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
Forgetting non-isomorphisms: does this category have a name?
Accepted answer
13 votes

It is called the core of $\mathcal C$.

View answer
Why isn't the axiom of extensionality considered a definition of equality?
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\...

View answer
Basic Example of Yoneda Lemma?
Accepted answer
12 votes

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,...

View answer
Obtain magnitude of square-rooted complex number
Accepted answer
12 votes

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}$. ...

View answer
Why, logically, is proof by contradiction valid?
11 votes

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,...

View answer
Why did we settle for ZFC?
Accepted answer
11 votes

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 ...

View answer
Topos theory and higher-order logic
Accepted answer
11 votes

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 ...

View answer
Why does one have to check if axioms are true?
10 votes

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, ...

View answer
What is the difference between Formal Logic and Proofs?
Accepted answer
9 votes

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. ...

View answer
What is the reason we usually don't use formal proofs in mathematics?
Accepted answer
9 votes

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-...

View answer
Purpose of universal property of a product.
Accepted answer
9 votes

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 ...

View answer
Axioms of a Ring and a Simple Example (that confused me)
Accepted answer
9 votes

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 ...

View answer
Simple theorems that are instances of deep mathematics
9 votes

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 ...

View answer
How are sets defined in reverse mathematics?
Accepted answer
8 votes

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 ...

View answer
bivariate Yoneda lemma
Accepted answer
8 votes

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 ...

View answer
Reconciling different definitions of left-exact functor
Accepted answer
8 votes

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 ...

View answer
What are the Laws of Rational Exponents?
8 votes

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,...

View answer
If $F$ is representable, then $G$ is representable? If $G$ is representable, then is $F$ representable?
7 votes

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,...

View answer
Multiple monoidal closed structures on the same category
Accepted answer
7 votes

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 ...

View answer
How is ultrafinitism imprecise?
Accepted answer
7 votes

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 ...

View answer
Why is the principle of explosion accepted in constructive mathematics?
7 votes

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 ...

View answer
Curry-Howard for an imperative programming language?
Accepted answer
7 votes

One (extreme) perspective on Curry-Howard (as a general principle) is that it states that proof theorists and programming language theorists/type theorists are simply using different words for the ...

View answer
How do I know what we already know in a proof when the assumptions we can use are even more complex?
Accepted answer
7 votes

As others have said in the comments, you know what rules and axioms you can use because you are given or choose a particular collection. One of the most common misunderstandings I see is the thought ...

View answer
1
2 3 4 5
22