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)

2
votes
0answers
71 views

Is $x^x$ rational for $x=\sqrt{2}^\sqrt{2}$

This might be naive. Is $x^x$ a rational number for $x=\sqrt{2}^\sqrt{2}$ ? I remember reading somewhere a long time ago that such $x^x$ is a rational number, as an example of issues with non-...
5
votes
2answers
99 views

Is there a clean non-contrived theorem that can only be proven by contradiction?

I know (see Can every proof by contradiction also be shown without contradiction? that there are some theorems that can be proven by contradiction (relying on the law of the excluded middle, that for ...
3
votes
1answer
39 views

Differences between constructivism and formalism

What are the main differences between the formalism and constructivism in mathematics? Is there some theorem or axiom valid in formalism which isn't valid in constructivism and vice versa? Is the ...
3
votes
1answer
198 views

Theorem regarding Change of Variables in finite dimesnion

My question is based on Change of Variables in Multiple Integrals II Peter D. Lax > It is not necessary to read the paper before answering this question.The author tried to prove change of variables ...
5
votes
1answer
53 views

If $a\geq 0$ and $a<\epsilon$ for all $\epsilon>0$ can we show $a=0$ without the law of excluded middle?

I am a PhD student currently studying for an upcoming analysis test. I was working through some problems with a study group and one problem was to show that functions with a certain property send sets ...
2
votes
0answers
61 views

Is there a “nice” “constructive” field of numbers?

I am wondering about this. I've had some interest in “constructive” mathematics, although also some rather strong opinions against those who want to insist that everything else is “wrong” in favor of ...
0
votes
0answers
16 views

Covering $10 \times 10$ board with L tetromino

Is it possible to cover a $10 \times 10$ board using L- tetrominoes? I think the problem relates to coloring proof but can't find a suitable colouring. Any help is greatly appreciated. P.S. Can ...
1
vote
1answer
34 views

Multiplicity of roots of polynomial with rational coefficients decidable?

From the standpoint of intuitionistic logic, multiplicity of roots of generic polynomial is uncomputable due to the inability to compare two real numbers. Even though the roots themselves are ...
1
vote
1answer
40 views

What does $0^-$ mean in set or type theory?

In "A Unification Algorithm for COQ Featuring Universe Polymorphism and Overloading", Ziliani and Sozeau say: Terms include variables $x \in \mathcal{V}$, constants $c \in > \mathcal{C}$, ...
2
votes
1answer
105 views

Is it possible that Gödel's completeness theorem could fail constructively?

Gödel's completeness theorem says that for any first order theory $F$, the statements derivable from $F$ are precisely those that hold in all models of $F$. Thus, it is not possible to have a theorem ...
3
votes
1answer
99 views

How do you visualize $\mathcal{P}(1)$ in constructive mathematics?

If I understand correctly, constructive mathematics doesn't prove that the powerset $\mathcal{P}(X)$ of a set $X$ is a Boolean algebra; in general, all we can say is that its a Heyting algebra. This ...
0
votes
0answers
40 views

Constructive proof of pigeonhole principle as stated in Software Foundations book

I'm trying to prove the pigeonhole principle from Pierce et al. Software Foundations book and I'm stuck with trying to do so without use of the principle of excluded middle. Here Coq formulation of ...
1
vote
2answers
64 views

Is $(\neg q \rightarrow \neg p) \rightarrow (p \rightarrow q)$ equivalent to $p \vee \neg p$ in intuitionistic logic?

I've heard mathematicians say that contrapositive arguments are usually preferable to proofs by contradiction, so I was curious if this was based on logical reasons (i.e. that $(\neg q \rightarrow \...
1
vote
2answers
27 views

Is there a way to see if $\alpha \in \mathbb{C}$ is constructible at a glance?

The notion of constructibility is not too obscure but mathematically, I find the definitions tedious and not very easy to handle with. I don't know if Ian Stewart's book Galois Theory edition 4 ...
1
vote
2answers
94 views

Intuitionistic Real Analysis?

It seems like the following argument is in some sense the basis of real analysis: If $\forall\epsilon>0,\;\; d(x,y)<\epsilon$ then $x=y$. But in order to prove this statement, wouldn't ...
0
votes
0answers
9 views

$Con(T) + T\vdash \neg\neg A$ implies $Con(T+A)$ for any intuitionistic theory T

It's easy to notice that for any intuitionistic theory T: $Con(T) + T\vdash \neg\neg A$ implies $Con(T+A)$ $Con(T) + T\vdash \neg\forall x\neg A$ implies $Con(T+\exists x A)$ where $Con(T)$ means, ...
11
votes
1answer
447 views

Approximate spectral decomposition

A detailed attempt below. I am interested in effective and constructive computations for finding approximate spectral decompositions in some suitable format. Namely, let $A: H \rightarrow H$ be a ...
3
votes
2answers
53 views

Multiplicity of real numbers in a tuple with known cardinality decidable?

Given a tuple $(x_1, \ldots, x_n)$ of computable real numbers $x_1, \ldots ,x_n$ and its cardinality $|\{x_1, \ldots x_n\}|=d \leq n$, is it decidable which numbers have which multiplicity? In other ...
3
votes
1answer
60 views

Proof that Henkin extension by constants is conservative over intuitionistic theories

In fact I'm interested in a (preferably constructive) proof of the meta-implication: $T\vdash[\exists x B(x)\to B(c)]\to A $ implies $T\vdash A $ , where $c$ is a new constant for $T, B$ and $A$ and ...
-1
votes
1answer
61 views

Mathematical Induction in constructive setting [closed]

I'm little confused. As we don't have a proof hence we can't say : let the equation holds till(for) fixed n, and then we are going to show (prove) it holds for n + 1. From this argument mathematical ...
1
vote
1answer
54 views

Intuitionistic logic unit type as truth

I am trying to learn constructive logic. Why can true be represent as a unit type while false is represented as the void type?
2
votes
0answers
27 views

Proving that a specific map exists

Let $(X, T_X)$ be a topological space and $\sim$ an equivalence relation on $X$, let $Q = X / \sim$ be the quotient space and let $q : X \to Q$ be the quotient map. Let $Z$ be a topological space and ...
2
votes
0answers
67 views

A doubt in the proof of “AC implies law of excluded middle”

i dont understand why axiom of choice is needed for the proof, since X is finite and (if i haven't misunderstand anything) we don't need axiom of choice to define a choice function for a finite set. ...
1
vote
0answers
84 views

Intuitonism and metamathematics.

There are various reasons why one would want to reject the law of the excluded middle when doing "normal" mathematics, which I won't get to here, but accepting those, does the same reasoning hold when ...
0
votes
0answers
30 views

An intuition connected with Heyting implication

Suppose $L$ is a bounded lattice and let $\Rightarrow$ be its Heyting implication, i.e. the operation defined in the standard way: $x\Rightarrow y$ is the largest object of the set $\{u\in L\mid u\...
0
votes
3answers
68 views

Give a “constructive” proof of the fact that in a metric space the intersection of two open balls is open

Main Question Can someone give a "constructive" proof of the fact that, Let $(X,d)$ be a metric space and $x,y\in X$. Let $B_d(x,r_x)$ and $B_d(y,r_y)$ be two open balls centered respectively at $...
6
votes
2answers
170 views

Law of Excluded Middle Controversy

I was reading an introductory book on logic and it mentioned in passing that the Law of Excluded Middle is somewhat controversial. I looked into this and what I got was the intuistionists did not ...
1
vote
1answer
25 views

Elements of bounded distributive lattice belonging to same prime ideals are equal?

I have read in a paper that by an easy application of Zorn's lemma one may show that two elements of a bounded distributive lattice are equal iff they are contained in exactly the same prime ideals of ...
1
vote
2answers
56 views

Are $\forall x \in A, \exists y \in B, p(x,y)$ and $\exists f \in B^{A}, \forall x \in A, p(x,f(x))$ equivalent?

Let $P := \forall x \in A, \exists y \in B, p(x,y)$ and $Q := \exists f \in B^{A}, \forall x \in A, p(x,f(x))$ It seems like the Q is stronger than P. I can prove P from Q, but not the other way ...
0
votes
1answer
78 views

Is there a sense in which a formal theory can be more or less “metamathematically aware”?

For example, in classical logic, because of the law of the excluded middle, all propositions must be true or false, so in order to prove that a proposition is actually independent of the theory, we ...
5
votes
2answers
527 views

What exactly are those “two irrational numbers” $x$ and $y$ such that $x^y$ is rational? [duplicate]

It's possible to prove nonconstructively that there exists irrational numbers $x$ and $y$ such that $x^y$ is rational, but that proof only proves that such numbers exist and does not specify what they ...
5
votes
0answers
53 views

Notation for inhabited sets

A set $X$ is called inhabited if it has some element. In classical mathematics, this means that it is not the empty set, so that one usually writes $X \neq \emptyset$. However, in intuitionistic ...
2
votes
1answer
33 views

Is there a conservative extension of IZF that extends IZF by a weak form of the axiom of choice?

The full axiom of choice implies the LEM, and so is incompatible with constructive mathematics, although there are some weaker forms of the axiom of choice, such as the axiom of dependent choice, or ...
6
votes
2answers
158 views

Does the law of the excluded middle imply the existence of “intangibles”?

First off, I'm not sure if "intangible" is standard terminology, Wikipedia defines an intangible object to be: "objects that are proved to exist, but which cannot be explicitly constructed". So if ...
5
votes
2answers
174 views

Constructivism versus the unicorn

Consider the following statement: "All unicorns have wings". As far as I know, Aristotle would consider this statement false, because as there are no unicorns, they cannot have any properties (like "...
1
vote
1answer
30 views

Focal distance on a parabola

If focal distance of a point on the parabola $y = x^2 - 4$ is $25/4$ . And the points are of form $(\pm \sqrt{a}, b$ then how can we find $a , b$ or sum of these . I think the focus of parabola would ...
4
votes
1answer
84 views

Go from A to D in three equal steps

Given two parallel lines $r$ and $s$, line $p$, perpendicular to both, and points $A$ and $D$ on different sides of $p$ with respect to the parallel lines, how can I prove the existence of two points, ...
4
votes
2answers
63 views

Does $A \lor \neg A$ assert decidability in intuitionistic logic?

I'm new to intuitionistic logic, so forgive my silly question. In intuitionistic logic, does $A \lor \neg A$ assert the decidability of $A$? For example, let's say I don't personally have a proof of $...
0
votes
0answers
29 views

Rota's Exoteric Slogan and Univalent Foundations

In "Indiscrete Thoughts" Gian Carlo Rota declares: Our exoteric slogan shall be: "Identity precedes existence." Esoterically, the problem of existence is a folie. From Wikipedia's current ...
0
votes
0answers
29 views

Division algorithm proof without well ordering principle

Is there a constructive proof of the division algorithm that doesn't invoke the well ordering principle?
2
votes
1answer
141 views

What is an example of a real-world application where a non-constructive proof has been sufficient?

When reflecting on applications of proof in the real-world, I find that I am only considering constructive proofs. For example, algorithms for performing robotic movement are useful because they ...
1
vote
1answer
94 views

Intensional vs. extensional equality (or something like this)

I'm reading this thesis by Michael Warren on Homotopy Type Theory. I'm really a newbie to the field and got puzzled right in the beginning, where the following rule appears: A little bit before he ...
0
votes
1answer
40 views

Must non-constructive existential proofs use axioms of foundation or choice?

I have been getting confused thinking about non-constructive proofs. Several axioms of ZFC imply existence of a set with certain properties, and for each axiom except foundation, infinity, and ...
1
vote
1answer
46 views

What is the difference between derivability and provability?

I am reading Lof's Intuitionistic type theory. He says, ...
2
votes
1answer
42 views

A property of Heyting implication

Let $H$ be a Heyting algebra with $\Rightarrow$ being its Heyting implication and $0$ its bottom element. Define $x^\ast:= x\Rightarrow 0$. Since: \[ x\cdot (x^\ast+y)=(x\cdot x^\ast)+(x\cdot y)=x\...
3
votes
2answers
193 views

Is ¬¬(¬¬P → P) provable in intuitionistic logic?

I have a feeling it's not, because ¬¬P → P is not provable. If it is, I'm not sure what kind of reductio I'd need to negate ¬(¬¬P → P). I believe a textbook somewhere said it was provable in ...
9
votes
3answers
149 views

Write $n^2$ real numbers into $n \times n$ square grid

Let $k$ and $n$ be two positive integers such that $k<n$ and $k$ does not divide $n$. Show that one can fill a $n \times n$ square grid with $n^2$ real numbers such that sum of numbers in an ...
1
vote
0answers
43 views

The Intermediate Value Theorem in Intuitionism

In a course on Intuitionistic Mathematics, the Intermediate Value Theorem is discussed, and it is shown why this theorem fails in intuitionism. This is true because: Let $\rho$ be a real number ...
1
vote
1answer
30 views

Showing that the free group (as a set of strings) is free

I'm working on a construction of the free group, and as the proof is taking me further afield than I'd expected I'd like some verification that I'm going the right direction and there is not some ...
1
vote
1answer
56 views

Density of $\mathbb{Q}$ in $\mathbb{R}$. Constructive Proof.

Is there any constructive proof that between two real numbers there is a rational number (I don't think so, but I don't really know)?