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)
3
questions
0
votes
2
answers
191
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 ...
- 175
3
votes
2
answers
134
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
17
votes
2
answers
288
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., ...
- 660