Tag Info

Hot answers tagged constructive-mathematics

Accepted

Yet another constructive (Coq) proof that nat -> nat -> nat is not bijective. How to explain it to myself?

First, let me say that "constructive" does not imply "all maps are Turing computable". It means “no excluded middle and axiom of choice were used“. In constructive mathematics the ...
• 29.4k
Accepted

Law of the Excluded Middle in complexity theory

There are several other non-constructive arguments that work along similar Karp-Lipton-esque lines, such as Santhanam's proof (STOC 2009) that $PromiseMA$ is not in $SIZE(n^k)$ for some $k$, and ...
• 27.5k
Accepted

• 29.4k

Can you define recursive predicates in 2nd order intuitionistic logic?

$\let\eq\leftrightarrow$Based on the comments, I’m interpreting the argument of $\psi$ as a “nullary predicate”. You can define $I$ by the formulas \begin{align*} I(n)&\iff\exists W\,((0\in W\eq\...
• 18.2k

Is just one W-type enough for formalizing mathematics?

We certainly do not need very many $W$-types. If we also have universes, we only need one $W$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no ...
• 29.4k