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

2
votes
1answer
126 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
220 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
71 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
88 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
140 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
148 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$: ...
5
votes
0answers
104 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
43 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
10 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
47 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
469 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
11 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
86 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
176 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
44 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
43 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
29 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
49 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
196 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
175 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
49 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
175 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
247 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
110 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
109 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
146 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
115 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
137 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
241 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 ...
9
votes
2answers
172 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 ...
13
votes
2answers
303 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
122 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
103 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
225 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
184 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
113 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
198 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
72 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 ...
4
votes
1answer
309 views

constructive canonical form of orthogonal matrix

For every orthogonal matrix $Q$ over the reals there is an orthogonal matrix $P$ and a block diagonal matrix $D$ such that $D=PQP^{t}$. Each block in D is either $(1)$, $(-1)$ or a two dimensional ...
1
vote
1answer
132 views

How is the double negation translation similar to CPS in functional programming languages?

On wikipedia, I found that any formula in classical logic has its double negation as its intuitionist equivalent: It is also possible to define φN by prefixing ¬¬ before every subformula of φ, ...
14
votes
2answers
154 views

How far is it true that statements dependent on Axiom of Choice are not constructive.

Axiom of Choice is often used in mathematics to construct various objects, such as basis of $\mathbb{R}$ as a vector space over $\mathbb{Q}$, unmeasurable subset of $\mathbb{R}$, or a non-principal ...