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
2 answers
54 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))...
user avatar
3 votes
1 answer
106 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, ...
user avatar
0 votes
1 answer
23 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": ...
user avatar
1 vote
0 answers
36 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 ...
user avatar
  • 11
0 votes
0 answers
36 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?
user avatar
2 votes
1 answer
53 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}}$ ...
user avatar
  • 19.6k
1 vote
1 answer
30 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$. ...
user avatar
1 vote
0 answers
70 views

Why does it appear that modern approaches to the Twin Prime Conjecture focus on optimization rather than construction? [closed]

I am wondering what makes it difficult to approach the twin prime conjecture by construction. I have only casual knowledge of the subject so far, so I apologize for any ignorance in advance. The ...
user avatar
0 votes
0 answers
52 views

Compactness theorem for first order language, constructive proof

Definition (satisfiability): a set $\Gamma$ of formulas of a first order language is satisfiable if there exist a structure $S$, a Boolean algebra $B$ and an evaluation function $V$ such that $V(C)=...
user avatar
2 votes
2 answers
129 views

How is reductio ad absurdum unintuitive?

I am not asking about opinions here, I'm asking for the reasoning behind the decision of certain logics/frameworks, like e.g. Intuitionism, to not contain RAA as a valid rule of inference. There is an ...
user avatar
4 votes
0 answers
97 views

The double negation of excluded middle in type theory

Context The following question concerns plain Martin-Löf type theory, under a propositions-as-types interpretation: in particular, proposition simply means type and not mere proposition, and ...
user avatar
  • 5,917
3 votes
0 answers
119 views

Using generating functions to construct or solve differential equations

I know that $T_n(x)$ is the solution of the differential equation $(1-x^2)y''-xy'+n^2y=0$, where $$ T_n(x)=\begin{cases} T_n(x)=1 & \text{if $n=0$}\\ T_n(x)=x & \text{if $n=1$}\\ T_{n}(x)=...
user avatar
  • 71
2 votes
1 answer
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 ...
user avatar
  • 2,302
1 vote
1 answer
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, ...
user avatar
  • 459
1 vote
0 answers
37 views

Equal subsquare sums

Let an $11\times 11$ square filled with numbers from 1 to 121. Is there a construction such that every $3 \times 3$ square has the same sum? Is there any generalization of the problem for $6n-1 \times ...
user avatar
0 votes
0 answers
28 views

Distance between two points being solved with Cramer's rule in a projective space

I'm trying to figure out the reasoning behind finding the distance between two points in order to solve for a new point. Given a point to represent a camera in 3D space, $\mathbf{X}_C$, find the 3D ...
user avatar
1 vote
1 answer
55 views

Instantaneously changing non differentiable function

Is it possible to construct a function such that it alternates between two values after each "infinitesimal"? Say $0$ and $1$. Now I am not able to properly define the question, but in terms ...
user avatar
0 votes
0 answers
62 views

Generalization of rationalization algorithm

In early algebra lessons, we are taught some algorithms to rewrite a fraction (in $\mathbb{Q}$) with roots in the denominator as another fraction with no roots (i.e. an integer) in the denominator. ...
user avatar
  • 1,231
4 votes
1 answer
86 views

Externalizing A Concrete Application of Double Negation Toposes

I'm trying to come up with concrete problems which can be solved via topos theory, and I've found a good case study which has been really instructive. I've spent the past few weeks trying to ...
user avatar
3 votes
0 answers
79 views

Proof intuition of Positive Linear Operators are Bounded.

I got stuck on proving this exercise for quite a while and found the proof of this statement Positive operator is bounded : For a real Banach space $E$ let $T:E\rightarrow E'$ be a positive operator ...
user avatar
4 votes
1 answer
98 views

Existence elimination in Lean 3

Lean 3 is a theorem prover that implements the calculus of inductive constructions. Differently than Coq, Lean 3s kernel works proof irrelevant. This means that in the kernel of Lean all proofs of the ...
user avatar
  • 1,368
1 vote
2 answers
122 views

Type Theory: we cannot prove double negation, but can we prove it is unprovable?

I'm currently trying to learn type theory from the first chapter of HoTT. It is remarked that we cannot prove $\neg\neg A \rightarrow A$, when $A$ is interpreted as a proposition, or, equivalently, we ...
user avatar
1 vote
1 answer
126 views

Constructive IVT: Question about initial step

Bishop states the constructive or approximate intermediate value theorem on page 40 of Constructive Analysis. Approx. IVT: Let $f$ be a continuous map on an interval $I$ with $a,b \in I$ and $f(a) <...
user avatar
  • 133
1 vote
0 answers
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 ...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 133
3 votes
2 answers
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 ...
user avatar
  • 133
6 votes
2 answers
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 ...
user avatar
5 votes
2 answers
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 ...
user avatar
  • 2,986
3 votes
2 answers
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$ ...
user avatar
  • 133
3 votes
0 answers
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\}$. ...
user avatar
2 votes
0 answers
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....
user avatar
  • 19.3k
1 vote
0 answers
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 ...
user avatar
  • 31
1 vote
1 answer
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 ...
user avatar
  • 5,917
3 votes
2 answers
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 ...
user avatar
  • 1,813
3 votes
1 answer
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....
user avatar
2 votes
1 answer
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, ...
user avatar
  • 21
0 votes
1 answer
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 ...
user avatar
  • 77
2 votes
1 answer
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 ...
user avatar
4 votes
0 answers
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 ...
user avatar
1 vote
1 answer
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-...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 3,535
6 votes
2 answers
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 ...
user avatar
  • 459
0 votes
1 answer
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$ ...
user avatar
  • 121
3 votes
1 answer
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. ...
user avatar
  • 133
1 vote
1 answer
83 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 $...
user avatar
  • 133
1 vote
1 answer
76 views

How does this formula $A\lor (A\to B)$ relate to intuitionistic logic?

It is my first approach to the proof theory of intuitionistic logic and I am considering a single-conclusioned Gentzen-style sequent calculus for it, namely $\bf G3i$ (Negri, Von Plato, Structural ...
user avatar
15 votes
0 answers
229 views

Does Tychonoff's Theorem imply Excluded Middle?

It is well-known that using excluded middle, we can prove that Tychonoff's Theorem implies the axiom of choice. This was proved by Kelley in 1950. However, the standard proof requires excluded middle ...
user avatar
  • 19.6k
2 votes
0 answers
52 views

What is the role of excluded middle in classic forcing arguments?

I was doing an exercise out of Jech's "Set Theory," and noticed something somewhat interesting. This is exercise 14.7 in Jech. Let $D=\{q:q\Vdash\varphi\}$ be dense below $p$. If there ...
user avatar
  • 1,892
3 votes
2 answers
125 views

Prove there is infinite number of 3 consecutive numbers which are sum of 2 squares.

Prove there is infinite number of 3 consecutive numbers which are sum of 2 squares of ($0\notin $) natural numbers. Example: $$72 = 6^2+6^2$$ $$73= 8^2+3^2$$ $$74 =7^2+5^2$$ I could only find 232,233 ...
user avatar
  • 86.2k
4 votes
1 answer
174 views

Does intuitionist second-order logic prove the negations of some classical theorems?

On p.2(!) of his book The Boundary Stones of Thought, Ian Rumfitt asserts Intuitionistic second-order logic affirms the negations of some classical theorems. That surprised me. I'm probably just ...
user avatar

1
2 3 4 5
10