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)
5
questions
2
votes
2
answers
126
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 ...
- 249
4
votes
1
answer
420
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'...
- 329
0
votes
2
answers
241
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 ...
3
votes
2
answers
187
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 ...
- 345
18
votes
2
answers
368
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., ...
- 680