Skip to main content

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.

Filter by
Sorted by
Tagged with
-4 votes
0 answers
71 views

Example of constructive/intuitionist proof [closed]

I am looking for Examples of constructive/intuitionist proofs I would like to demonstrate a short constructive proof that is simple to explain in about 2 minutes. This is for a presentation about the ...
illuminatitruthseeker's user avatar
0 votes
0 answers
51 views

Would this logic be considered constructive?

I have asked about similar logics before, but this one is different. The logics that I’ve asked about in the past take the Gödel-McKinsey-Tarski translation for Intuitionistic Propositional Logic to ...
PW_246's user avatar
  • 1,308
2 votes
0 answers
51 views

Different Notions of Maximal Ideals in Constructive Mathematics?

I was working on proving the following classic result for non-zero commutative rings in constructive logic: $I \subseteq R$ is a maximal ideal iff $R / I$ is a field. The definition of maximal ...
Léreau's user avatar
  • 3,115
5 votes
1 answer
102 views

Transfering colored balls from random bags into identical ones

Let's consider the following scenario: There are $n$ colors, and there are $n^2$ colored balls, where we have $n$ balls of each of the $n$ colors. There are also $n$ bags $[b_1,b_2,\dots,b_n]$ where ...
EnEm's user avatar
  • 982
2 votes
3 answers
160 views

A constructive proof of this innocent set theoretic proposition?

I was reading Freiwald's An Introduction to Set Theory and Topology, and I came across the following exercise from Chapter 1: E8. Suppose $A$, $B$, $C$, and $D$ are sets with $A\ne\emptyset$ and $B\...
Atom's user avatar
  • 4,037
6 votes
1 answer
183 views

Why is homological algebra nonconstructive?

In the Introduction to Weibel's homological algebra book, he states that homological algebra gives nonconstructive results. He doesn't elaborate on this further, so I wanted to know where exactly the ...
Hyunbok Wi's user avatar
6 votes
1 answer
293 views

How to construct a nonzero real number between two given nonzero real numbers?

Statement: Let $$X=$$ $$\{(a,b) \in \mathbb{R} \setminus \{0\} \times \mathbb{R}\setminus \{0\}:a<b\}$$ There exists a function $f:X \rightarrow \mathbb{R} \setminus \{0\}$ such that for all $(a,b) ...
Mohammad tahmasbi zade's user avatar
1 vote
1 answer
98 views

Set-theoretic semantics for sigma types

I'm trying to understand the set-theoretical semantics of sigma types. Suppose $\Gamma\vdash A : \text{type}$, $\Gamma.A\vdash B:\text{type}$, $\Gamma\vdash a:A$, $\Gamma\vdash b:B[1.a]$, $\Gamma\...
user avatar
1 vote
1 answer
45 views

Does microaffineness imply function extensionality?

I am currently working through Bell's Primer of Infinitesimal Analysis. Because constructive math (in the sense of Martin-Löf Type Theory) does not have function extensionality, I wondered whether it ...
Schatzmeister's user avatar
5 votes
2 answers
122 views

Why does countability misbehave in intuitionistic logic

On page 3 of this paper https://arxiv.org/pdf/2404.01256.pdf I spotted the claim: Definitions of countability in terms of injection into ℕ misbehave intuitionistically, because a subset of a ...
Y.X.'s user avatar
  • 4,183
2 votes
2 answers
182 views

Finding an irrational number between two given irrational numbers constructively

Statement: Let $$X=\{(a,b) \in \mathbb{R} \setminus \mathbb{Q} \times \mathbb{R} \setminus \mathbb{Q}:a<b\}$$ There exists a function $f:X \rightarrow \mathbb{R} \setminus \mathbb{Q}$ such that for ...
Mohammad tahmasbi zade's user avatar
3 votes
0 answers
106 views

Construct a continuous function $f(x)$ periodic with period $2\pi$ such that the Fourier series of $f(x)$ is divergent at $x = 0$

problem statement: Construct a continuous function $f(x)$ periodic with period $2\pi$ such that the Fourier series of $f(x)$ is divergent at $x = 0$ but the Fourier series of $f^2(x)$ is uniformly ...
Martin.s's user avatar
2 votes
1 answer
96 views

The equivalences between points in a locale in constructive mathematics

I am currently following the definitions of the book Frames and Locales and those in the articles Pointfree topology and constructive mathematics and Topo-logie. There are at least three ways of ...
Dylan Facio's user avatar
2 votes
1 answer
120 views

Non-syntactic characterization of $\Delta_0$ formulae

A common schema in intuitionistic, constructive set theories is that of $\it{\Delta_0}$ separation: $$ \forall x\exists y\forall z(z\in y\leftrightarrow z\in x\wedge\phi(x, z))\text{ provided $\phi$ ...
Soundwave's user avatar
  • 443
2 votes
0 answers
97 views

Constructive Proofs in Elementary Real Analysis

In considering the theorem cited here uniform continuity and equivalent sequences , which states that where $f:X \rightarrow \mathbb{R}$ is a function, the following two conditions are equivalent: (a) ...
Noah 's user avatar
  • 61
4 votes
1 answer
83 views

Is it possible to prove that a finitely generated linear subspace has a basis constructively?

Here is a usual proof of the statement above. (A family of elements of $X$ indexed by $I$ is a function from $I$ to $X$. Bases are families. $\operatorname{cl}(\bar{v})$ is the closure (hull) of the ...
beroal's user avatar
  • 2,483
1 vote
1 answer
79 views

False statements in intuitionistic logic

In the explanations of intuitionistic logic I've been reading (1, 2, 3), especially in the explanation of the semantics, I don't understand how a proposition being false influences the situation. ...
bobismijnnaam's user avatar
1 vote
0 answers
136 views

Proving a theorem by proving that there must be proof of it

Is there an example where a mathematical theorem is proven by demonstrating the necessity of a proof, without actually providing the proof?
زكريا حسناوي's user avatar
4 votes
1 answer
185 views

confused by nonconstructive equivalence relations

I was reading "constructive analysis" by Bishop and right on page 15 he writes "The relation of equality given above for rational numbers is an equivalence relation. In this example ...
Jello's user avatar
  • 103
1 vote
0 answers
169 views

“Meet” of Zorn’s Lemma and Law of Excluded Middle

Work in intuitionistic logic (IL), and assume ZF. The Axiom of Choice (AC) implies both Zorn’s Lemma (ZL) and the law of excluded middle (EM). Furthermore, AC is the “join” of ZL and EM, since we can ...
Gavin Dooley's user avatar
  • 1,107
6 votes
1 answer
249 views

Non-constructiveness and finite mathematics

It is known that the multiplicative group $(\mathbb{Z}/p\mathbb{Z})^{\times}$ is cyclic. However, known proofs are all "non-constructive" in the sense that they don't rely on a direct ...
Weier's user avatar
  • 737
3 votes
1 answer
185 views

Why do constructive mathematicians claim that mathematical truth is temporal?

It seems to me (and correct me if this is a misconception) that the traditional divide in the interpretation and practice of mathematics is between platonists, who believe that mathematical objects ...
user9812063's user avatar
1 vote
1 answer
56 views

Is the set-indexed wedge of connected $1$-types a $1$-type?

We are working in homotopy type theory. Given a type $I$ and a family of pointed types $P : \prod i : I, \sum T : Type, T$, we can define the wedge product $\bigvee\limits_{i : I} P(i)$ as a certain ...
Mark Saving's user avatar
  • 32.1k
3 votes
2 answers
205 views

LEM and the curry-howard correspondence

The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus ...
user avatar
0 votes
0 answers
90 views

Classicalities of Homotopy Type Theory

What are statements of HoTT that are not provable therein and thus may or may not be true in specific models, specifically models in $(\infty,1)$- topoi? I've also seen the term "classicalities&...
Secher Nbiw's user avatar
1 vote
1 answer
207 views

How to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic?

I tried to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic. I used LEM for this proof: $\lnot(a \neq b)$ : $a=b$ $\lor$ $a \neq b$ Let $a=b$. Then statement $a \neq b$ is ...
Mike_bb's user avatar
  • 877
5 votes
2 answers
207 views

Proof that LEM is equivalent to the well-ordering of $\Bbb{N}$

John L. Bell's Intuitionistic Set Theory contains an exceedingly slick demonstration that the law of excluded middle is equivalent to the well-ordering of the natural numbers $\Bbb{N} := \{ 0, 1, 2, .....
Rivers McForge's user avatar
9 votes
0 answers
169 views

Does the Mostowski Collapse Lemma hold in CZF?

The Mostowski Collapse Lemma states that for all sets $S$ and extensional, well-founded relations $R$ on $S$, there exists a transitive set $T$ such that $(S, R)$ and $(T, \in_T)$ are isomorphic. It ...
Mark Saving's user avatar
  • 32.1k
2 votes
1 answer
176 views

Is the fundamental theorem of algebra true for constructive complex numbers?

I wonder whether the fundamental theorem of algebra holds in intuitionistic logic, using constructive complex numbers. (To get around the fact that in general we cannot compute the degree of a ...
Daniel Schepler's user avatar
2 votes
1 answer
113 views

What is the nature of the double negated axiom of choice?

Under what circumstances is the principle $$nnaoc : (\Pi x:A. \lnot \lnot B_x) \implies \lnot \lnot (\Pi x: A. B_x)$$ valid? So the axiom of choice, but using double negation instead of propositional ...
tailcalled's user avatar
1 vote
2 answers
90 views

Dumb Question: Is the set $\Delta$ in Smooth Infinitesimal Analysis a subset of the set $\mathbb{R}$ of the real numbers?

I am currently reading O'Connor's Introduction to Smooth Infinitesimal Analysis. In the paper, O'Connor defines $\Delta$ (or D in his paper) as the set of all numbers that are an element of R such ...
Abraham Robinson's user avatar
3 votes
1 answer
89 views

Do the Exponent Properties Apply in Constructive Mathematics?

I have been studying smooth infinitesimal analysis which depends entirely on the set $\Delta$ of numbers whose square (and all higher powers) are equal to $0$. Now, I know smooth infinitesimal ...
Abraham Robinson's user avatar
0 votes
4 answers
237 views

A Question about Proof of Lemma 8.5.14 in Terence Tao Analysis I

Lemma 8.5.14. Let X be a partially ordered set with ordering relation $\leq$, and let $x_0$ be an element of $X$. Then there is a well-ordered subset $Y$ of $X$ which has $x_0$ as its minimal element, ...
ju so's user avatar
  • 297
0 votes
0 answers
34 views

Construct a new feasible solution from an old one

The Problem Here is a part of the constraint of a linear programming. $$ \begin{align} \displaystyle\sum_{n=0}^{\infty}\pi_n=1,\;\pi_n&> 0,\forall n\geq0.,\\ ...
WenheWang's user avatar
1 vote
1 answer
59 views

Exercise 1.4.4 in A Course in Constructive Algebra.

I am asking about Exercise 1.4.4 in A Course in Constructive Algebra by R. Mines et al.: Let $I$ be the set of [infinite] binary sequences, and for each $i$ in $I$, let $A_i$ be $\{ x \in \{0, 1\} \...
Jan Matula's user avatar
0 votes
1 answer
99 views

How to prove that a formula is intuitionistically valid using Kripke semantics?

I want to know how to use Kripke semantics so that I can prove that a formula is intuitionistically valid. I think that all others cases will clear out if I understand the case of implication. Let's ...
Νικολέτα Σεβαστού's user avatar
8 votes
1 answer
312 views

Is $\sqrt{2}^{2\log_2 3} = 3$ a constructive solution?

$\sqrt{2}^{2\log_2 3} = 3$ is a solution to Can an irrational number raised to an irrational power be rational? While the famous $\sqrt{2}^{\sqrt{2}}$ proof is nonconstructive, this one is apparently ...
Monday's user avatar
  • 83
2 votes
1 answer
110 views

Intuitionistic well-orderings of uncountable sets

The well-ordering principle has always been considered to be highly unconstructive, as far as I know. However, I think intuitionistic mathematics can be compatible with the existence of a well-...
Keplerto's user avatar
  • 388
0 votes
0 answers
45 views

Deducing $(\forall x . P) \implies P$ in minimal logic if P does not depend on any variable.

This might be a bit of a dumb question, but after pondering for a while I can't arrive to a conclusion which satisfies me. In minimal logic, the elimination rule for $\forall$ is as follows: $\forall ...
Nicky García Fierros's user avatar
2 votes
0 answers
45 views

Are there constructively defined bump functions? [duplicate]

I am looking for a function $f:\mathbb{R} \to\mathbb{R}$ that is $C^\infty$, that equals zero when $|x| \geq 1$, that is strictly positive when $|x|< 1$ and that is constructively defined. Those ...
V. Semeria's user avatar
  • 1,279
2 votes
1 answer
103 views

Can $ZF$ construct this function?

Is it possible in the $ZF$ theory to construct a function with domain $\omega_1$ (the set of all countable ordinals) that maps each countable ordinal $\alpha$ to a bijection between $\alpha$ and $\...
cnikbesku's user avatar
  • 417
1 vote
2 answers
86 views

Well-Ordering Principle From Recursion Theorem

As far as I understand, in intuitionistic logic we have neither (i) the well-ordering principle nor (ii) the recursion theorem. But can one deduce one from the other? I believe we cannot deduce (ii) ...
fweth's user avatar
  • 3,574
9 votes
3 answers
2k views

Why is the Principle of Explosion considered constructive?

I read over this post Why is the principle of explosion accepted in constructive mathematics? and still have some thoughts/questions. One of the answers mentions that a formula is constructively valid ...
PW_246's user avatar
  • 1,308
3 votes
2 answers
200 views

If a proposition can be proved nonconstructively, does a constructive version of it also hold?

In this question, I define as follows. A sequence $\{a_n\}_{n\in\mathbb{N}}$ constructively converges to $a$ if there is a function $N:(0, \infty)\to\mathbb{N}$ such that $\forall \varepsilon>0, \...
Hayatsu's user avatar
  • 391
0 votes
1 answer
112 views

Would a constructive proof that intuitionstic ZF has a nonconstructive model be a problem for the intuitionist?

It is my understanding it is provable in ZFC+zero sharp that intuitionistic ZF has a nonconstructive model. (Here I am assuming the existence of zero sharp only to guarantee that ZFC has a ...
shipwaymg's user avatar
3 votes
1 answer
187 views

Is this proof constructive?

I found the following proof to be constructive: There is a bijection from $[0,1]$ to $(0,1]$. Have $0\mapsto \frac12, \frac12\mapsto\frac23,\frac23\mapsto\frac34,$ and so on. That takes care of $\...
Hayatsu's user avatar
  • 391
6 votes
2 answers
157 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 ...
FaranAiki's user avatar
  • 297
2 votes
3 answers
192 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 $...
BonBon's user avatar
  • 397
3 votes
2 answers
101 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 ...
Katarina's user avatar
  • 429
1 vote
1 answer
107 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 ...
effezeta's user avatar
  • 455

1
2 3 4 5
12