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
1answer
67 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
85 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 ...
0
votes
0answers
21 views
0
votes
2answers
136 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 ...
3
votes
1answer
55 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
124 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 ...
7
votes
2answers
147 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
45 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
28 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
29 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 ...
0
votes
2answers
24 views

drawing tangents to circle whenangle is given

How to draw tangent to a circle when the angle between the tangents is given Here we cannot use the old conventional way of drawing tangents from a point
2
votes
0answers
163 views

Formalizing finitism in category theory

If we assume that finitism can be formalized by primitive recursive arithmetic (PRA), what category could it correspond to? In particular, which sort of a natural numbers object (NNO) may it contain? ...
3
votes
2answers
144 views

De Morgan laws of linear logic

I find it stated, in all the resources I have searched, that the following De Morgan laws$$(A\otimes B)^{\perp}\equiv A^{\perp}\wp B^{\perp}\quad\quad\quad (A\text{&}B)^{\perp}\equiv A^\perp ...
0
votes
0answers
52 views

Computability, Continuity and Constructivism

Triggered by an IMO extremely interesting question & Mathematics Stack Exchange, asked by Dal: Computability and continuous real functions And a link in one of the comments that could have ...
0
votes
0answers
42 views

Glivenko's theorem for propositional logic: $\neg\neg A, \neg\neg(A \rightarrow B) \vdash \neg\neg B$. [duplicate]

In proving Glivenko's theorem for propositional logic I have found myself not able to prove the following: $\neg\neg A, \neg\neg(A \rightarrow B) \vdash \neg\neg B$. The only inference rule I have is ...
5
votes
1answer
172 views

Is category theory constructive?

Roughly: This question concerns the process and the constructive nature of formalizing and proving category theoretic statements within $\textsf{ZFC}$. $\textsf{ZFC}$ can only talk about sets, ...
-1
votes
1answer
55 views

Finding a formula in intuitionist logic [closed]

I am looking for a formula which is true semantically but not syntactically in propositional intuitionist logic. Does it exist? If yes what's that? Thanks for your help.
4
votes
0answers
43 views

Construction of injective hulls without axiom of choice

Motivation: It is known that without the axiom of choice (AC), it is not provable that all categories of modules have enough injectives, let alone injective hulls. Still, there are examples of rings ...
2
votes
2answers
91 views

Intuitionistic proof of $(\exists x P(x)\to\exists x Q(x))\to\exists x(P(x)\to Q(x))$

This one is throwing me for a loop. My gut tells me that this isn't intuitionistically valid, although it is classically valid, since you have $$\forall x\,P(x)\implies\exists x\,P(x)$$ \begin{align} ...
3
votes
1answer
133 views

Online tools for checking validity of classical, intuitionistic, … logic formulas?

What online tools are available, where one can enter a formula of (first order) propositional or predicate logic, and have it check whether it is valid classically, intuitionistically, or even ...
3
votes
2answers
79 views

Intuitionistic proof of $\forall x(P(x)\lor Q(x))\to(\forall x P(x)\lor\exists x Q(x))$

Similar to Is $ \forall x(P(x) \lor Q(x)) \vdash \forall x P(x) \lor \exists xQ(x) $ provable?, but with intuitionistic logic. I expect it is not, since I don't think the $\exists x Q(x)$ on the right ...
2
votes
1answer
82 views

Is $\lor$ definable in intuitionistic logic?

The Wikipedia page mentions that $\{\lor,\leftrightarrow,\bot\}$ and $\{\lor,\leftrightarrow,\neg\}$ are complete sets of operators for intuitionistic logic, and also gives a few equivalences for ...
3
votes
3answers
88 views

Proving that two summations are equivalent [duplicate]

Give a constructive proof to show that for all $n \geq 1$ , $\sum\limits_{i=1}^n i^3 = (\sum\limits_{i=1}^n i)^2$ Observe that $(n+1)^4 - n^4 = 4n^3 + 6n^2 + 4n + 1$ . Now, the two following ...
4
votes
1answer
103 views

How is induction justified in intuitionistic logic?

This question might be extremely naïve for which I apologise in advance. The induction principle can be stated as: If $A ⊂ ℕ$ such that $1 ∈ A$, and $ν(A) ⊂ A$ (where $ν\colon ℕ → ℕ$ is ...
4
votes
1answer
48 views

Two question about ${\mathbb Q}(\alpha)$ for $\alpha$ := $\sqrt[n]{7}$ + $\sqrt[n+3]{7}$

Let $\alpha$ = $\sqrt[n]{7}$ + $\sqrt[n+3]{7}$ with $n$ not divisible by $3$. Prove that $[{\mathbb Q}(\alpha) : {\mathbb Q}] = n(n + 3)$. Conclude that $\alpha$ is constructible if and only if $n = ...
36
votes
13answers
3k views

An easy example of a non-constructive proof without an obvious “fix”?

I wanted to give an easy example of a non-constructive proof, or, more precisely, of a proof which states that an object exists, but gives no obvious recipe to create/find it. Euclid's proof of the ...
1
vote
1answer
34 views

Inequality and Intuitionistic logic

$x, y \in \mathbb{R}$ Is the proposition $x \leq y \Rightarrow x=y \lor x<y$ true in intuitionistic logic ? And what about $x \leq y \Rightarrow \lnot(\lnot(x=y \lor x<y))$ (with $\lnot$ the ...
6
votes
3answers
271 views

Does $A\times A\cong B\times B$ imply $A\cong B$?

This is similar to What does it take to divide by $2$? about $(A\sqcup A\cong B\sqcup B)\Rightarrow A\cong B$ which is valid in $\textsf{ZFC}$ by using cardinalities and also in $\textsf{ZF}$ by some ...
5
votes
3answers
246 views

Intuitionistic Logic and Classical Logic on the proof of (A or B)

In intuitionist logic, a proof of (A or B) means a proof of A, or a proof of B, whereas in Classical logic, a proof of (A or B) may be done withouth either proving A or proving B. I'm trying to ...
4
votes
1answer
129 views

Is the anti-foundation axiom considered constructive?

In the area of theoretical computer science that I am interested in, constructive mathematics is of practical interest because it gives algorithms that can be implemented on a computer. However, ...
4
votes
1answer
46 views

How to prove that an existence statement cannot be constructive

Given the well known spaces of sequences: $$ l_\infty =\{(x_n), n\in \mathbb{N}, x_n \in \mathbb{R} : \sup_n |x_n|<\infty\} $$ $$ l_1= \{(x_n), n\in \mathbb{N}, x_n \in \mathbb{R} : \sum_n ...
3
votes
0answers
65 views

Is the following derivation of Gödel's Paradox generalizable to an intuitionistic one using provability?

I will follow Goedel's original proof of Goedel's paradox located on pg. 264 of Hao Wang's A Logical Journey: From Gödel to Philosophy. With this in sight, and to also avoid confusion, I will also ...
1
vote
1answer
67 views

Unordered pair of proper classes

The usual Kuratowski ordered pair function does not work on proper classes, because if $A,B$ are proper classes and $\langle A,B\rangle=\{\{A\},\{A,B\}\}$, then since $A\notin\{A\}$ and so on you get ...
0
votes
0answers
15 views

Bump function construction with positive Fourier transform [duplicate]

Fellow math people, I am looking to construct a bump function with a positive and rapidly decaying Fourier transform. In particular, the function f should satisfy: (1) f non-negative and smooth and ...
0
votes
1answer
35 views

How to construct a polynomial from a radix-term?

A term only composed of the following operatings shall henceforth be called a radix term because I don't know how these terms are called. A radix term $t$ is either an integer or a sum of two radix ...
1
vote
2answers
37 views

Additive Inverses are unique on the integers

I'm trying to prove that the additive inverses on $\mathbb{Z}$ are unique. We define the elements of the integers as equivalence classes of ordered pairs in order to define subtraction. My idea is to ...
1
vote
1answer
55 views

Weak (Brouwerian) Counterexample for existence of right inverse of a surjection

I'm dealing with Exercise 2 of Bishop's Constructive Analysis, Chapter 2 : Construct a mapping $f$ from a set $A$ to a set $B$ such that $f$ is onto $B$, but there does not exist a mapping ...
0
votes
1answer
121 views

how can I publish my log approximation formula

I've successfully found out a formula which can give log value of any base till 4-5 places after decimal I want to know whether it can get published because I've seen some journals which have ...
36
votes
1answer
1k views

What does it take to divide by $2$?

Theorem 1 [ZFC, classical logic]: If $A,B$ are sets such that $\textbf{2}\times A\cong \textbf{2}\times B$, then $A\cong B$. That's because the axiom of choice allows for the definition of ...
1
vote
1answer
84 views

Algorithm to force decidability of statements using an intuitionistic series of new axioms

Say that a set $\Phi$ is a finite set of statements in Peano arithmetic is meekly consistent if it contains no "inner,immediate" contradiction, i.e. for any statements $\alpha,\beta$, it does not ...
1
vote
2answers
107 views

Proving the non-derivability of formula using the of the kripke model

I try proving the non-derivability of $(p\to q) \to \lnot p \lor q$, using the of the kripke model. I tried using different combinations of $Wi$, but I get fail.
3
votes
3answers
115 views

Formal notion of computational content

In constructive mathematics we often hear expressions such as "extracting computational content from proofs", "the constructivity of mathematics lies in its computational content", "realizability ...
0
votes
1answer
60 views

Why do you only need to show validity in one world when using trees in institutionist/constructivist logic?

Depicted below, my prof used a tree to prove that an argument is valid according to intuitionist logic. However, I can't find a contradiction in world 0. Why is invalidity ascertained when all ...
2
votes
2answers
107 views

Is there any case where classical logic has “proven” an incorrect result?

Intuitionistic logic rejects proof methods like double negation and proof by contradiction, making it impossible to make, for example, existence proofs without having a method of deriving what is ...
4
votes
3answers
90 views

Seeking help to understand a simple Kripke model

I'm reading A Brief Introduction to the Intuitionistic Propositional Calculus, at page 7, there is a simple Kripke model represented by a graph, I interpret it as: $W = \{w_1, w_2\}$ $w_1 \ge w_2$ ...
0
votes
0answers
56 views

Existence of a basis in constructive vector spaces

As I was trying to review forgotten knowledge on Vector Spaces in wikipedia, I read that the existence of a basis follows from Zorn lemma, hence equivalently from the axiom of choice. Actually, the ...
2
votes
2answers
165 views

Is constructive proof of non-existence possible

Constructive proof construct(indicates) object that satisfies given predicate. Question is whether one can give constructive proof of non-existence of an object with given property e.g. that every ...
5
votes
1answer
204 views

Equivalence between Peirce's law and Excluded Middle in Intuitionistic logic

I'm searching for a intuitionistically valid proof of the formula : $[((P→Q)→P)→P] ↔ (P \lor \lnot P)$ using the "standard" Hilbert-style axiom system from Kleene [1952], for ...
3
votes
1answer
91 views

Is intuitionistic naive set theory consistent?

I'm asking because the usual argument that a set either belongs in itself or not doesn't apply. I did a quick search and it appears that the logic is also required to be contraction free. If it's ...
1
vote
1answer
279 views

Constructive proof of pigeonhole principle

I'm trying to prove Pigeonhole principle with Coq proof assistant. Here is how I defined it: ...