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.

learn more… | top users | synonyms

0
votes
0answers
38 views

Existence of a basis in constructive vector spaces

As I was trying to review forgotten knowledge on Vector Spaces in wikipedia, I read that the existence of a basis follows from Zorn lemma, hence equivalently from the axiom of choice. Actually, the ...
2
votes
2answers
110 views

Is constructive proof of non-existence possible

Constructive proof construct(indicates) object that satisfies given predicate. Question is whether one can give constructive proof of non-existence of an object with given property e.g. that every ...
1
vote
1answer
71 views

Constructive proof of pigeonhole principle

I'm trying to prove Pigeonhole principle with Coq proof assistant. Here is how I defined it: ...
2
votes
1answer
137 views

What if 'proof by contradiction' is not a valid method of proof?

I've just been reading this question about the existence (or lack thereof) of contradictions in maths. I've been wondering: What if 'proof by contradiction' is not a valid method to (dis)prove a ...
5
votes
1answer
232 views

Can the proof of fixed point theorems ever be constructive?

Overall, Brouwer fixed point theorem and Kakutani fixed theorem are non-constructive. Is there any established paper that demonstrates that there exists constructive proofs that do exactly what these ...
4
votes
1answer
75 views

An explicit construction for an everywhere discontinuous real function with $F((a+b)/2)\leq(F(a)+F(b))/2$?

I would like to know an explicit method on constructing an everywhere discontinuous real function $F$ with the property: $$F((a+b)/2)\leq(F(a)+F(b))/2.$$ There is a non-constructive example (with the ...
5
votes
1answer
94 views

Is there a formal way to describe classical logic as a reflective subcategory of constructive logic?

Working informally, we can take any proof $P$ in constructive (or intuitionistic) logic and turn it into a classical proof $cP$ by 'copying' it, since all the rules of constructive logic reappear in ...
3
votes
6answers
145 views

Constructive proof of Euler's formula

In most textbooks on the subject I have seen, Euler's formula (by which I mean $e^{ix}=\cos(x)+i\sin(x)$) is proved by applying either differential equations or the power series of sine and cosine. ...
7
votes
3answers
150 views

Algebraically, What Does $\Bbb R$ get us?

In terms of the basic algebraic operations -- addition, negation, multiplication, division, and exponentiation -- is there any gain moving from $\Bbb Q$ to $\Bbb R$? Say we start with $\Bbb N$: ...
6
votes
0answers
105 views

Is there such a thing as 'overtification' (dual to compactification)?

The dual to the notion of compactness for spaces is overtness. This duality is not manifest in the category of spaces but rather in the quantifiers used to define these notions. Is there a process ...
0
votes
0answers
17 views

Can we prove constructively that $\epsilon$-equilibrium converges to (mixed strategy) Nash equilibrium?

We know that by using standard classical mathematics, $\epsilon$-equilibrium does converge to exact (mixed strategy) Nash equilibrium as $\epsilon$ becomes smaller. My question is, can we prove this ...
3
votes
2answers
57 views

Contraposition in intuitionistic logic?

I read that contraposition $\neg Q \rightarrow \neg P$ in intuitionistic logic is not generally equivalent to $P \rightarrow Q$. If this is right, in what case can this contraposition ...
0
votes
0answers
12 views

Understanding Bishop's Constructive Intermediate Value Theorem

I'm reading Bishop's "Constructive Analysis," and I'm a little hung up on IVT. It says "Let $f$ be a continuous map defined on an interval $I$, and let $a$, $b$ be points of $I$ with $f(a)<f(b)$. ...
1
vote
1answer
48 views

$(\forall x,\, p\vee q(x))\leftrightarrow p\vee\forall x,\, q(x)$

Consider the logical formula $(\forall x,\, p\vee q(x))\leftrightarrow p\vee\forall x,\, q(x)$ where x does not appear free in p. This formula is not derivable in intuitionistic logic, but it is in ...
0
votes
0answers
18 views

Construct a Fourier series that diverges almost everywhere.

Andrey N. Kolmogorov was one of the greatest mathematicians and polymaths of the 20th century. One of his first achievements was to construct a Fourier series that diverges almost everywhere. How ...
10
votes
2answers
479 views

a “natural” real number that is not computable

Most of the examples of non-computable real numbers use some kind of a diagonalization construction over some turing computable model of computation. See Are there any examples of non-computable real ...
1
vote
0answers
14 views

Elliptical Cone

I have a building design in the shape of an elliptical cone. To understand the elevation of the structure. I need to draw/unfold an elliptical cone. Can somebody explain the process for the same ?
1
vote
1answer
48 views

Constructivist Interpretation of a Function

Lets suppose I have an exponential function $a^{x}$, and I desire to show that for any number $n$ in $(0, \infty)$, it is possible to find a value of $x_0$ such that $a^{x_0} = n$. The simplest proof ...
2
votes
2answers
91 views

Goedel's completeness theorem in and/or for intuitionistic first order logic

Warning: I am neither a logician nor a set theorist, just curious about foundations of classical and intuitionistic mathematics. Therefore it might well be that the things to come are plain wrong, and ...
6
votes
1answer
182 views

What's wrong with the classical Cauchy construction of the reals?

I am reading Bishop's "Constructive Analysis" and he says that defining a real number to just be an equivalence class of Cauchy sequences of rationals would be wrong. Why is that?
2
votes
1answer
47 views

Are there statments which do not have a constructive proof?

I understand that a lot of statements are just non-nonconstructive in nature (like negative statements), and I understand that a lot of statements are not provable without the axiom of choice. ...
0
votes
1answer
58 views

Why is P or not P is unsatisifiable by construction?

A proof of predicate logic inability to express graph reachibility (page 63) involves a formula which can be interpreted as (there is no path, no matter what is the length) or (there is some path). ...
2
votes
1answer
44 views

Intuitionistic logic and explicit existence proofs

I have read that to intuitionistically prove a statement of the form $\exists x.\varphi,$ we have to actually describe such an $x$ as an explicit expression (with free variables from $\varphi$, ...
1
vote
0answers
31 views

Are there useful combinatorial constructions of grammars?

By grammar I mean a formal language grammar such as $$ A \to aaBa \\ B \to bB | a $$ You can define a tree recursively as, letting $T= $ set of all trees, as $T = \bullet \times SEQ(T)$, where ...
4
votes
1answer
90 views

Is it true that there is no algorithm to approximate the least upper bound?

I just read the following text below from Bishop's Foundations of Contructive Analysis, is it true that there is no such algorithm? The book is from 1967 - I don't know if someone managed to invent ...
2
votes
1answer
51 views

Are all constrtuctively describable functions continuous? Do they necessarily come with a topology?

In the paper "An injection from $\mathbb{N}^\mathbb{N}$ to $\mathbb{N}$" by @AndrejBauer, about the question whether there exists an injection $\mathbb{N}^\mathbb{N}\to\mathbb{N}$, we writes ...
4
votes
2answers
98 views

Non-upper bounds without excluded middle

Motivated by an earlier question, I'm curious if we can prove the following statement without the law of excluded middle: Let $E$ be a set of real numbers. A number $x$ is said to be an upper ...
2
votes
1answer
207 views

How to represent Smullyan's “Mockingbird” puzzles in (Homotopy) Type Theory?

(If you're unfamiliar with the puzzles from To Mock a Mockingbird, three pages tell you everything you should need.) Is it possible to solve the riddles in To Mock a Mockingbird in a "propositions as ...
7
votes
1answer
184 views

What is the dual of implication?

You may divide Intuitionistic Propositional Logic into the negative and positive fragments. The negative fragment includes truth, conjunction, and implication while the positive fragment includes ...
2
votes
0answers
53 views

Set Theory - Well Order (Lexiographical combination)

Question: Prove constructively that if $(A_{1},\prec_{1})$ and $(A_{2},\prec_{2})$ are two well-ordered sets then their lexicographical combination $(A_{1} \times A_{2},<_{1,2})$ is also well ...
3
votes
1answer
192 views

About constructive mathematics and Homotopy type theory

I am a CSer and I am reading the HoTT book and found that doing math with computer is fascinating. I found that constructive math compared with classical math is beautiful because: type theoretic ...
8
votes
1answer
252 views

Axiom of Choice - Type Theory (Proof)

Background In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory ...
2
votes
1answer
112 views

Unprovable Equivalence in Type Theory

Let $\prec$ be a binary relation on a set $A$… A predicate $P(x)$ set $(x:A)$ is said to be progressive with respect to $(A,\prec)$ if \begin{equation} (\forall a:A)\Big((\forall b:A)\big(b \prec a ...
4
votes
2answers
112 views

Constructive proofs and omega-consistency

That old MSE question discusses the notion of “constructive proof”, and the answers explain that there is no one definition of what "constructive" or "non-constructive" means. Recently, I thought of ...
3
votes
1answer
159 views

What are the benefits or losses of learning real analysis through a constructivist approach instead of a standard apporach?

Recently I've found some courses on real analysis that use the constructivist approach and I got curious on some aspects: What are the benefits of learning through this approach? Is it ok to learn ...
2
votes
1answer
41 views

Computation and Elimination (Solution Verification)

Consider a set B (of binary strings) given by the introduction rules: \begin{equation} \frac{}{\epsilon :B} \quad \frac{a:B}{s_{0}(a):B} \quad \frac{a:B}{s_{1}(a):B}\end{equation} ...
4
votes
1answer
118 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
2
votes
0answers
142 views

Non-Constructive Proofs

I have just started to read more about constructivism and its critique towards classical logic. As I was reading, I came across a passage about non-constructive results, that mentioned the following ...
5
votes
1answer
244 views

Elaboration of calculus in finitistic maths

I was just curious if there were some approaches to prove major theorems of calculus in finitistic systems like PRA or ZF with negation of Axiom of Infinity? I'm aware of some questions which were ...
4
votes
2answers
88 views

Crowding the boundary of non-constructivity without crossing it?

Can any sense be made out of my vague feeling that some proofs in Ramsey theory are as close as you can get to non-constructive proofs without crossing the line? Is there any way to make this ...
10
votes
2answers
177 views

A group is not the union of two subgroups, constructively.

Let $G$ be a group, and let $H$ and $K$ be subgroups of $G$. The following is well-known: Proposition 1. If $H \cup K = G$, then $H = G$ or $K = G$. See, for instance, this answer. Question. Is ...
14
votes
2answers
327 views

What practical proofs work in intuitionistic but not minimal logic?

Intuitionistic logic contains the rule $\bot \rightarrow \phi$ for every $\phi$. In the formulations I have seen this is a separate axiom, and the logic without this axiom(?) is termed "minimal ...
2
votes
1answer
146 views

Is proof by contradiction always a sufficient proof technique?

Is proof by contradiction always a sufficient proof technique ? A proof by contradiction has the form: Let $P$ and $Q$ be statements. If $ P \rightarrow Q \land \lnot Q $ then you can conclude ...
4
votes
1answer
105 views

Decidable & Recursive predicates

Let $C$ be a decidable predicate in the language of arithmetic HA, that is $$ \vdash (\forall \underline x)\: C(x) \vee \neg C(x).$$ $C$ is recursive if there exists a computable characteristic ...
4
votes
6answers
231 views

Proving the real numbers are complete

In Rudin's book, the following proof is published: Let $A$ be the set of all positive rationals $p : p^2 < 2$. Let $B$ be the set of all positive rationals $p : p^2 > 2$. $A$ contains no ...
5
votes
3answers
195 views

How can some statements be consistent with intuitionistic logic but not classical logic, when intuitionistic logic proves not not LEM?

I've heard that some axioms, such as "all functions are continuous" or "all functions are computable", are compatible with intuitionistic type theories but not their classical equivalents. But if they ...
1
vote
1answer
115 views

Why do sequences exist? What does “constructing a sequence” mean formally?

Everybody knows arguments like: "We can construct such a sequence inductively. Let $a_0$ be chosen as [..]. Then we can choose $a_{k+1}$ out of the set $A_{k+1}$ (which was shown to be non-empty)." ...
3
votes
2answers
205 views

Axiom of Choice, Continuity and Intermediate Value Theorem

I am trying to understand a proof I read in Herrlich's book Axiom of Choice. For those who know the book, it is theorem 4.54 on page 74. The part I am interested in reads: (9) A function $f:X ...
2
votes
1answer
74 views

constructive proof of solution for this recursive formula

The two conditions $$\frac{p_{\mathrm{up}}(n)}{p_{\mathrm{down}}(n+1)}=c \quad \text{and} \quad p_{\mathrm{up}}(n)+p_{\mathrm{down}}(n)=1$$ lead to $p_{\mathrm{up}}=\frac{c}{c+1}$ and ...
2
votes
1answer
80 views

Co-transitivity of the constructive order relation

One of the first exercises in J.L. Bell's A Primer of Infinitesimal Analysis asks the reader to show that, for arbitrary real numbers $a$, $b$, and $x$, if $a < b$, then either $x > a$ or $x ...