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
1answer
16 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
61 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
95 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
15 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
53 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
0answers
47 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
368 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
47 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
24 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 ...
5
votes
2answers
106 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
153 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
25 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
80 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
52 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
23 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
21 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
0answers
79 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
65 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
28 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
37 views

What is the difference between derivability and provability?

I am reading Lof's Intuitionistic type theory. He says, ...
2
votes
1answer
28 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
151 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
145 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 ...
0
votes
0answers
36 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
28 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
46 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
34 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
32 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
83 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
314 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
108 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
99 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
28 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
50 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
52 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
35 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, ...
5
votes
3answers
220 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
59 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 ...
4
votes
1answer
143 views

Apartness of reals and algorithm exctraction

I am trying to wrap my head around the notion of apartness in constructive mathematics and it turns out I lack understanding miserably. I would like to use as elementary notions as possible, in the ...
0
votes
1answer
251 views

Constructive Induction to derive and prove the formula for a geometric sequence

$\sum_{i=1}^nr^i = a \cdot (b^n) + c$ Base Case: n=1, this holds Inductive Hypothesis: Assume for $n = k$, $k \ge 1$ that $\sum_{i=1}^k r^i = a * (b^k) + c$. Inductive Step: Prove for $n = k+1$ ...
2
votes
1answer
94 views

Quantifier-free induction and comparison with $\sqrt{2}$

I am trying to understand quantifier-free induction in the system called PRA - primitive recursive arithmetic which states the following: $$ \frac{ \varphi[0] \quad \varphi[n] \implies ...
5
votes
2answers
92 views

Proving that $\alpha\approx|\alpha|$ is not constructive

$\sf ZF$ tells us that for every ordinal $\alpha$ there is a bijection $f:\alpha\to|\alpha|$, more or less by the definition of $|\alpha|$, the cardinal of $\alpha$. What I would like to show is that ...
1
vote
1answer
139 views
0
votes
2answers
157 views

Limits and Series in Smooth Infinitesimal Analysis

I just learned a tiny bit about SIA. While it is interesting, that it handles derivatives so easily, I wonder: Can we still recover the concepts of limits (of sequences) and especially series, to ...
4
votes
1answer
96 views

Explicit homeomorphism between open and closed rational intervals?

Sierpiński's theorem states that every countable metric space without isolated points is homeomorphic to $\mathbb{Q}$. (A proof can be found here and a discussion here). An immediate corollary is ...
8
votes
2answers
160 views

Intuitionistically, are these inequivalent? $P \rightarrow Q,\; \neg Q \rightarrow \neg P,\; P \wedge \neg Q \rightarrow \bot,\; \neg P \vee Q$

Sometimes we get questions like this that essentially ask: Okay, I know there's at least three different ways of proving an implication, namely: direct proof proof by contraposition ...
8
votes
3answers
633 views

Difference between proof of negation and proof by contradiction

I stumbled across this interesting article titled "Proof of negation and proof by contradiction" in which the author differentiates proof by contradiction and proof by negation and denounces an abuse ...
1
vote
2answers
76 views

Can I define a bounded sequence whose Banach limit is not unique?

Banach limit, as a non-constructive object, is not unique. The Banach limit for some sequences, say, convergent sequences, sequences satisfying $a_n = a_{n+m}$ for all $n$ and some $m$, the Banach ...
0
votes
1answer
37 views

Constructing the Integers from the Naturals

I'm watching a video right now about the construction of the Integers from the Naturals. The way to do so was to define the equivalence relation $$(a,b)\text{ is equivalent to }(c,d)\text{ if ...
2
votes
1answer
32 views

Persistency on formulas in Kripke models

Let $ (W,R,f) $ a Kripke model. I have some trouble proving that the persistency property holds for formulas i.e if $ wRw' $ and $ w \Vdash \phi $ then $ w' \Vdash \phi $ , mainly due to the forcing ...