Skip to main content

Questions tagged [constructive-mathematics]

Broadly speaking, constructive mathematics is mathematics done without the principle of excluded middle, or other principles, such as the full axiom of choice, that imply it, hence without “non-constructive” methods of formal proof, such as proof by contradiction. This is in contrast to classical mathematics, where such principles are taken to hold. (from nLab)

Filter by
Sorted by
Tagged with
2 votes
2 answers
122 views

Bijections on Coq

In the ssr.ssrfun library we have the following definition: Variant bijective : Prop := Bijective g of cancel f g & cancel g f. At first glance it was what I ...
Bruno's user avatar
  • 227
4 votes
1 answer
416 views

Does "unique mere existence" imply "existence"?

Hopefully this question fits in well here. I'm hoping that more people who know the answer will see it here than on somwehere like mse, but please let me know if you'd rather I move it there! Say you'...
Chris Grossack's user avatar
0 votes
2 answers
239 views

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

My understanding is that Stephen Wolfram's concept of a multiway system begins with certain rules and then generates all possible combinations of those rules. There are many distinct mathematical ...
Julius Hamilton's user avatar
3 votes
2 answers
182 views

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

I don't think a particular choice of such type theory matters much. Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types. Reals is supposed to be a Set (in HoTT ...
Russoul's user avatar
  • 345
18 votes
2 answers
354 views

Is there computational interpretation for countable choice?

I've wondered how a type theory/proof assistant could manage to add countable choice (or its dependent choice version) as something primitive as well as to keep the computational properties, e.g., ...
KANG Rongji's user avatar