# Questions tagged [foundations]

This tag is for questions about the foundations of mathematics, and the formalization of mathematical concepts in foundational theories (e.g. set theory, category theory, and type theory).

774 questions
80 views

### Why do mathematicians generally write definitions in “declarative” rather than “imperative style?

In programming, we can make the distinction between declarative / functional and procedural / imperative programming. The distinction is not exact, but nevertheless meaningful. One major difference ...
48 views

### Natural examples of “set-theorems” provable in MK but not ZFC and NBG

NBG set theory proves nothing additional about sets relative to ZFC. MK set theory, on the other hand, is stronger, meaning it should prove statements about sets that NBG and ZFC don't. Are there ...
34 views

### Finite axiomatization of second-order NBG

First-order NBG set theory is finitely axiomatizable. The proof of this basically shows that the axiom schemas, in the presence of the other axioms, can be reduced to a finite set of cases, and are ...
73 views

### Definitions in metamathematics

In model theory, the satisfiability relation $\vDash$ between a model $M= (D,f)$ and a set of formulas tells us when a formula $\varphi$ is true or not in the model ("interpretation") $M$. This ...
62 views

### Why is the Axiom of Well-ordered Choice not strong enough to prove Zorn's Lemma?

This is based on this question: How strong is the axiom of well-ordered choice? The "axiom of well-ordered choice" says that any transfinitely-indexed family of sets has a choice function. The ...
171 views

### How strong is the axiom of well-ordered choice?

I sometimes see references to the "Axiom of Well-Ordered Choice," but I'm not sure how strong it is. It states that every well-ordered family of sets has a choice function. By "well-ordered family," ...
87 views

### What is the most expressive logic?

What is the most expressive logic studied in the literature (in terms of expressing properties about a structure in the sense of model theory)? Many people talk about second-order logic, but third-...
81 views

### Is there a notion differentiating $\frac1{\mbox{countable }\infty}$ and $\frac1{\mbox{uncountable }\infty}$?

It is accepted belief $\mbox{countable }\infty$ is not $\mbox{uncountable }\infty$. Is there notion differentiating $\frac1{\mbox{countable }\infty}$ and $\frac1{\mbox{uncountable }\infty}$ (latter ...
75 views

25 views

### Sequence of Number System Construction

After constructing the naturals, why construct integers before rationals? Is there a historical explanation? Couldn't ordered pairs of fractions constructed from the naturals be used to represent ...
67 views

### What is the difference between the logical formula $\alpha$ and expression “$\alpha$ is true”?

What is the difference between the logical formula $\alpha$ and expression "$\alpha$ is true"? I feel that there is a difference between those expressions. I think this difference is the difference ...
41 views

52 views

### Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there. I would be glad if someone can help me with some of the exercises, ...
79 views

146 views

### Principia Mathematica, chapter *117: a false proposition?

I was reading Principia Mathematica of Whitehead and Russell and I have found what I think is a false proposition. The proposition in question is *117.632 click on the link to see the formula and the "...
34 views

### Category theory using 2-sorted logic

Can anyone give some reference text that axiomatizes category theory using first order logic using 2 sorts (if that makes sense)? I have found reference about 1 sorted axiomatization but I also found ...
58 views

### Proving Equivalence Relations, Constructing and Defining Operations on Equivalence Classes

I think I have an intuitive sense of how ordered pairs can function to specify equivalence classes when used in the construction of integers and rationals, for example. I put the cart before the horse,...
47 views

### Definition of < in Construction of Reals

In the section of Spivak's Calculus on the construction of the reals, < is defined: if alpha and beta are real numbers, then a < b means that a is contained in b (that is, every element of a is ...
61 views

### Model for the type-theoretic axiom of choice in Coq.

This is the request for references. It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent. It is also know that there is a double-negation Godel-Gentzen ...
59 views

### Is it possible to prove Regularity with Transfinite Induction only?

Let us assume that we have only statement of transfinite induction. (And maybe some other well-know axioms) My question: "Is it possible to derive from it a regularity axiom as a theorem?". Some of ...
### Formal definition of a functor in $\mathsf{ZFC}$
Let $\mathcal{C}$ and $\mathcal{D}$ be categories. The first thing that comes to mind when considering a definition of a functor between $\mathcal{C}$ and $\mathcal{D}$ in $\mathsf{ZFC}$ is that it ...
### Category of functors $[C,D]$ and Grothendieck universes
A set $U$ is a universe if for any $x \in U$ we have $x \subseteq U$, for any $x,y \in U$ we have $\{x,y\} \in U$, for any $x \in U$ we have $\mathcal{P}(x) \in U$, for any family \$(x_i)...