Questions tagged [constructive-mathematics]

Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.

Filter by
Sorted by
Tagged with
1
vote
1answer
196 views
+50

Collection of proper classes with in CZF

In Aczel's Constructive Set Theory (CZF), no non-degenerate complete lattice can be proved to be a set. There are hallmark examples of complete lattices that are proper classes in CZF, including the ...
2
votes
1answer
167 views

Alternative definitions of étale and formally unramified in Wraith

I have stumbled upon the following definitions in a paper by Gavin Wraith. Definition 1. Say a ring morphism $A\overset \varphi \to B$ is formally unramified if every $b\in B$ admits: $b_0\in B$ ...
8
votes
1answer
407 views

What is the status of Jordan's theorem in constructive mathematics in the language of locales?

By constructive mathematics in this matter we mean intuitionistic ZF (*). In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$,...
13
votes
1answer
745 views

How to express in categorical language that in some toposes not all complex numbers have square roots

I'm trying to improve my ability to translate constructive logic into the category theoretical language of topos theory. So far, my understanding of constructive logic has been rather naive. I know ...
5
votes
1answer
127 views

Possible values of "Kripke rank" for formulae in IPL

Fix a (countable) set $\mathcal{P}$ of atomic propositional variables. Recall a Kripke model $\mathcal{K}$ for intuitionistic propositional logic (IPL) consists of: A preorder $(W,\leq)$ For each $w \...
4
votes
1answer
209 views

Is there a correspondence between principles of omniscience and computability classes?

My question will be speculative and therefore a little vague. I wonder if attempts have been made to define a correspondence between, on the one hand, limited principles of omniscience that can be ...
3
votes
2answers
230 views

Constructive lattice completion

The Dedekind–MacNeille Completion is the generalized way of completing an arbitrary lattice $L$. We will call $C$ the Dedekind–MacNeille completion of $L$ (I will not go into the details of the ...
5
votes
4answers
532 views

What does overtness mean for metric spaces?

Original question: For compact metric spaces, plenty of subtly different definitions converge to the same concept. Overtness can be viewed as a property dual to compactness. So is there a similar ...
3
votes
1answer
205 views

Subset Collection axiom

In Constructive Set Theory (CZF) the Power Set axiom is replaced with the Subset Collection axiom which I will state here: $$ \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \...
8
votes
1answer
211 views

Can you constructively prove a univariate polynomial algebra over a Jacobson ring is itself Jacobson?

Recall the Jacobson radical of a commutative ring $\mathrm J(A)=\lbrace a\in A\mid \forall b\in A:1-ba\in A^\times\rbrace$. The Jacobson radical of a quotient by an ideal $I\vartriangleleft A$ is ...
3
votes
0answers
167 views

Is intuitionistic predicate logic (semantically) complete or incomplete?

According to Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (https://archive.org/details/constructivismin0002troe/page/718/mode/2up) it is proven in an intuitionisitc ...
17
votes
4answers
2k views

What is neutral constructive mathematics

In Mike Shulman's answer to Initiation to constructive mathematics, he discusses how "neutral constructive mathematics" is the fashionable topic in constructive mathematics. When ...
4
votes
1answer
357 views

How do working constructivists get by with out the zero product property?

It is stated by Douglas Bridges in Constructive mathematics: a foundation for computable analysis that the following property, which I will call the zero product property: If $x,y \in \mathbb{R}$ and $...
2
votes
1answer
124 views

LLPO as constructivity/computability for dense subsets

LLPO is the statement $\forall x \in \mathbb R. x \leq 0 \vee x \geq 0.$ The statement should be understood as a fragment of the Law of Excluded Middle, rather than a statement about the ordering of ...
3
votes
1answer
315 views

What is known about constructively irrational numbers?

Intuitively, a constructively irrational number is one for which we can effectively separate it from any rational number in terms of the latter's denominator. More formally, a constructively ...
5
votes
0answers
110 views

Within pointless topology inside of choiceless constructivism, prove that division is possible

In Frank Waaldijk's paper on the foundations of constructive analysis, Waaldijk shows that various definitions of "continuous function" for functions of the form $f: \mathbb R \to \mathbb R$ ...
11
votes
1answer
478 views

Are the “topologies” arising from constructive type theories with quotients actually condensed sets?

This is the second in a pair of questions. For the other see Are representations in computable analysis the equivalent to countably-generated condensed sets?. Dustin Clausen and Peter Scholze have a ...
2
votes
0answers
101 views

In a constructive order/lattice theory are the arbitrary join and the weak suprema the same?

For a poset $X$ we define an upperbound $w \in X$ of a subset $S \subseteq X$ to be a weak-supremum if $(\forall a \in S (a \leq b)) \implies w \leq b$. While a supremum is defined more carefully (in ...
6
votes
1answer
338 views

Realizability for constructive Zermelo-Fraenkel set theory

$ \def \CZF {\mathbf {CZF}} \def \IZF {\mathbf {IZF}} \def \A {\mathcal A} \def \then {\mathrel \rightarrow} \def \r {\mathrel \Vdash} \DeclareMathOperator \V V $ In "Realizability for ...
0
votes
1answer
277 views

What's the condition to prove the equicontinuity?

Let $K: I\times I\rightarrow \mathbb{R}$ be a scalar kernel, where $I=[0,1]$, and $a: I \rightarrow (0,+\infty)$ an $L^1(I)$ function. For $t_1,t_2\in I$, define $$I_{t_1,t_2}=\int_{0}^{1} \left |\...
8
votes
1answer
445 views

Exposition of concrete constructions

I am frequently interested to find less technical proofs of results which already appear in the literature, at least in some special cases of these results. Sometimes a published proof shows that an ...
6
votes
0answers
316 views

Proof of Tennenbaum's Theorem by McCarty

Tennenbaum's Theorem in its usual form states that for any countable non-standard model $M$ of PA there is no way to code the elements of $M$ as natural numbers such that either the addition or ...
12
votes
1answer
675 views

So after all, what is this thing about topos theory and non-binary truth?

Disclaimer. The question below is necessarily vague. I understand neither the subject matter topos theory nor the object about which my question is (the construction of a fractional / non-binary / ...
8
votes
1answer
312 views

A weak form of countable choice

Let $\Omega$ be the set/type of truth values. We're using constructive logic. Define $AC_{0, 0} = \forall P : \mathbb{N}^2 \to \Omega, (\forall n \in \mathbb{N}, \exists m \in \mathbb{N}, P(n, m)) \to ...
5
votes
0answers
149 views

What is known about these "explicitly represented" spaces?

Apologies if this is too low-level. A related question that I asked on the Math Stack Exchange got no answers after a year, so I thought it might be better to ask this one here. The standard approach ...
10
votes
3answers
1k views

Initiation to constructive mathematics

What are some good introductory references to constructive mathematics for non-specialist mathematicians? I would like to learn more about constructive mathematics, just to improve my general ...
40
votes
3answers
4k views

How to rewrite mathematics constructively?

Many mathematical subfields often use the axiom of choice and proofs by contradiction. I heard from people supporting constructive mathematics that often one can rewrite the definitions and theorems ...
3
votes
0answers
170 views

Is there a non-constructive dependent type theory?

If I understand correctly constructivism is not the only difference between intensional Martin-Löf type theory and a first-order set theory (e.g. ZFC). Can we drop constructivism and yet have a ...
8
votes
1answer
314 views

Reference request: proof-theoretic strength of $\mathsf{KP}$ with recursively large ordinals and $\mathsf{CZF}$ with large set axioms

Large set axioms are notions corresponding to large cardinals on constructive set theories like $\mathsf{IZF}$ or $\mathsf{CZF}$. The notion of inaccessible sets, Mahlo sets, and 2-strong sets ...
6
votes
1answer
515 views

Do we have an algorithm for comparing $e^e$ with rationals?

Do we have an algorithm for comparing $e^e$ with rationals, with a known time to convergence? In a non-constructive sense, there obviously is an algorithm. If $e^e$ is some rational $q_0$, then we ...
1
vote
0answers
58 views

Approximation Rates for Multivariate Taylor Series

Let $k,n,m$ be positive integers and suppose that $f$ is $C^{k}(\mathbb{R}^n,\mathbb{R}^m)$ functions. For any given $\epsilon>0$ and $x_0\in \mathbb{R}^n$, are there known sharp approximation ...
1
vote
0answers
70 views

Constructive way to optimally cover a compact subset of Euclidean space

Let, $(X,d)$ be a simply connected compact subset of $\mathbb{R}^d$ with non-empty interiorn, let $d$ denote the Euclidean metric, and let $\varepsilon>0$. Is there a way to iteratively select ...
7
votes
1answer
191 views

Functions on Stone spaces as "enveloping algebra" of Boolean algebra

I'm looking for references for the following closely related facts: Given a Boolean algebra $B$, I denote by $\mathbb{Z}[B]$ the free ring generated by symbols $e_b$ such that $e_b e_{b'} = e_{b \cap ...
10
votes
1answer
458 views

Does $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$ imply excluded middle?

Suppose that we take constructive set theory and add the axiom $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$. Does this imply excluded middle, or are there still some formulas $\varphi$ for ...
1
vote
0answers
100 views

Algorithm/iterative procedure for constructing hypercyclic vectors?

Let $B$ be a separable Banach space and let $L:B\rightarrow B$ be a hypercyclic operator; here I use the definition of hypercyclicity given implicitly by Birkhoff's Transitivity Theorem: continuous ...
6
votes
1answer
212 views

When do algebraic closures exist constructively?

The field of algebraic numbers exists constructively, since we can represent a number by an irreducible polynomial plus an estimate in rational coordinates that separates it from any other root. More ...
2
votes
1answer
122 views

Constructivity of two problems on a standard simplex?

Maximizing a hyperplane $\sum_i a_ix_i$ where $a_i\in\mathbb R$ and each $a_i$ are fixed and non-negative and $x_i$ are variables over a standard simplex $\sum_i x_i\leq 1$ with $0\leq x_i$ always ...
7
votes
1answer
232 views

Constructive definition of noncommutative rational functions (aka free skew fields)

The question Let $F$ be a field. (I am fine with assuming $F=\mathbb{Q}$, but I suspect that a "right" answer will be independent of $F$.) Let $k$ be a nonnegative integer. Question. Is ...
3
votes
0answers
150 views

Constructive proof of the approximate Brouwer's Fixed Point Theorem for $\Delta^n$

The approximate Brouwer Fixed Point Theorem (aBFPT) for the standard $n$-simplex is: Let $f$ be a uniformly continuous function from $\Delta^n$ into itself. Then for each $\varepsilon>0$ there ...
1
vote
0answers
141 views

Is there difference in notion of measurability in classical versus constructive?

Are there notions of measure and examples of sets measurable in that measure in classical logic but not in constructive logic (I think there cannot be counterexamples in other direction)? Are there ...
11
votes
0answers
453 views

Does Merkurjev's argument help Voevodsky's program?

In the talk Unimath - its present and its future, July 10, 2017. Video and slides of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. (abstract) Voevodsky mentioned that he was ...
3
votes
0answers
65 views

Embedding abelian categories into abelian sheaves

The Yoneda functor from an abelian category into sheaves of abelian groups is shown to be exact in The Stacks Project, Lemma 19.9.2. I like this proof because it is constructive and it doesn't use ...
11
votes
0answers
345 views

Isomorphic free groups have bijective generating sets

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement: $F(X) \cong F(Y)$ if and only if $|X|=|Y|$. The proofs (that I have seen) consist of turning the group ...
2
votes
2answers
844 views

Monotonic and bounded sequences throughout mathematics [closed]

When I refer to the Monotone Convergence Theorem below, I refer to the very simple claim that if a non-decreasing sequence has an upper bound then it converges. I don't refer to the claim from Measure ...
3
votes
1answer
368 views

From a constructive perspective, what are the ordinal numbers?

From a constructive and computational perspective, what are the ordinal numbers? On the one hand, it seems you can represent ordinal numbers symbolically using something like Cantor Normal Form ...
13
votes
1answer
417 views

History of well founded relations

I have changed the title in the hope of attracting the attention of someone who knows about the history of set theory as well as intuitionistic logic: Who was the first to state the definition of ...
11
votes
3answers
638 views

The constancy principle in choiceless constructive foundations

Prove, without any Choice principles or Excluded Middle, that if a pointwise differentiable function has derivative $0$ everywhere, then it is constant. The function in this case maps $\mathbb R$ to $\...
9
votes
1answer
456 views

Toposes in which countable choice is true but dependent choice isn't

I'd like examples of toposes in which Countable Choice is true but Dependent Choice isn't. I'd prefer examples without Excluded Middle. It's hard to find a natural example.
13
votes
2answers
932 views

Contrasting theorems in classical logic and constructivism

Is it possible there are examples of where classical logic proves a theorem that provably is false within constructivism? Is so what are some examples? What are some examples of most contrasting ...
1
vote
1answer
125 views

Markov's principle from constant domain logic

I am looking for a proof of and/or a reference for the result that Markov's principle can be proved in the framework of constant domain logic. By constant domain logic, I mean intuitionistic logic ...