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.

Filter by
Sorted by
Tagged with
1
vote
0answers
69 views

Is there a game semantical countermodel to Markov's Principle?

For specificity, let's fix Markov's Principle as $$\forall P : \mathbb N \to 2. \neg(\forall n : \mathbb N. P(n) = 0) \to \exists m : \mathbb N. P(m) = 1.$$ I've seen an informal argument that this ...
1
vote
1answer
60 views

Piecewise linear functions in constructive mathematics

Is is possible to constructively prove that, for any function $f:\mathbb{R}\to\mathbb{R}$ piecewise linear, the absolute value $|f|:\mathbb{R}\to\mathbb{R}$ is also piecewise linear ? "Constructively"...
0
votes
1answer
39 views

Something missing in the definition of “doesn't hover”?

Definition 1.4 of “A lambda calculus for real analysis” (Paul Taylor) says: Definition 1.4 We say that $f:\Bbb R\to \Bbb R$ doesn't hover if, $$ \text{for any $e<t$,}\qquad \exists x.(e<x<...
0
votes
1answer
20 views

Minimum number of splits graph into two sets to delete all edges.

You are given a graph with $N$ vertices and $M$ edges. For one operation you can divide vertex set into two sets. After each operation you delete all edges between vertices from different sets. The ...
3
votes
1answer
68 views

Ultrafilter principle and Axiom of Dependent Choice as 'nonconstructive and constructive' components of the Axiom of Choice

As in the title, in the book 'Handbook of Analysis and its Foundations' by Schechter, the Ultrafilter principle is presented as a nonconstructive component of the Axiom of Choice, while the Axiom of ...
0
votes
0answers
19 views

Algorithm to decide whether a proposition is constructively provable [duplicate]

To decide whether a propositional formula $P$ is classically provable, the completeness theorem gives an easy algorithm : simply test all finite boolean combinations of the variables of $P$. It is ...
2
votes
1answer
90 views

Constructive proof that $\liminf na_n = 0$ if the series $\sum_{n=1}^{\infty} a_n$ converges

As stated in this question If $\sum a_n$ converges then $\liminf na_n=0$, the proof in the title can be proven if it can be shown that there is a subsequence of $na_n$ that converges to 0. I was ...
0
votes
0answers
55 views

Is every proof an array of implications?

I want to prove an implication but I don't know how I can do it without using contradiction. Is there a way to rewrite the contradiction in logical terms, only using the implication "$\Rightarrow$" ...
0
votes
0answers
38 views

Can you define non-effectively calculable function in constructive mathematics?

Pretty simple just what the title says. Can you define non-effectively calculable functions in constructive mathematics? Does this answer differ in any way if it were in an intuitionistic logic?
0
votes
0answers
58 views

Defining sets in intuitionistic logic

I'm somewhat familiar with the school of intuitionistic logic. I know that an intuitionistic logician thinks of infinity as constructive as apposed to complete. Thus a intuitionistic logician cannot ...
1
vote
1answer
54 views

Predicative separation and the limited principle of omniscience

The axiom schema of predicative separation says that, for a set X and a predicate F containing only bounded quantifiers, there exists a set whose members are exactly those members of X which satisfy F....
1
vote
1answer
67 views

How exactly does the currry-howard formalization of logic capture the semantics of LEM not holding?

Let $p$ be a proposition and $P$ the collection of propositions. In classical logic, the law of excluded middle holds, and we can model the semantics of this as saying that there is a function $\text{...
2
votes
1answer
74 views

Constructive models of Martin-Löf type theory with extensionality

I am trying to find a justification for homotopy type theory. Of course, I understand that there is value for certain types of mathematicians, but I would like to understand why normal computer ...
0
votes
1answer
73 views

Is there a subsystem of ZFC which constrains the Universe to $L$?

The Axiom of Constructibility states that $V$, the Universe of all sets, is equal to $L$, the Constructible Universe. When added to $ZFC$ does not place a constraint on what sets exist, instead what ...
0
votes
2answers
89 views

Constructive proof that only zero is less than one

Based on intuitionistic number theory as defined in https://plato.stanford.edu/entries/logic-intuitionistic/#IntNumTheHeyAri, I'm trying to prove that if $x < 1 \Rightarrow x = 0$ (with $1 = S(0)$ ...
2
votes
1answer
75 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
73 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
46 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
58 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
56 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
468 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
89 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
19 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
71 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
38 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
29 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
1answer
77 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
92 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
100 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
87 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
77 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
17 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
109 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
67 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
83 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
95 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
150 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
24 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
76 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
146 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
47 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
52 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 ...
5
votes
3answers
242 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
1k 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
392 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
90 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
36 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
181 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 ...