Hi fellows, I was wondering. Is the axiom of choice used to show that $\mathbb{R}$ is complete? If yes, is there a way to construct monotonic bounded sequences that do not converg …

I am curious as to whether there exists a mathematical object in any field that can be proven to exist but has no concrete examples? I.e., something completely non-constructive. …

Given that $X = \{0, 1, 2, ..., 7, 8, 9\}$, and $P$ is a permutation on $X$. Let $M(P)$ be the maximum sum of 3 consecutive elements. For example, if $P = (0, 2, 4, 1, 5, 7, 9, 3, …

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exist …

Several questions actually. All rings and algebras are supposed to be commutative and with $1$ here. (1) Let $k$ be a field, and let $A$ and $B$ be two $k$-algebras. I need a pro …

Here are two well known facts, which put together leave me confused. First, it's well known that intuitionistic logic is the logic of constructive mathematics. From every intutio …

Is there a direct construction of the integers which does not involve taking any quotients? I am of course aware of the usual construction. I am also aware of the nice axiomatic …

The classic example of a non-measurable set is described by wikipedia. However, this particular construction is reliant on the axiom of choice; in order to choose representatives o …

We are talking about ordinary reals in constructive mathematics. Let represent each real number by infinite converging series: $$r = [\;(a_0,b_0),(a_1,b_1),...,(a_i,b_i),...\;]$$ …

Is there a version of the Löwenheim-Skolem theorem in intuitionistic logic? I'm particularly interested in the "downward" form. The standard proof I know uses the Tarski-Vau …

Is there are nice way to prove the primitive element theorem without using field extensions? The primitive element theorem says that if $x$ and $y$ are algebraic over $F$ and $y$ …

By "constructive" I mean something that would go through in CZF for example. [added Oct 6] A sketch of a standard proof (such as referenced in comment below), which is almost cons …

I understand that a generic $G$-polynomial $f(t_1,...,t_n)[X]$ over field $k$ has Galois group $G$ over $k(t_1,...,t_n)$. And basically any $G$ extension of $k$ should be generated …

One way to state the axiom of foundation is that the $\in$ relation on any transitive set is well-founded in the following sense: A relation $(X,\prec)$ is well-founded if for an …

Background In constructive set theory (say based on CZF) there are inequivalent ways of stating the continuum hypothesis. Some of them are easily if not trivially refutable with c …