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

1
vote
1answer
45 views

Unordered pair of proper classes

The usual Kuratowski ordered pair function does not work on proper classes, because if $A,B$ are proper classes and $\langle A,B\rangle=\{\{A\},\{A,B\}\}$, then since $A\notin\{A\}$ and so on you get ...
0
votes
0answers
14 views

Bump function construction with positive Fourier transform [duplicate]

Fellow math people, I am looking to construct a bump function with a positive and rapidly decaying Fourier transform. In particular, the function f should satisfy: (1) f non-negative and smooth and ...
0
votes
1answer
25 views

How to construct a polynomial from a radix-term?

A term only composed of the following operatings shall henceforth be called a radix term because I don't know how these terms are called. A radix term $t$ is either an integer or a sum of two radix ...
1
vote
2answers
30 views

Additive Inverses are unique on the integers

I'm trying to prove that the additive inverses on $\mathbb{Z}$ are unique. We define the elements of the integers as equivalence classes of ordered pairs in order to define subtraction. My idea is to ...
1
vote
1answer
41 views

Weak (Brouwerian) Counterexample for existence of right inverse of a surjection

I'm dealing with Exercise 2 of Bishop's Constructive Analysis, Chapter 2 : Construct a mapping $f$ from a set $A$ to a set $B$ such that $f$ is onto $B$, but there does not exist a mapping ...
0
votes
1answer
93 views

how can I publish my log approximation formula

I've successfully found out a formula which can give log value of any base till 4-5 places after decimal I want to know whether it can get published because I've seen some journals which have ...
11
votes
0answers
150 views

What does it take to divide by $2$ (or even $3$)?

Theorem 1 [ZFC, classical logic]: If $A,B$ are sets such that $\textbf{2}\times A\cong \textbf{2}\times B$, then $A\cong B$. That's because the axiom of choice allows for the definition of ...
3
votes
3answers
98 views

Formal notion of computational content

In constructive mathematics we often hear expressions such as "extracting computational content from proofs", "the constructivity of mathematics lies in its computational content", "realizability ...
2
votes
2answers
85 views

Is there any case where classical logic has “proven” an incorrect result?

Intuitionistic logic rejects proof methods like double negation and proof by contradiction, making it impossible to make, for example, existence proofs without having a method of deriving what is ...
0
votes
0answers
47 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
129 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
146 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
150 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 ...
6
votes
1answer
255 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
85 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
147 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
173 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
158 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
111 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
18 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
93 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
15 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
49 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
19 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
519 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
19 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
51 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
105 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
2answers
230 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
48 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
47 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
33 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
52 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
103 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
230 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
204 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
56 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
217 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
274 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
113 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
121 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
174 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
43 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
121 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
148 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
250 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
89 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
179 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 ...