# 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.

500 questions
Filter by
Sorted by
Tagged with
54 views

110 views

### Real Numbers Cannot be Constructed: Question about Constructive Mathematics

I got into a discussion with someone stemming from the set of uncomputatble numbers and how they claimed that such numbers like $\pi$ (not uncomputable but you'll see in a second) don't exist. I was ...
1 vote
99 views

### Is there a constructive presentation of the Henstock-Kurzweil integral?

Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, ...
1 vote
37 views

1 vote
42 views

### Order relation on the geometric line as defined in Kock's synthetic differential geometry

I'm trying to figure out to what an order relation $<$ would look like on the geometric line $R$ as defined in Kock's synthetic differential geometry. If I understand correctly (in constructive ...
1 vote
79 views

### Order Properties of Constructive Reals (Bishop)

I aim to prove some of the order properties of Bishop's Real Numbers (given on page 22 of Constructive Analysis by Bishop and Bridges.) Bishop defines a real number to be a regular sequence of ...
306 views

### Impredicative Definitions (CZF)

CZF is touted as the predicative and constructive variant of ZF. This is because CZF avoids the fully impredicative axioms of powerset and full separation and alternatively because CZF has an ...
149 views

### Is there a decision procedure for *monadic* intuitionist first-order logic?

In Ch. 19 of the 4th edition of Methods of Logic, Quine gives a decision procedure for classical monadic first order logic (technically it's a decision procedure for what he calls "Boolean ...
172 views

### Prove that a construction exists: is this a constructive proof or existential proof?

This top answer claims that it is possible to prove that a constructive proof cannot exist. I think, if "non-existence of constructive proof" can be proven, then for some other questions, it ...
65 views

### Defining arbitrary join on the set of complete ideals of a Heyting Algebra

Given a Heyting Algebra $H$ we define a complete ideal (or c-ideal) $I$ to be a subset of $H$ satisfying. $\bot \in I$ $b \in I$ and $a \leq b$ implies $a \in I$ $X \subseteq I$ and $\bigvee X$ ...
65 views

### Maximal number of intersections within a bipartite graph

Consider $n$ line segments in the Cartesian plane. For $1\leq k\leq n$, the $k$-th line segment is drawn from $(k,0)$ to $(x_k,1)$, where $\{x_1,x_2,...,x_k\}$ is a permutation of $\{1,2,...,n\}$. ...
117 views

### Learning roadmap for constructive mathematics

I just watched the talk "five stages of accepting constructive mathematics". I am very interested to learn constructive mathematics but have zero knowledge of constructive mathewmatics/logic....
1 vote
61 views

### ¬(A∨¬A)⊢¬B in paracomplete systems

I am considering a paracomplete logic where the principle ¬(A∨¬A)⊢¬B holds. What does it take for the principle to be explosive, such that we can infer any ¬B? If we have some statement that is ...
1 vote
161 views

### Ordinary mathematical uses of Axiom K

Context. In what follows, we work in Martin-Löf type theory (MLTT). We denote dependent product types by $\forall$, the identity type over a type $T$ by $\equiv_T$, and let $U$ stand in for arbitrary ...
171 views

### How is the axiom of choice used (or not used) in the proof of the Lesbegue covering theorem in Andrej Bauer's paper in constructive mathematics?

In this paper Five stages of accepting constructive mathematics on page 484 (shown in the image below) it contrastingly shows the use of the axiom of choice ($\sf AC$) in the first proof and avoidance ...
97 views

### Topoi as models of constructive mathematics

In this question, it is argued that constructive mathematics cannot prove the existence of a discontinuous real function, because there is a topos $\mathcal{E}$ where all real functions are continuous....
82 views

### How to understand the Definitions of existential and disjunction of intuitionistic logic.

In the testbook I have learnt that with the natural deduction rules: $A \lor B \to (A \to C) \to (B \to C) \to C$ $\exists x A \to \forall x ( A \to B) \to B$ after put $\bot$ into C, B respectively, ...
126 views

### Is the Godel sentence considered true intuitionistically?

In classical logic, Godel shows that there are true statements undecidable for arithmetic, and consequently, that truth goes beyond a system of axioms ability for proof. My question is, given that ...
160 views

### Is there a definition of finite sets, such that it can be used to constructively prove that a subset and a quotient set are finite?

Is there a definition of finite sets equivalent to the traditional definition (equal cardinality {0, 1, .., n}) in classical mathematics, such that it can be used to constructively prove that a subset ...
55 views

### Gaps between intutionistic and classical arithmetic

Let $\mathrm{I}\Sigma_n$ stand for the classical theory of Robinson arithmetic + bounded induction + induction on $\Sigma_n$ formulas. Let $\mathrm{CI}\Sigma_n$ stand for the intuitionistic theory of ...
1 vote
84 views

### Generalization of Lawvere's fixed point for a bijection between $A$ and $(A\to B)\to B$

At the end of his paper about the set semantics of System F, Reynolds produces two sets $A,B$ and a bijection between $A$ and $(A\to B)\to B$. He concludes "since $(A\to B)\to B$ and $A$ are well-...
1 vote
190 views

### Is there a precise sense in which ZF is constructive

Often times proofs in ZF which do not use the axiom of choice are called constructive, but of course really it is easy to create non constructive proofs using LEM. Is there a precise sense in which ZF ...
374 views

### Why do so few authors package up the definition of a limit into a function?

Occasionally, you will literally see people arguing for nonstandard analysis purely to unnest the quantifiers in the definition of a limit. By unnesting, I mean avoiding an exists quantifier that is ...
54 views

### What is a selection protocol for choosing from n teams so all teams play k other teams?

Note: this problem is similar to this previous question but this aspect of the query was not fully addressed there. First, if $n$ is even, $k$ can be any value from 1 to $n-1$. If $n$ is odd, then $k$ ...
87 views

### Correct constructive proof of $0 \leq x < 1/n$, $\forall n \in \mathbb{N} \implies x = 0$.

I've set out to prove $$0 \leq x < 1/n, \ \forall n \in \mathbb{N} \implies x = 0$$ constructively. I will be using the construction of the real numbers given in Bishop's Constructive Analysis. ...
1 vote