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
18 votes
2 answers

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
3 votes
2 answers

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
0 votes
2 answers

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 H.'s user avatar