# Tagged Questions

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.

71 views

### Is $x^x$ rational for $x=\sqrt{2}^\sqrt{2}$

This might be naive. Is $x^x$ a rational number for $x=\sqrt{2}^\sqrt{2}$ ? I remember reading somewhere a long time ago that such $x^x$ is a rational number, as an example of issues with non-...
99 views

### Is there a clean non-contrived theorem that can only be proven by contradiction?

I know (see Can every proof by contradiction also be shown without contradiction? that there are some theorems that can be proven by contradiction (relying on the law of the excluded middle, that for ...
39 views

### Differences between constructivism and formalism

What are the main differences between the formalism and constructivism in mathematics? Is there some theorem or axiom valid in formalism which isn't valid in constructivism and vice versa? Is the ...
198 views

### Theorem regarding Change of Variables in finite dimesnion

My question is based on Change of Variables in Multiple Integrals II Peter D. Lax > It is not necessary to read the paper before answering this question.The author tried to prove change of variables ...
53 views

### If $a\geq 0$ and $a<\epsilon$ for all $\epsilon>0$ can we show $a=0$ without the law of excluded middle?

I am a PhD student currently studying for an upcoming analysis test. I was working through some problems with a study group and one problem was to show that functions with a certain property send sets ...
61 views

### Is there a “nice” “constructive” field of numbers?

I am wondering about this. I've had some interest in “constructive” mathematics, although also some rather strong opinions against those who want to insist that everything else is “wrong” in favor of ...
16 views

### Covering $10 \times 10$ board with L tetromino

Is it possible to cover a $10 \times 10$ board using L- tetrominoes? I think the problem relates to coloring proof but can't find a suitable colouring. Any help is greatly appreciated. P.S. Can ...
34 views

### Multiplicity of roots of polynomial with rational coefficients decidable?

From the standpoint of intuitionistic logic, multiplicity of roots of generic polynomial is uncomputable due to the inability to compare two real numbers. Even though the roots themselves are ...
40 views

### What does $0^-$ mean in set or type theory?

In "A Unification Algorithm for COQ Featuring Universe Polymorphism and Overloading", Ziliani and Sozeau say: Terms include variables $x \in \mathcal{V}$, constants $c \in > \mathcal{C}$, ...
105 views

### Is it possible that Gödel's completeness theorem could fail constructively?

Gödel's completeness theorem says that for any first order theory $F$, the statements derivable from $F$ are precisely those that hold in all models of $F$. Thus, it is not possible to have a theorem ...
99 views

### How do you visualize $\mathcal{P}(1)$ in constructive mathematics?

If I understand correctly, constructive mathematics doesn't prove that the powerset $\mathcal{P}(X)$ of a set $X$ is a Boolean algebra; in general, all we can say is that its a Heyting algebra. This ...
40 views

### Constructive proof of pigeonhole principle as stated in Software Foundations book

I'm trying to prove the pigeonhole principle from Pierce et al. Software Foundations book and I'm stuck with trying to do so without use of the principle of excluded middle. Here Coq formulation of ...
64 views

68 views

29 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 ...
29 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?
141 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 ...
94 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 ...
40 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 ...
46 views

### What is the difference between derivability and provability?

I am reading Lof's Intuitionistic type theory. He says, ...
42 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 y)=x\...
193 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 ...
149 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 ...
43 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 ...