# Tagged Questions

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

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

**1**answer

619 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

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

**18**

votes

**11**answers

1k 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

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