New answers tagged constructive-mathematics
1
vote
A new and subtle order-theoretic fixed point theorem
Re-formulating an order-theoretic idea for categories can often clarify how it works,
by making it proof relevant (as Type Theorists would say), as well as
linking to older studies of initial algebras....
- 8,248
0
votes
Tarski-Seidenberg for strict inequalities and bounded quantification
EDIT(n+1):
I didn't see how this can work for universal quantifiers, as
$(\forall y)(xy\neq 1)$ is equivalent to $(x=0)$.
Certainly, one must also impose $y_0\leq y\leq y_1$, for some $y_0<y_1$, to ...
19
votes
Consistency strength of HoTT
The proof theoretic strength of HoTT was studied by Rathjen in Proof Theory of Constructive Systems: Inductive Types and Univalence. The paper surveys a number of long known results on the relative ...
- 4,211
11
votes
Accepted
Decimal expansion definition of real numbers, constructively
We have a well defined map from decimal expansions to Cauchy real numbers, so by taking the image factorisation of this map, we can always quotient out the set of decimal expansions to get a subobject ...
- 4,211
Top 50 recent answers are included