11
votes
7answers
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
7answers
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
8answers
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
1answer
625 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
4answers
730 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
3answers
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
11answers
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
3answers
838 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 ...