## 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....

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 ...

Community wiki

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 ...

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 ...

Top 50 recent answers are included

#### Related Tags

constructive-mathematics × 293lo.logic × 152

set-theory × 37

topos-theory × 37

reference-request × 31

ct.category-theory × 26

real-analysis × 22

computability-theory × 21

intuitionism × 20

ac.commutative-algebra × 18

foundations × 18

type-theory × 18

proof-theory × 17

gn.general-topology × 15

reverse-math × 14

locales × 14

ag.algebraic-geometry × 11

model-theory × 11

axiom-of-choice × 10

mathematical-philosophy × 10

homotopy-type-theory × 9

realizability × 8

ra.rings-and-algebras × 7

co.combinatorics × 6

fa.functional-analysis × 6