The constructive tag has no wiki summary.

**1**

vote

**2**answers

468 views

### Axiom of choice and convergence

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 converge?
Thanks in ...

**0**

votes

**1**answer

420 views

### Maximum sum of 3 consecutive numbers in a permutation [closed]

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, 8, 6)$, then $M(P)$ ...

**12**

votes

**8**answers

2k views

### Are there any mathematical objects that exist but have no concrete examples? [closed]

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. The closest example ...

**5**

votes

**4**answers

2k views

### Does constructing non-measurable sets require the axiom of choice?

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 of $\mathbb{R} ...

**5**

votes

**3**answers

727 views

### Are all group monomorphisms regular, constructively?

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 constructive: Let H be a ...

**11**

votes

**7**answers

1k views

### What happens when we print the digits of a real number?

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 intutionistic proof, you ...

**4**

votes

**7**answers

2k views

### Are real numbers countable in constructive mathematics?

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),...\;]$$
$$where\quad a_i ...

**5**

votes

**2**answers

2k views

### Primitive element theorem without building field extensions

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$ is separable over ...

**10**

votes

**8**answers

2k views

### Direct construction of the integers

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

**7**

votes

**2**answers

814 views

### Why do generic polynomials work in reality?

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 by a realization of ...

**7**

votes

**1**answer

622 views

### Some constructive versions of the Continuum Hypothesis are false. Are any true, or open?

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 common anti-classical ...

**6**

votes

**4**answers

724 views

### Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...

**9**

votes

**3**answers

1k views

### Is set-induction relatively consistent?

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 any subset $S\subseteq ...

**9**

votes

**4**answers

2k views

### reduced ⊗ reduced = reduced; what about connected?

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 proof that if $A$ and ...

**18**

votes

**11**answers

2k views

### Are there any good nonconstructive “existential metatheorems”?

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 exists than it is ...

**9**

votes

**3**answers

836 views

### Intuitionistic Lowenheim-Skolem?

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-Vaught test for ...