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
0answers
18 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
49 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
36 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
27 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
83 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
47 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
96 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
144 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
114 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
44 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
131 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 ...
5
votes
0answers
106 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
87 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
104 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
128 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
41 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
97 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
123 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
213 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
85 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 ...
8
votes
2answers
161 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 ...
13
votes
2answers
250 views

What practical proofs work in intuitionistic but not minimal logic?

Intuitionistic logic contains the rule $\bot \rightarrow \phi$ for every $\phi$. In the formulations I have seen this is a separate axiom, and the logic without this axiom(?) is termed "minimal ...
2
votes
1answer
107 views

Is proof by contradiction always a sufficient proof technique?

Is proof by contradiction always a sufficient proof technique ? A proof by contradiction has the form: Let $P$ and $Q$ be statements. If $ P \rightarrow Q \land \lnot Q $ then you can conclude ...
4
votes
1answer
96 views

Decidable & Recursive predicates

Let $C$ be a decidable predicate in the language of arithmetic HA, that is $$ \vdash (\forall \underline x)\: C(x) \vee \neg C(x).$$ $C$ is recursive if there exists a computable characteristic ...
4
votes
6answers
214 views

Proving the real numbers are complete

In Rudin's book, the following proof is published: Let $A$ be the set of all positive rationals $p : p^2 < 2$. Let $B$ be the set of all positive rationals $p : p^2 > 2$. $A$ contains no ...
5
votes
3answers
148 views

How can some statements be consistent with intuitionistic logic but not classical logic, when intuitionistic logic proves not not LEM?

I've heard that some axioms, such as "all functions are continuous" or "all functions are computable", are compatible with intuitionistic type theories but not their classical equivalents. But if they ...
1
vote
1answer
107 views

Why do sequences exist? What does “constructing a sequence” mean formally?

Everybody knows arguments like: "We can construct such a sequence inductively. Let $a_0$ be chosen as [..]. Then we can choose $a_{k+1}$ out of the set $A_{k+1}$ (which was shown to be non-empty)." ...
3
votes
2answers
181 views

Axiom of Choice, Continuity and Intermediate Value Theorem

I am trying to understand a proof I read in Herrlich's book Axiom of Choice. For those who know the book, it is theorem 4.54 on page 74. The part I am interested in reads: (9) A function $f:X ...
2
votes
1answer
67 views

constructive proof of solution for this recursive formula

The two conditions $$\frac{p_{\mathrm{up}}(n)}{p_{\mathrm{down}}(n+1)}=c \quad \text{and} \quad p_{\mathrm{up}}(n)+p_{\mathrm{down}}(n)=1$$ lead to $p_{\mathrm{up}}=\frac{c}{c+1}$ and ...
2
votes
1answer
74 views

Co-transitivity of the constructive order relation

One of the first exercises in J.L. Bell's A Primer of Infinitesimal Analysis asks the reader to show that, for arbitrary real numbers $a$, $b$, and $x$, if $a < b$, then either $x > a$ or $x ...
4
votes
1answer
233 views

constructive canonical form of orthogonal matrix

For every orthogonal matrix $Q$ over the reals there is an orthogonal matrix $P$ and a block diagonal matrix $D$ such that $D=PQP^{t}$. Each block in D is either $(1)$, $(-1)$ or a two dimensional ...
1
vote
1answer
113 views

How is the double negation translation similar to CPS in functional programming languages?

On wikipedia, I found that any formula in classical logic has its double negation as its intuitionist equivalent: It is also possible to define φN by prefixing ¬¬ before every subformula of φ, ...
12
votes
2answers
137 views

How far is it true that statements dependent on Axiom of Choice are not constructive.

Axiom of Choice is often used in mathematics to construct various objects, such as basis of $\mathbb{R}$ as a vector space over $\mathbb{Q}$, unmeasurable subset of $\mathbb{R}$, or a non-principal ...
68
votes
9answers
4k views

How far can one get in analysis without leaving $\mathbb{Q}$?

Suppose you're trying to teach analysis to a stubborn algebraist who refuses to acknowledge the existence of any characteristic $0$ field other than $\mathbb{Q}$. How ugly are things going to get for ...
1
vote
1answer
36 views

Provably finite sets in constructivist logic

I was reading about Diaconescu's theorem and began with the following statement: If for a given proposition $P$ we let $U=\lbrace x \in \lbrace 0,1 \rbrace : (x=0) \lor P \rbrace$, then $U$ is not ...
2
votes
2answers
112 views

Why a “set” whose elements is contingent on the truth value of a proposition is a set?

Let $P$ be a proposition (such as Goldbach's conjecture) that we can state precisely, but that we do not necessarily know to be true or false. Now define $$ S = \begin{cases} ...
3
votes
0answers
171 views

What do ultrafinitists think about Graham's number?

I know ultrafinitists want to require not only that mathematical objects be constructible, but be constructible given finite resources (such as time). So I wonder about something like the famous ...
1
vote
1answer
227 views

Run the girl-proposal algorithm to find a set of stable marriages

This is an example in a discrete structures book on stable marriages. Though i don't understand its solution. Any help will be appreciated Run the girl-proposal algorithm to find a set of stable ...
0
votes
1answer
104 views

sSet is a model for Martin-lof type theory

Simplicial sets category sSet satisfies the univalent axiom this is theorem now;with some large cardinal hypothesis. My question, Is sSet a model for Martin-lof typ theory by this theorem? any ...
4
votes
1answer
130 views

Model theory for intuitionistic predicate logic: a non-empty domain?

In classical logic we tend to make the assumption that the domain of quantification is non-empty. This isn't (too) problematic because classical mathematicians assume a language/mind/proof independent ...
4
votes
1answer
365 views

Constructing Idempotent Generator of Idempotent Ideal

Exercise 2.1 in Matsumura's Commutative Ring Theory reads as follows: "Let $A$ be a commutative ring and $I$ an ideal that is finitely generated and $I=I^2$. Then $I$ is generated by an idempotent." ...
0
votes
0answers
84 views

How to observe infinity?

In my calculus course, there's example stated on the book: Given that $M$ is an ordered set and the sequence $\{a_n\}\subset M$, prove that there's a (weakly) monotonic subsequence of $\{a_n\}$. ...
0
votes
1answer
302 views

Is the Green-Tao primes theorem true or pseudo-true? [closed]

The Green-Tao primes theorem "The primes contain arbitrarily long arithmetic progressions" Ann Math 2008, is certainly a tour de force and extremely technical. The authors point out that they have ...
2
votes
1answer
169 views

Can we get uncountable ordinal numbers through constructive method?

As we know, $2^{\aleph_0}$ is a limit ordinal number, however, it is greater than $\omega$, $\omega+\omega$, $\omega \cdot \omega$, $\omega^\omega$, $\omega\uparrow\uparrow\omega$, and even $\omega ...
6
votes
3answers
944 views

Double negation elimination in constructive logic

How can I prove that the double negation elimination is not provable in constructive logic? To clarify, double negation elimination is the following statement: $$\neg\neg q \rightarrow q$$
5
votes
4answers
310 views

Can the principle of explosion be removed from constructive logic?

Classical logic has the theorem ($p\wedge\lnot p)\rightarrow q$, which I will call EFQ ("ex falso quodlibet"). Constructive logic often has the principle built in, in the form of an axiom ...
24
votes
2answers
612 views

A few questions about intuitionistic mathematics

I have to write a paper on Intuitionism for my Philosophy of Science class and I'm struggling with a few concepts I have encountered in my self-study. The (intuitive) characterization of valid ...
4
votes
3answers
550 views

What is a constructive proof of $\lnot\lnot(P\vee\lnot P)$?

Glivenko's theorem says that $\lnot\lnot P$ is a theorem of intuitionistic logic whenever $P$ is a theorem of classical logic. Is it closely related to the so-called Gödel–Gentzen negative translation ...
2
votes
2answers
365 views

Induction as Peano Axiom

Let P be some proposition. If we have that $P(0)$ is true and that if $P(n)$ is true, then $P(S(n))$ is true, where $S(n)$ is the successor of natural number $n$. Then we have that $P(n)$ is true for ...
5
votes
1answer
202 views

How to compute isomorphism $V \simeq V^{**}$ (in Haskell)?

Since there is a canonical isomorphism between vector space $V$ and his dual dual space $V^{**}$, $\dim V \in \mathbb N \;$, I want to write it as a Haskell function. This function is going to have a ...