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)

0
votes
0answers
15 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
30 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
33 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
100 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
92 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
32 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
60 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
26 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
70 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
7 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
420 views

Approximate spectral decomposition

A detailed attempt below. Wanted: complex analysts I am interested in effective and constructive computations for finding approximate spectral decompositions in some suitable format. Namely, let $A: ...
3
votes
2answers
52 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
55 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
60 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
49 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
26 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
62 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
82 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
1answer
26 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 ...
0
votes
3answers
67 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
156 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
0answers
20 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
55 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
77 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
463 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
50 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
31 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
157 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
171 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
27 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
83 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
60 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
27 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
126 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
85 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
39 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
42 views

What is the difference between derivability and provability?

I am reading Lof's Intuitionistic type theory. He says, ...
2
votes
1answer
36 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 ...
3
votes
2answers
182 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
146 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
40 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
51 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)?
2
votes
1answer
36 views

“Two” definitions of injectivity on constructive mathematics

In classical mathematics, following two statements are equivalent: If $f(x) = f(y)$ then $x = y$ for each $x$ and $y$. If $x\neq y$ then $f(x)\neq f(y)$ for each $x$ and $y$. However, in ...
0
votes
1answer
36 views

Definition of all real numbers in terms of four arithmetic operations on 1? Reading material?

Is there a (more or less complete) theory of real numbers, where every number except for $1$ is defined by a combination of arithmetic operations acting on $1$. I know we can build any whole number ...
7
votes
0answers
87 views

Turning ZFC into a free typed algebra

The standard way of using ZFC to encode the rest of mathematics is sometimes criticized because it introduces unnecessary, strange properties such as, for example $1\in 2$ if we encode integers by ...
10
votes
4answers
352 views

Countable choice and term extraction

The constructive Axiom of Countable Choice (ACC) is widely accepted due to its computational content. It states that: $$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: ...
4
votes
1answer
121 views

Hidden usage of countable choice

Axiom of Countable Choice is a weaker form of the famous Axiom of Choice which is usually accepted even by constructivists. Following the famous book by Bishop & Bridges, Countable Choice in ...
1
vote
1answer
108 views

Constructive proof of transcendence of $e$ and $\pi$?

Someone asks to me that can we prove the transcendence of $\pi$ without using proof by contradiction. I find some proofs of transcendence of $\pi$ and $e$ and I found that all of proof I found starts ...