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
28 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 ...
1
vote
0answers
47 views

Contructive implications of Cantor's diagonalisation argument [closed]

Following the question here (which is not duplidate), can the argument of Cantor (the famous diagonalisation argument that $\mathbb{R}$ is not countable) ever be constructed (or be finished)? ...
0
votes
1answer
23 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
27 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
1answer
20 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
147 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
136 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
37 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
40 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
144 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
49 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
42 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
84 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
55 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
69 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
76 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
81 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
99 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
46 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 = ...
35
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 ...
0
votes
0answers
25 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
259 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
220 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
122 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
45 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
62 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
56 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
30 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
36 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
48 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
114 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 ...
35
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
0answers
28 views

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

Consider pairs $(\Phi,n)$ where $\Phi$ is a finite set of statements in Peano arithmetic and $n$ is an integer. Say that $p'=(\Phi',n')$ is an elementary intuitionistic extension of $p=(\Phi,n)$ iff ...
1
vote
2answers
104 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
110 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
59 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
98 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
87 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
52 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
155 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
185 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
89 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
215 views

Constructive proof of pigeonhole principle

I'm trying to prove Pigeonhole principle with Coq proof assistant. Here is how I defined it: ...
2
votes
2answers
292 views

Equivalence between middle excluded law and double negation elimination in Heyting algebra

It's well-know that in intuitionistic logic, middle excluded law and double negation elimination are equivalent. For example, in Johnstone - Topo theory, I read that, in a Heyting algebra, $p\vee\neg ...
1
vote
2answers
100 views

Is it possible to prove that the encoding of existentials in System F is valid?

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows: $$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to ...
2
votes
1answer
165 views

What if 'proof by contradiction' is not a valid method of proof?

I've just been reading this question about the existence (or lack thereof) of contradictions in maths. I've been wondering: What if 'proof by contradiction' is not a valid method to (dis)prove a ...
6
votes
1answer
289 views

Can the proof of fixed point theorems ever be constructive?

Overall, Brouwer fixed point theorem and Kakutani fixed theorem are non-constructive. Is there any established paper that demonstrates that there exists constructive proofs that do exactly what these ...
4
votes
1answer
94 views

An explicit construction for an everywhere discontinuous real function with $F((a+b)/2)\leq(F(a)+F(b))/2$?

I would like to know an explicit method on constructing an everywhere discontinuous real function $F$ with the property: $$F((a+b)/2)\leq(F(a)+F(b))/2.$$ There is a non-constructive example (with the ...
5
votes
1answer
172 views

Is there a formal way to describe classical logic as a reflective subcategory of constructive logic?

Working informally, we can take any proof $P$ in constructive (or intuitionistic) logic and turn it into a classical proof $cP$ by 'copying' it, since all the rules of constructive logic reappear in ...