Questions tagged [constructive-mathematics]
The term "constructive mathematics" refers to the discipline in mathematics in which one proves the existence of mathematical objects only by presenting a construction that provides such an object. Indirect proofs involving proof by contradiction and law of excluded middle are considered nonconstructive. Constructivism is the philosophical stance that the only "true" mathematics is constructive mathematics.
542
questions
6
votes
2
answers
117
views
Proving the Existence of a Number without Constructing
Prove that for all $k \in \mathbb{N}$ then there exists $n$ such that
$$
7^k \mid 2^n + 5^n + 3
$$
My idea is to construct $n$ such that the equation above is valid. However, the construction that I ...
- 266
0
votes
0
answers
28
views
Defining function "constructability"
I have a question regarding the idea of a "constructible" function, in the sense that I can write down an expression for it.
For example, a bijection between $\mathbb{R}$ and its Hamel basis ...
- 3,023
1
vote
2
answers
134
views
How to solve $(x-1)(x-2)=0$ constructively?
I want to prove that
$$(x-1)(x-2)=0\Leftrightarrow x=1, 2$$
$\Leftarrow$ is easy. The problem is $\Rightarrow$.
Assuming $x\neq 1, 2$, we can derive $1=0$ by dividing both sides of $(x-1)(x-2)=0$ by $...
- 186
-1
votes
0
answers
31
views
What kind of partition of N over a computable function would describe the construct I'm posting?
I was wondering whether a pattern for Collatz conjecture be found within a partition based on a computable function.
I constructed the S6 set as follows:
The first member would be (0 x 2) + (2^0 x 21)...
3
votes
2
answers
79
views
The points M and N and the circle k are given. Construct an equilateral triangle ABC inscribed in circle k such that |AM|=|BN|.
I chose an arbitrary length r and constructed two circles with centers in M and N of radius r and marked their intersections with the given circle. Then I looked at the angle formed by the center of ...
- 99
1
vote
1
answer
89
views
Countable set in constructive mathematics
Let $A$ be an alphabet (i.e. a set of symbols) and suppose that $A$ is countable.
Let $X$ be the set of all the words (i.e. finite strings) that I can write using the alphabet $A$.
Can I prove in ...
- 275
4
votes
1
answer
231
views
What is considered proof? Wondering about the construction of the reals via Dedekind cuts, and how they can be said to exist.
BIG EDIT: I decided to re-write this question completely as it was first posted with a lot of misunderstandings on my part and unclear statements. Trying to edit it - with feedback from the lovely ...
- 59
6
votes
1
answer
320
views
Is intuitionist logic two-valued?
On this page https://en.wikipedia.org/wiki/Principle_of_bivalence :
Intuitionistic logic is a two-valued logic but the law of excluded middle does not hold.
On this page https://en.wikipedia.org/...
- 111
0
votes
1
answer
32
views
About double negation and dependent function in Agda
data ⊥ : Set where
f : {A : Set} → {B : A → Set} → ((a : A) → ((B a) → ⊥) → ⊥) → (((a : A) → B a) → ⊥) → ⊥
f = {! !}
Type of the function f means: If "If ...
- 13
1
vote
0
answers
62
views
Errett Bishop's formulation of Diaconescu's theorem
The Wikipedia article on Diaconescu's theorem states that
Already in 1967, Errett Bishop posed the theorem as an exercise (Problem 2 on page 58 in Foundations of constructive analysis).
The exercise ...
- 373
0
votes
1
answer
111
views
Real numbers cannot be constructed?
Sorry if this is another crank finitism question, I am bit confused.
According to wikipedia:
Constructivism asserts that it is necessary to find (or "construct") a specific example of a ...
4
votes
1
answer
74
views
Is there a non-constructive proof-functional logic
I understand that classical logic preserves truth, is bivalent, and contains non-constructive proofs. In contrast, intuitionistic logic preserves justification/verification for a proof, is not ...
- 606
0
votes
1
answer
161
views
Does the Axiom of Constructibility make Pasch's Axiom unnecessary?
I conjecture that we can weaken or replace Pasch's axiom while still admitting the n-dimensional Cartesian spaces over Euclidean ordered fields. Am I correct?
Tarski's axioms include the Continuity ...
- 2,317
2
votes
1
answer
81
views
Constructive proof of compactness theorem for countable propositional languages
Let $\mathcal{L}$ be a countable propositional language and let $\Gamma$ be a set of propositions of $\mathcal{L}$ (i.e. $\Gamma \subseteq \text{Prop}(\mathcal{L})$).
Definition: $\Gamma$ is ...
- 275
2
votes
1
answer
147
views
Is there a sheaf model where the Weak Markov's principle fails?
We define a real number $x$ to be pseudopositive if $\forall y \in \mathbb{R}$ we have $ \neg \neg (x > y) \vee \neg \neg (y > 0) $.
The Weak Markov's Principle (WMP) is the axiom that every ...
- 609
2
votes
1
answer
216
views
Having hard times to understand the double negation translation implications. Is constructive logic at least as strong as classical, after all?
I do understand that constructive logic forbids the "lemma of excluded middle" for various reasons (let's not discuss these now).
I do understand that lots & lots of classical theorems ...
- 1,426
3
votes
1
answer
50
views
Books about constructivist approach for proof
I'm interested about the constructivist approach to math, and how the proof works in thoose framework.
What are good introductory books I can read? I'm interested in online sources
- 407
11
votes
3
answers
406
views
Two vertices of a triangle being fixed, find the locus of the third vertex such that the triangle has its circumcenter inside the incircle
Recently I played a little bit around with GeoGebra and I constructed the in- and circumcircle of a $\triangle ABC$ with $A=(0,0)$ and $B=(1,0)$ and I asked myself if it is possible to construct the ...
- 1,732
4
votes
1
answer
132
views
Are constructivists in favor of the Property of Baire?
Since the Axiom of Choice proves the law of excluded middle, constructivists reject it. Does this mean that constructivists are in favor of the negation of Choice?
I take this further: Perhaps ...
- 1,619
0
votes
0
answers
94
views
Proving axiom consistency
I am trying to prove that some preconditions don't introduce an inconsistency to my (constructive) system. I would like to know if this is possible with the set-up below, and how to do this, and what ...
- 1
0
votes
0
answers
64
views
What methods/objects in ZFC can't be computed and why not?
I was reading the Wikipedia page for set theory and read the following passage:
"The most common objection to set theory, one Kronecker voiced in set theory's earliest years, starts from the ...
- 321
2
votes
0
answers
114
views
Does "Every set of $\mathbb{R}$ is Lebesgue measurable" imply some weakened LEM?
I would like to know if the Reverse Mathematics has a conclusion for this axiom ($\text{LM}$:Every set of $\mathbb{R}$ is Lebesgue measurable).
I have tried to translate this axiom into a halting ...
- 35
0
votes
2
answers
95
views
LLPO implies $x\leq0$ or $x\geq0$ in $\mathbb R$ [closed]
LLPO:If $a^{n}$ is a binary sequence containing at most one $1$, then
either $a^{2n}=0$ for each $n$, or else $a^{2n+1}=0$ for each $n$.
Prove LLPO implies $x\le 0$ or $x\ge 0$ in $\mathbb R$.
1
vote
1
answer
106
views
Prove the existence of $f$ and why the function $f_n$ is constructed
I'm not an experienced person in proof.
This is a proposition in Amann/Escher's Analysis.
Let $X$ be a nonempty set and $\mathcal{a}\in X$. For each $n \in\mathbb{N}^{\times}$, let $V_{n}:X^{n} \to X$ ...
- 11
-2
votes
1
answer
129
views
Why do most constructivists accept the axiom of countable choice? [closed]
One obvious reason is that it is useful. But is there a philosophical justification for it? This axiom does not seem of constructive flavour to me since there is no clear way to construct a choice ...
2
votes
1
answer
84
views
Why does Brouwer choose time as the only *a priori* concept in intuitionism, and how the numbers are constructed under such interpretation
I recently read some materials about intuitionism in the philosophy of mathematics, such as Intuitionism and Formalism by Brouwer himself, and some relative interpretations, I maybe understand how he ...
- 21
2
votes
0
answers
37
views
Constructive proof that analytic function equals zero
Let $h : V \to \mathbb{R}$ be an analytic function where $V \subseteq \mathbb{R}$ is open. This means by definition that for all $c$ in the domain of $h$, there is some neighbourhood $U \subseteq V$ ...
- 29.8k
2
votes
0
answers
57
views
Does the inverse image part of a geometric morphism preserve "transitive set objects"?
Background
Definitions
Recall that a functor $F : A \to B$, where $A$ and $B$ are toposes, is said to be the inverse part of a geometric morphism when $F$ preserves finite limits and has a right ...
- 29.8k
1
vote
1
answer
76
views
Constructive Zermelo-Fraenkel set theory is contained in Zermelo-Fraenkel set theory
I'm searching for a book or an article that proves that if a statement can be proved in Constructive Zermelo-Fraenkel set theory then the statement can be proved in Zermelo-Fraenkel set theory (for ...
- 275
0
votes
1
answer
113
views
Does the LNC imply the LEM?
If we do not assume the Law of Excluded Middle, we do not assume that there is no proposition $P$ for which it is false. However, if there were such a proposition, it would violate the Law of Non-...
- 960
-1
votes
1
answer
133
views
What are proofs in constructivist logic?
The difference in syntax between classical and constructivist mathematics is, as far as I've understood, not because constructivists think a well-formed proposition may be untrue and unfalse at the ...
- 960
0
votes
3
answers
117
views
Constructive proof that limits preserve inequalities
Suppose that $a_n \leq b_n$ for all $n \in \mathbb{N}$, where $a_n$ and $b_n$ are two convergent sequences. Is there a constructive proof that $\lim_{n \to \infty} a_n \leq \lim_{n \to \infty} b_n$? ...
- 10.3k
7
votes
1
answer
298
views
Axiom of Choice in Constructive Mathematics. Is it really an axiom?
The status of the Axiom of Choice varies between different branches of Constructive Mathematics.
For example, in Constructive Set Theory the Axiom of Choice is not accepted because it implies the law ...
- 275
0
votes
0
answers
31
views
Can we see association of sequencing of words in linguistic expression and the corresponding mathematical concept?
Consider a mathematical concept: "discrete random variable", here as par part of speech variable (being a noun) is coming first and the random (being an adjective) is coming just after the ...
- 71
-3
votes
1
answer
163
views
Why do intuitionists think that proving $\neg \neg P$ merely constitutes a proof of the inexistence of a proof for $\neg P$?
In every case of $\neg \neg P$ that I've come across, the statement $\neg P$ has been disproven. Never has such a proof merely been proof for the inexistence of a proof for $\neg P$.
Take the ...
- 960
1
vote
1
answer
205
views
Is there a constructive proof of Brouwer's fixed-point theorem that does not rely on triangulation?
I'm aware of the constructive proof of Brouwer's fixed-point theorem via Sperner's Lemma, and I love it for its simplicity, directness, and constructiveness.
However, I still have a lingering ...
- 1,125
0
votes
1
answer
58
views
Proving that the map $f:\mathbb R \to \text{Seq}(\mathbb Q)/\sim$ is surjective
I was reading about constructing Real numbers using Cauchy sequences of rational numbers.
To be more specific, let $\text{Seq}(\mathbb Q)$ be the set of all Cauchy sequences of rational numbers and ...
- 3,991
1
vote
0
answers
62
views
On constructive calculus of variations
I am looking for a constructive treatment of calculus of variations and, a bit more generally, infinite-dimensional vector spaces. To a certain extent, my problem is that I am not sure what the right ...
- 138
2
votes
1
answer
52
views
Constructively, under what conditions is $x < y \vee y < x$ an apartness relation?
A binary relation $⧣$ on a set $A$ is called an apartness relation if it satisifies the following three properties:
irreflexivity: for all $x \in A$, $\neg (x ⧣ x)$;
symmetry: for all $x,y \in A$, if ...
- 175
2
votes
1
answer
122
views
Class functions in constructive set theory
In Aczel’s book (draft) on constructive set theory (https://www1.maths.leeds.ac.uk/~rathjen/book.pdf) there is a proposition (4.2.4 on page 34) regarding when a class function exists. I’m not ...
- 209
2
votes
4
answers
244
views
Is the dual of Cantor's theorem provable without choice? without excluded middle?
For the sake of concreteness let's say we're talking about ZF, though I imagine this question can be asked for any 'typical' set theory without a choice axiom (and would prefer an answer that doesn't ...
- 175
14
votes
2
answers
630
views
law of excluded middle from subsets of finite sets being finite in “five stages of accepting constructive mathematics”
i’m reading andrej bauer’s five stages of accepting constructive mathematics (after watching his excellent talk of the same name).
here i stumbled upon a curiosity. on page 6 of the document, he ...
- 429
2
votes
1
answer
186
views
Intuitionistic Disproof of Intermediate Value Theorem
For uni I'm studying intuitionism, and I came across the following disproof for the IVT:
The thing I'm trying to understand is why this disproof is not valid in classical mathematics. In my research ...
- 187
4
votes
2
answers
203
views
distribution of disjunction and conjunction over each other in intuitionistic logic
I can't find any references as to whether or not the usual properties of disjunction and conjunction distributing over each other hold in intuitionistic logic. Consider:
$$(1) \ \ (p \vee (q \& r))...
- 647
5
votes
1
answer
228
views
A Reference From Andrej Bauer's Recent Talk on Countable Reals
Andrej Bauer gave a talk today in the topos institute colloquium (video here) announcing a proof that the dedekind reals can be countable in the absence of LEM and CC.
At roughly the 27 minute mark, ...
- 32.6k
0
votes
1
answer
28
views
Show the rational representation of e "converges to e" under constructive math, i.e. show that $\sum _{k=j+1}^i \frac{1}{k!} \le \frac{1}{n}$.
I'm trying to show that $e$ has a representation in constructive mathematics from Wikipedia's definition of convergence and definition of finite e.
Here is their definition of "convergence": ...
- 23
1
vote
0
answers
47
views
Make n numbers equal
Given $n$ rational numbers. Every time you can delete $2$ numbers, and add 2 numbers which are equal to $\frac{a+b}{2}$ (assume the number you delete is $a$ and $b$). How to judge whether it is ...
- 11
0
votes
0
answers
47
views
Zermelo-Fraenkel versus Constructive-Zermelo-Fraenkel
Let's suppose that a particular theorem cannot be proved in ZF (for example, because I have a counterexample in ZF).
Is it possible that the theorem hold in CZF?
- 275
2
votes
1
answer
99
views
“Large” Dependent Choice in IZF
The scheme of “large dependent choice” (LDC) consists of statements of the form
Suppose $\forall x \exists y P(x,y)$. Then for all $z$, there is some infinite sequence $\{s_i\}_{i \in \mathbb{N}}$ ...
- 29.8k
1
vote
1
answer
44
views
Constructive proof that AOC implies every subset has a complement
I am studying Bridges' Varieties of Constructive Mathematics. Exercise 7 in the first chapter is confounding to me. I don't know how the hinted proof strategy works.
Let $A$ be a subset of a set $B$. ...
- 96