This is a very natural question, but as it happens one needs some more background to give a natural answer (is my humble opinion). For clarity let me give a summary first indication: As to your ...

The following version of Lagrange's theorem is equivalent to AC: LT+: Let $H$ be a subgroup of the group $G$. Then there is a bijection $k: (G:H)\times H\to G$ such that for each $(\tilde{g},h)\in (...

In BISH the follwoing two statements are equivalent: (i) If $f:[0,1] \to \{y\in\mathbb R\, | \,y>0\}$ is uniformly continuous, then there is $n\in\mathbb N$ such that $\forall x \in [0,1]\ [f(x)&...

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this: Theorem (constructive Brouwer fixed-point theorem) Let $B$ be the closed unit ...

Your question almost answers itself, but this may not be so obvious. So I will try to give a short and clear answer. Regarding 1) of your question: As a mathematician well-schooled in intuitionistic ...

You ask: Has anyone seriously explored what mathematics would look like in the absence of PUC? Actually, I believe I have done so in my PhD thesis modern intuitionistic topology. Don't let the title ...

CSB fails intuitionistically even under the conditions which you describe. This was proved by Van Dalen in A note on spread-cardinals, Compositio Mathematica, tome 20 (1968), p. 21-28. Van Dalen ...

Your question appeals to me in its clarity and relevance. I would love to give a similar clear answer, but as we stand in math and physics I believe that matters are not so clear-cut. As pointed out ...

A course in constructive algebra by Mines, Richman & Ruitenburg, covers the constructive development of discrete fields and their algebraic completion, and even their valuation-metric completion. ...

Being both a professional visual artist and mathematician, I feel obliged to attempt an answer. There are to me very strong similarities, common mechanisms, overlaps, correspondences, between ...

Let $P\subseteq X\times Y$ be sets such that $\forall x\in X\exists y\in Y[(x,y)\in P]$. We wish to derive from (S) the existence of an $f\subseteq P$ such that $\forall x\in X\exists! y\in Y[(x,y)\in ...

In my PhD thesis modern intuitionistic topology in chapter 3 there is a comprehensive treatment of partitions of unity within BISH. In essence the main theorem is that per-enumerable open covers of a ...

The answer is in spirit: yes. One can prove uncountability of the reals without using countable choice by using a modified version of LLPO which I call fLLPO (functional LLPO). Still, fLLPO is also ...

Since the work of Church and Turing (say around 1936), the notion of algorithm is definitely not considered primitive in intuitionism. But Brouwer started intuitionistic mathematics more than 2 ...

In general, finding the smallest integer solution to a system of modular (in)equalities seems to be very hard. To be precise: the question is how to find the smallest $x$ such that e.g. $x\mod{3}\in\{...

Without polishing up on linear algebra, the not very subtle topological answer is yes. Different eigenvalues $\lambda_i$ mean unique solutions (the eigenvectors) on the unit hemisphere, of the kernel ...

[I just started here and do not have enough reputation to comment...so I´m kind of forced to give an answer.] I believe there is a different way to eliminate countable choice in the proof of aIVT (...

For a real function $f$ with continuous derivative $f'$ we have the following identity which should not require any choice to prove: $$ f(x) = f(0) + \int_0^x f'(y)dy \ \ (\mbox{all}\ x\in\mathbb{R}) ...

In answer to what I think to be your question (which isn't very clear to be honest): For $RH$ and $P=NP$ I believe it makes no constructive difference if you use LPO (LLPO) or not. According to Joe ...

An answer in the opposite direction (helpfully meant, for completing the picture): In 'old-fashioned' constructive mathematics, the set $A$ already has an apartness $\#$. Then we have: $x<y\...

${\rm\small\color{#808080}{(1st\ answer, also\ see\ updates\ below):}}$ I think the connective $A⅋B$ is not more constructive than existing connectives. You say that a witness for$A⅋B$ consists of two ...

Because regular paths can be very wild indeed, it seems to me that Andreas' answer in the comments above is in fact the most intuitive definition...! (call two regular paths $p, q$ path-equivalent iff ...

Consider in intuitionistic mathematics the example of $A$ being the unit interval $[0,1]$ with the trivial topology $\{\emptyset,[0,1]\}$. Then $A$ is not $T_0$ and yet $A$ still has the fixed-point ...

Neither 1. nor 2. is provable constructively, in my not so humble opinion. To answer your question completely, let me explain the reason for this which goes back to the fundamental research of Brouwer,...

[Incorrect answer, perhaps mendable, perhaps not, sorry, see my comments below] The answer is yes, the statement is in fact equivalent to AC. AC is equivalent to "every set of pairwise disjoint ...

Second version after incomplete first version, using John's theorem and some remarks thereon by Keith Ball. == The worst case is the triangle (as intuition predicts). A few images would be really ...

Discontinuous functions are perfectly acceptable in constructive mathematics. But BISH (the way of doing constructive math as put forward by Errett Bishop) is actually deficient in its definition of '...

The way I understand it is as follows. The most general formula $ (\neg A \; \to \; B \vee C) \;\; \to \;\; ((\neg A \; \to \; B) \vee (\neg A \; \to \; C)) $ is not derivable in IPC, because it ...

The Cantor-Schröder-Bernstein theorem (CBS) implies excluded middle in intuitionistic mathematics (INT) and in recursive mathematics (RUSS), since CBS is false ($\neg$CBS is a theorem), and ex falso ...