Skip to main content
8 votes
Accepted

Does "unique mere existence" imply "existence"?

If $\varphi$ is proposition-valued and has at most one witness, then $\sum_{x:X}\varphi(x)$ is a proposition. We can see this because, given two inhabitants of $\sum_{x:X}\varphi(x)$, they have the ...
James Wood's user avatar
  • 1,053
5 votes

Is there computational interpretation for countable choice?

In realizability theory another computational interpretation of countable choice is a procedure for computing canonical forms of natural numbers. I explained this in detail in this answer to a similar ...
Andrej Bauer's user avatar
  • 9,593
5 votes

Is there computational interpretation for countable choice?

It really depends on what you call countable choice, and in particular the semantics of your Prop fragment. Assuming you phrase CC as ...
Pierre-Marie Pédrot's user avatar
5 votes
Accepted

Bijections on Coq

This is a case of abstract vs. concrete existence. First-order logic only supports the former, pure Martin-Löf type theory only the later, but mathematicians use both (and don't know it because they'...
Andrej Bauer's user avatar
  • 9,593
4 votes

Is there a multiway system which is equivalent to taking ZFC as axioms?

Wolfram's multi-way systems are expressive enough to accommodate generation of any computably enumerable set. Thus they are powerful enough to generate all theorems of a computably enumerable formal ...
Andrej Bauer's user avatar
  • 9,593
2 votes
Accepted

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

Here are some formalizations of constructive reals that you can build on, roughly by decreasing level of "state-of-the-art". Some come equipped with a considerable amount of real analysis, ...
Andrej Bauer's user avatar
  • 9,593
2 votes

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

First off, you need to distinguish between constructing the reals and defining the reals. Your question asks about the former, but: Classically we almost never simply construct two versions of reals ...
Trebor's user avatar
  • 4,015
1 vote

Bijections on Coq

As Naïm Favier mentioned, you need an axiom in general. If you are willing to accept an axiom, constructive_definite_description suffices. ...
djao's user avatar
  • 484
1 vote

Is there a multiway system which is equivalent to taking ZFC as axioms?

For a long time I have been interested in the idea of computationally enumerating every possible expression of a formal theory. Who hasn't! :) As one with a background in linguistics, I am sure you ...
Julio Di Egidio - inactive's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible