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)

1
vote
2answers
54 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
68 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, ...
9
votes
1answer
293 views
+100

Approximate spectral decomposition

See 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 Hermitian ...
3
votes
2answers
50 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
53 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
58 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
47 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
58 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
81 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 ...
5
votes
2answers
136 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
73 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
450 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
30 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
153 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
168 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
26 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
82 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
59 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
26 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
27 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
122 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
82 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
38 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
175 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 ...
6
votes
0answers
84 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
342 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
119 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
107 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 ...
0
votes
0answers
31 views

Structural induction over types that accept functions, in Coq

If you define an inductive type in Coq with a constructor that accepts a function mapping to that type, you get a somewhat odd induction rule. ...
0
votes
2answers
68 views

Question about Lemma (2.3) in Constructive Analysis, Bishop and Bridges

I am in the process of formalizing the constructive notion of a real number and the equivalence on them in the proof assistant Agda, but I am having trouble with the proof of Lemma (2.3) in the ...
0
votes
2answers
55 views

What is a Cauchy sequence of definable reals whose limit is undefinable?

Wikipedia claims that there exist Cauchy sequences of definable numbers whose limit is not definable. Are there constructive proofs of this? If so, what is an example of a Cauchy sequence of definable ...
-1
votes
1answer
39 views

Numerical integration of functions over computable Cauchy sequences

I'm interested in exact real arithmetic (and by extension constructive analysis). A nice representation of real numbers is via Cauchy Sequences. The basic idea being that you have a function which, ...
6
votes
3answers
303 views

Why can't you prove the law of the excluded middle in intuitionistic logic (for layman)?

I am learning about the difference between booleans and classical logics in Coq, and why logical propositions are sort of a superset of booleans: Why are logical connectives and booleans separate in ...
2
votes
1answer
61 views

Are there sets $S\subseteq\Bbb N$ which are provably non-empty, but we don't know what is $\min S$? [duplicate]

I was wondering if there is a property that is known to be satisfied for certain "things" but for which we do not know any explicit example. More explicitly (also more restrictive but possibly ...