Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [constructive-mathematics]

In constructivism, an existence proof is not accepted, unless the object in question is constructed. Also, the law of excluded middle is typically not accepted as an axiom.

1
vote
0answers
21 views

Noetherian sets without LEM

A noetherian ring can be defined as a ring in which any nonempty set of ideals has a maximal element. They're pretty nice objects. One can obviously generalize this to a bunch of different algebraic ...
0
votes
0answers
32 views

Why is the calculus of constructions called that way, and what is a “construction” in CoC?

I'm reading about the calculus of construction Nederpelt & Geuvers' book "Type theory and formal proof". I can see that CoC allows us to extend the curry howard isomorphism from simply typed ...
0
votes
1answer
41 views

Is there a procedure to calculate the multiplicative inverse in a quotient by a maximal ideal?

An elementary result in ring theory is that if $R$ is a commutative ring with unity and $M$ is a maximal ideal of $R$, then $R/M$ is a field. There are many proofs of this, as you can see here. But ...
3
votes
1answer
46 views

Constructivist proofs + LEM = classical math?

I have been told that constructivist/intuitionist logic is classical logic - LEM. I see why LEM doesn't hold given the basic philosophy of constructivist mathematics, ehich I understand to be based ...
0
votes
0answers
49 views

Constructive proof for a problem of discrete random variables.

The problem is: For two discrete random variables $X$, $Y \sim p(x,y)$, can we find another random variable $Z$ independent of $X$, such that there exists a function $f$ satisfying $Y = f(X,Z)$? I'...
4
votes
2answers
440 views

Proof by contradiction in Constructive Mathematics

I’m watching this video on Constructive Mathematics Five Stages of Accepting Constructive Mathematics, and Andrej Bauer makes the following claim: Mathematicians call two different things “Proof by ...
0
votes
0answers
81 views

Can you recommend literature - easy/gentle/for self-study/introductory… - for the following topics…?

I am looking for literature that is as self-explanatory, easy, gentle, readable to the beginner, suitable for self-study, etc.. as possible, in the following fields. (I mean the mathematical part as ...
0
votes
0answers
18 views

How do I calculate the difference in the scale of objects at a distance

I’m in drafting class and I’m creating a template for $2$ point perspective drawings, I’m stuck trying to determine the decrease in the scale of two lines at a distance. The first line is $3$ inches ...
0
votes
0answers
53 views

Intermediate value theorem on open or closed ball in $\Bbb R^n$

Let $f:R \rightarrow \mathbb{R} $ be a continuous function, where $R$ is either a open or closed ball in $\mathbb{R}^n$. Let $a,b$ be arbitrary points in $R$. Proof that if $ d$ is an arbitrary number ...
0
votes
1answer
32 views

Realizability model not realizing all of CZF

I would like to know some non-trivial examples of partial combinatory algebras whose realizability universe does not satisfy all of the axioms of Constructive Zermelo-Fraenkel (CZF) set theory. Based ...
0
votes
0answers
24 views

Constructive limit for bounded sequence

Define a constructive real number as a sequence of rational numbers $u:\mathbb{N}\to \mathbb{Q} $ equipped with a Cauchy modulus, ie a function $f : \mathbb{Q}\to \mathbb{N}$ such as $$ \forall \...
0
votes
0answers
51 views

The price of constructivity

It is said that proofs in constructive math, if possible at all, tend to be more verbose than in classical math. I'm trying to get an intuition for this, so: Are there any good example of theorems ...
0
votes
0answers
79 views

Is real analysis constructive?

I'm still wrapping my head around exactly what 'constructive' mathematics is. To my understanding, there are several theorems in real analysis which depend on the axiom of either dependent or ...
2
votes
1answer
92 views

Prove constructively that $\log_2 3$ is irrational.

The usual proof that $\log_2 3$ is irrational is by contradiction. For instance: Assume the negation: that $\log_2 3 = m/n$ for some integers $m$ and $n$. Then, by the property of logarithms, $2^{m/...
1
vote
2answers
83 views

Prove or disprove non-constructively there exist irrationals $a, b, c$ such that $a^{b^c}$ is rational.

Consider the interesting question: Do there exist irrationals $a$ and $b$ such that $a^b$ is a rational? Alternatively, prove or disprove that there exist irrationals $a$ and $b$ such that $a^b$ is ...
0
votes
1answer
64 views

Constructive Group theory?

What would group theory look like in constructive mathematics? i.e. what results in group theory do we know it is impossible to prove constructively?
1
vote
1answer
16 views

Constructive characteristic function of complemented sets

In Bishop and Cheng's paper, "Constructive Measure Theory", page 18, they define the characteristic function of a complemented set $A=(A_1,A_2)$ by the function $\chi : A_1\cup A_2 \to \mathbb{R}$, ...
2
votes
1answer
93 views

Understanding a quote from G. H. Hardy in 'A Mathematician's Apology'

I recently learned about the philosophy of constructive mathematics. In several discussions of the topic, I keep seeing a quote from G. H. Hardy's book A Mathematician's Apology; Reductio ad ...
5
votes
0answers
60 views

How to construct infinite products in constructive mathematics?

Maybe this is a very naive question because I don't know much about constructive mathematics besides basic definitions. Well, according to this article, I can interpret most of mathematics in a topos ...
2
votes
1answer
79 views

Intuitionistic logic and derivation

It is my first approach to intuitionistic logic (IL) and, even if I understand the principle behind it, I struggle understanding when a sequent is derivable in IL and when is not. I know that IL ...
1
vote
1answer
92 views

Does the canonical bijection between $\mathcal P(S)$ and $2^S$ use the axiom of choice or the law of excluded middle

Let $\mathcal{P}(S)= \{X \ | X \subseteq S\}$ and $2^S = \{g \ | \ g: S \rightarrow \{0,1\}\}$ and consider the bijection $$f : \mathcal{P}(S) \rightarrow 2^S$$ Defined for all $X \in \mathcal{P}(S)...
1
vote
4answers
117 views

Constructivity and Piecewise Functions

I'm currently exploring homotopy type theory and intuitionistic mathematics. In constructive/intuitionistic mathematics, 2 features arise: A proof of $\neg \neg A$ is not a proof of $A$. All ...
0
votes
1answer
23 views

How to construct a sequence that is the set of limit points but not equal to any element in another sequence?

Let ${y_j}_{j=1}^N$ be N given real numbers. Construct a sequence ${a_n}$ so that ${y_j}_{j=1}^N$ is the set of limit points of ${a_n}$, but $a_n \ne y_j$ for any n or j. My work is as follows, but ...
0
votes
0answers
74 views

Can this separating theorem imply yields the sign of a real number?

I am looking at the following separation theorem (called TH1): $\neg(\exists a \in \mathbb{R}^{1 \times m } ( a A > 0)) \Rightarrow \exists b \in \mathbb{R}^n_+ (Ab=0).$ Here $A$ is a matrix in $\...
2
votes
1answer
94 views

Constructive Intermediate Value Theorem (IVT)

I'm trying to learn a bit about intuitionistic/constructive mathematics, as I want to understand a little about topos theory and homotopy type theory (HoTT). I'm confused as to why the intermediate ...
0
votes
1answer
23 views

Transforming the inequality bellow

How do I get from here: $$\left(1+\frac{1}{n}\right)^n < e < \left(1+\frac{1}{n}\right)^n+1$$ To this this: $$\frac{n}{n+1} < \log(n+1)-\log(n) < \frac{1}{n}$$
2
votes
1answer
39 views

Constructive proofs for statements about rational numbers in Constructive Analysis

On page 26 of Bishop and Bridges "Constructive Analysis", in a proof of "If $x_1,...,x_n$ are real numbers such that $x_1 + ...+x_n$>0, then for some $i$, $x_i>0$", it seems to me this lemma is ...
1
vote
2answers
48 views

Proof in constructive mathematics using decidability.

I am working in constructive mathematics that means without the law of excluded middle. One may also interpret this as working in inuitionistic logic. Lets assume I have some set $A$ such that I ...
6
votes
3answers
179 views

Proof verification in constructive analysis

I want to proof something in constructive analysis, that means without the law of excluded middle (or, if one prefers this interpretation, in intuitionistic logic). First some definitions: $C(x_1,...
6
votes
3answers
858 views

Why is the principle of explosion accepted in constructive mathematics?

I think something is wrong with the principle of explosion, because according to it, if I know $P\wedge \lnot P$, I can deduce $Q$ though I don't know anything about $Q$. Is it really constructive to ...
-1
votes
2answers
60 views

Correction / Explanation of a proof in Constructive Anaylsis

I have two real numbers $x,a$ and I know that $\vert 1 - t \vert > 0$, where $t > 0$. Then I have \begin{align*} \Vert tx + (1-t)a\Vert = \Vert 1- t \Vert \Vert \frac{t}{1-t} x - a\Vert. \end{...
4
votes
2answers
372 views

Constructive intermediate value theorem

I have given real numbers $x_1,x_2,y_1,y_2$ such that $x_1 > x_2$ and $y_1 < y_2$. The the claim is that there exists some $\lambda \in (0,1)$ such that $\lambda (x_1 - x_2) + (1-\lambda)(y_1-...
3
votes
1answer
65 views

Do either of Markov's Principle and the Fan Theorem imply the other?

To be concrete: Let's define Markov's Principle as $$\forall P \subseteq \mathbb N, (\forall n \in \mathbb N, n \in P \vee n \notin P) \to \neg(\forall n \in \mathbb N, n \notin P) \to \exists n \in \...
-3
votes
1answer
34 views

agree or disagree and prove : UA = UB then A=B [closed]

agree or disagree and prove : union of A equal union of B then A equal to B .
3
votes
3answers
152 views

Constructive proof of the Cauchy Schwarz inequality

The famous CS inequality states $$ \left| \left< x , y \right>\right| \le \left\| x \right\| \cdot \left\| y \right\| $$ for $x,y$ in an inner product space $X$ over $\mathbb{K}$. Every ...
1
vote
1answer
202 views

Constructive proof of $\Vert x \Vert = 0 \Rightarrow x = {\mathbf0}$.

Let $X$ be a linear space over $\mathbb{R}$. We call the mapping \begin{align*} \left\Vert \cdot \right\Vert : X\longrightarrow \mathbb{R}^+\cup \{0\} \end{align*} a norm if for all $x,y \in X$ and ...
4
votes
0answers
99 views

Logic for physics

I'm looking for references on applications of logic (e.g. intuitionistic logic, toposes) to physics (especially quantum physics, as this is the area that I'm aware can be helped by logical ...
1
vote
1answer
88 views

Total order on constructive real numbers

Is there a definition of the real numbers in constructive or intuitionistic logic such as the order is total, ie $$ \forall x,y\in\mathbb{R},\; x \leq y \lor y \leq x $$ The classical proof of this ...
2
votes
0answers
116 views

Convex set is closed

I have some points $x_1,\dots,x_n$ in $\mathbb{R}^j$. I define the set $C(x_1,\dots,x_n)= \left\{\sum_{i=1}^{n} \lambda_i x_i : \lambda_1+\dots+ \lambda_n = 1, \lambda_i \ge 0 \right\}$. The closure ...
-1
votes
2answers
61 views

Annihilator in dual space [closed]

Let U and W are subspaces of a vector space V. If U is subset of W, inh(W) is subset of inh(U). Is the Converse true? How?
1
vote
1answer
74 views

Lie groups in synthetic differential geometry

I'm reading Mike Shulman's Synthetic Differential geometry (a small article for the "pizza seminar" it seems); and there's a part about Lie groups that I have trouble understanding. Actually there ...
3
votes
1answer
112 views

Locales as spaces of ideal/imaginary points

I recently saw a video of a presentation of Andrej Bauer here about constructive mathematics; and there are two examples of locales he mentions that strike me : he explains quickly what the space of ...
1
vote
2answers
82 views

Explicit/constructive example of open maps that are not continuous (especially from R to R)?

TLDR: I'm looking for an explicit map that is an open map but not continuous. The context my question arose was when learning the topological definition of continuous function. I made some progress ...
0
votes
2answers
65 views

Maximum of real numbers

A real number is a subset $x$ of $\mathbb{Q} \times \mathbb{Q}$ such that for all $(q,q')$ in $x$ we have $ q \le q'$, and a) for all $(q,q')$ and $(r,r')$ in $x$, the closed intervals $[q,q']$ ...
1
vote
1answer
103 views

Follow up question: Showing $\langle x , y_l \rangle > 0$

The setting is the same as in this question I now am supposed to show that $\langle x , y_l \rangle > 0$. I originally thought that this would be a quick consequence of \begin{align} \Vert x \Vert ...
1
vote
2answers
361 views

Distance from a convex set to a point

Let $Y \in \mathbb{R}^n$ be a nonempty convex set such that $0 \notin Y$ and fix $y_1,\dots,y_n$ in $Y$, where $n \ge 2$. I know that there exist $i,j$ such that $\Vert y_i \Vert > \Vert y_j\Vert$....
3
votes
1answer
104 views

Proof Verification $ x \ge 0 \wedge x \neq 0 \Rightarrow x > 0$.

Let the real numbers and the relations =, >, $\ge$ be defined as in this lecture PDF. I want to show the following statement: $$\forall x \in \mathbb{R}( x \ge 0 \wedge x \neq 0 \Longrightarrow x &...
1
vote
0answers
69 views

LPO, MP and LLPO

LPO $\forall x \in \mathbb{R} ( x = 0 \vee x < 0 \vee x > 0)$. MP $ \forall x \in \mathbb{R} (\neg (x = 0) \Rightarrow \vert x \vert > 0)$. LLPO $\forall x \in \mathbb{R} ( x \ge 0 \vee x \...
5
votes
1answer
127 views

Why is Markov's Principle an axiom?

Markov's Principle: Let $ x \in \mathbb{R}$. Then the following holds: \begin{align*} \neg (x = 0) \Longrightarrow \vert x \vert >0. \end{align*} In constructive mathematics (no law of excluded ...
2
votes
0answers
75 views

Constructive Separating Theorem from LLPO

LLPO: $\forall x \in R (x \ge 0 \vee x \le 0)$. Is there any known separating theorem following from the LLPO? By separating theorem I mean the separation of a convex, located set Y away from $0$. ...