Franka Waaldijk
  • Member for 5 years, 2 months
  • Last seen more than a week ago
Contrasting theorems in classical logic and constructivism
Accepted answer
12 votes

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

View answer
Is Lagrange's Theorem equivalent to AC?
11 votes

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

View answer
BISH: If a function is pointwise positive, is its infimum positive?
Accepted answer
10 votes

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

View answer
Does the Brouwer fixed point theorem admit a constructive proof?
10 votes

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

View answer
Constructivist defininition of linear subspaces of $\mathbb{Q}^n$?
Accepted answer
10 votes

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

View answer
Mathematics without the principle of unique choice
7 votes

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

View answer
How much of the Cantor-Schröder-Bernstein theorem is constructively recoverable if the injections have retractions and decidable images?
Accepted answer
6 votes

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

View answer
Is there any physical or computational justification for non-constructive axioms such as AC or excluded middle?
6 votes

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

View answer
Constructive proof of a rational version of Perron-Frobenius?
6 votes

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

View answer
Mathematical theory of aesthetics
6 votes

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

View answer
Choice sets and the axiom of choice
Accepted answer
6 votes

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

View answer
Partitions of unity in constructive mathematics
Accepted answer
5 votes

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

View answer
Uncountability of the real numbers from LLPO without countable choice
4 votes

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

View answer
Why is the notion of algorithm a primitive one in Brouwer's intuitionism?
Accepted answer
4 votes

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

View answer
Question: How to find the smallest value $x$ satisfying the equation: $x^2 = a \pmod c$ (known is $a$ and $c$, $c$ is not the prime)?
3 votes

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

View answer
Matrix diagonalization and eigenvector computation constructively
3 votes

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

View answer
Approximate intermediate value theorem in pure constructive mathematics
3 votes

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

View answer
The constancy principle in choiceless constructive foundations
2 votes

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

View answer
On provability of false statements in constructive mathematics
2 votes

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

View answer
Strict and non-strict orderings
2 votes

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

View answer
Adding nonconstructive disjunction to intuitionistic logic
2 votes

${\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 ...

View answer
Topology: what defines (non-trivial) paths as being the same trace (curve)?
1 votes

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

View answer
Fixed-point property and $T_0$ separation property
Accepted answer
1 votes

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

View answer
Constructive proof of existence of non-separable normed space
1 votes

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

View answer
Minimal covering sets in families of sets intersecting in at most $1$ point
1 votes

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

View answer
Maximin diameter of a transformed convex figure
1 votes

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

View answer
Are all functions in Bishop's constructive mathematics continuous?
1 votes

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

View answer
Admissibility of Harrop's rule, computationally
1 votes

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

View answer
How strong is Cantor-Bernstein-Schröder?
0 votes

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

View answer