29 problems

Dalen's conjecture. The function $f$ has an exact fixed point; that is, there exists $x\in S$ such that $x=f(x)$.

The passage discusses a proposed choice principle for the library: a function associates to each predicate another predicate such that, whenever the first predicate is nonempty, th…

Let $S_n$ be a syntactic fractal space with a family of definable sets $cF_n$, and let $\nu_n$ and $\mu_n$ be $S_n$-measures. Write $\nu_n \ll \mu_n$ when $\mu_n(A)=0$ implies…

Cauchy-completeness separation conjecture. 1. There exists an elementary topos in which $\mathbb{R}_C\neq\mathbb{R}_E$; equivalently, there exists an elementary topos in which…

Let $\mathsf{WFT}_{\mathit{pred}}$ be the intuitionistically provable variant of the weak finite tree theorem in which infinite paths are represented by a predicate, and let…

Let $\mathsf{DDNS}_{\mathcal{C}}$ denote the disjunctive double-negation scheme for the class $\mathcal{C}$, and let $\mathsf{DNS}^{\forall}_{\mathcal{C}}$ denote the corresponding…

Well-founded-materialization conjecture. The theory

Disjunction-property conjecture. All reasonable constructive set theories possess the disjunction property.

Representation conjecture. The three modified axioms should imply a corresponding representation theorem for variable lotteries.

Let $D_{0,1}$ be the unit ball and let $\partial D_{0,1}$ be its boundary. For $p\geq1$, let $\mathbf{h}^{p}$ denote the Hardy space of harmonic functions on $D_{0,1}$. The classic…

Sharpness and maximality conjecture. The strongly maximal elements of $\mathcal R$ coincide with the elements that are both sharp and maximal only if a constructive taboo holds.

Kleene's conjecture. In 1943, Kleene conjectured that whenever $\forall x.$

Strongly maximal elements conjecture. The strongly maximal elements of $\mathcal R$ coincide with the elements that are both sharp and maximal only if a constructive taboo holds.

A social welfare order is an ordering of infinite utility streams, and the Anonymity and Weak Pareto axioms require, respectively, invariance under permutations of individuals and…

The discussion concerns constructive measure theory, measurable locales, forcing, and categorical frameworks such as sheaves, toposes, and type theory, in which randomness can be f…

Propositional-canonicity conjecture. The context $(x:\mathbf{LLPO}_\vee)$ has propositional canonicity for $\mathbb{N}$ over type theory with bracket types, as studied by Awodey an…

Let $\mathrm{BKS}^{-}$ and $\mathrm{BKS}^{+}$ denote the negative and positive Brouwer-Kripke schemas, respectively, in a classically defined model for a formal intuitionistic theo…

Let a topos with natural number object be a topos equipped with a natural number object, and let a monic polynomial with reductions be as considered in the paper. Initial-algebra f…

A monic polynomial with reductions is the polynomial-with-reductions structure considered in the paper whose underlying polynomial map is monic. Choice-necessity conjecture. In gen…

A W-pretopos is a category with the structural properties implicit in the paper, and WISC denotes the weak internal axiom of choice used there. Free algebra existence conjecture. F…

Classical Nonstandard Analysis uses the predicate “$x$ is standard” to distinguish standard from nonstandard objects. A proof can be viewed as consisting of an initial part using T…

Carleson's theorem concerns the almost-everywhere convergence of Fourier series: for suitable $f\in L^p[-\pi,\pi]$, the partial sums $\{S_N(f)\}_{N\in\mathbb{N}}$ converge almost e…

Let $\mathbb{R}$ denote the Dedekind real numbers. The analytic Markov principle is the statement … Assume the axioms referred to in the source as … . Analytic Markov principle con…

A simplex is the localic analogue of the interval, with its vertices as distinguished points, and infinite sequences can be used to represent points through successive subdivisions…

Conjecture on the inadequacy of bare axiomatic theories. The studied cases are not exceptional, so the received notion of axiomatic theory as a bare system of propositions cannot b…