Questions tagged [constructive-mathematics]

The term "constructive mathematics" refers to the discipline in mathematics in which one proves the existence of mathematical objects only by presenting a construction that provides such an object. Indirect proofs involving proof by contradiction and law of excluded middle are considered nonconstructive. Constructivism is the philosophical stance that the only "true" mathematics is constructive mathematics.

Filter by
Sorted by
Tagged with
2
votes
2answers
88 views

Can a set have a complement in intuitionistic ZF?

Does IZF (ZF formulated in intuitionistic logic) prove that for any set $a$, $\{x: x \notin a \}$ does not exist?
1
vote
1answer
47 views

Intuition behind the construction of a fixed point from Kleene's fixed point theorem

Below is an explicit construction of a fixed point the existence of which is guaranteed by Kleene's fixed point theorem. I was wondering if there's any intuitive explanation of why the fixed point ...
1
vote
1answer
66 views

Is a constructive proof known for Tutte's Theorem?

I have been reading the Chapter on Matchings in Graph Theory, R. Diestel, Fifth Edition, and have just encountered the proof of Tutte's theorem. The statement of the theorem is: A graph $G$ has a $1$-...
0
votes
2answers
92 views

The law of excluded middle and the abstraction of “actual infinity”.

The encyclopedia of mathematics states: "Logically, acceptance of the abstraction of actual infinity leads to the acceptance of the law of the excluded middle as a logical principle." This ...
1
vote
1answer
63 views

In homotopy type theory, prove that law of excluded middle implies reduction ad absurdum

It's about Excercise 2 from here: While the principle of excluded middle $P\vee\neg P$ ( tertium non datur) is not provable, prove its double negation using the propositions as types translation: $\...
7
votes
1answer
75 views

Universal Quantifier $\forall$ and Generalized Conjunction $\bigwedge$ in intuitionistic logic

I have a question about $\forall xA(x)$ and $\bigwedge\! A(a_i)$ (= $A(a_1)\wedge...\wedge A(a_n)$). In classical logic, the universal statement $\forall xA(x)$ can be understood as a generalized ...
4
votes
0answers
45 views

Quotienting by an apartness relation

In Martin-Löf type theory, the notion of equality is basic, and for every type $A$ and elements $x, y \in A$ there is a type $x =_A y$. For any function $f\colon A \to B$ you can then prove $f(x) =_B ...
4
votes
3answers
110 views

Question about Bishop's “constructive analysis” for people familiar with bishop style constructive analysis only

It has been a while since i read Bishop's book "constructive analysis", recently I dug it out of my book shelve and started to read. I came around this observation on the top of page 85. &...
1
vote
1answer
75 views

What is the intuitionist / contructivist view of the Fermat theorem proof?

Since Wiles proof is in essence proof by contradiction, it relies on the law of excluded middle. Which as I understand intuitionists / constructivists do not accept as an axiom. So what is their view ...
6
votes
1answer
203 views

Constructive logic and Russell's paradox

To show that "naive set theory" doesn't work, Russell devised the famous example of the set $$A := \{ x \ | \ x \not\in x \},$$ which turns out can't be a set after all, because either $A \...
-1
votes
1answer
69 views

Constructing real numbers and why every real is not computable

Constructive vs computable real numbers asked two questions : Why isn't every real number computable? How is it possible to construct an uncountable set? What is wrong with following answers? 1....
2
votes
0answers
53 views

Defining function by overlapping cases in constructive logic

Is it possible to define a function by cases in intuitionistic logic where the cases possibly overlap and the function values disagree in the overlapping area? In particular, if I am working with real ...
2
votes
1answer
55 views

Identity and substitution in Intuitionistic Logic

I am a beginner in mathematical logic. I have a basic question about identity propositions in intuitionistic logic. For example, from $(*)$ and $(**)$: $$\Gamma\vdash a=b\quad\quad(*)\quad\quad\quad\...
5
votes
3answers
211 views

Constructive vs computable real numbers

I find it confusing that all of the following statements are true : The computable real numbers are countable. $-\hspace{-3pt}-$ Alan Turing, "On Computable Numbers, with an Application to the ...
3
votes
1answer
85 views

Type theory and constructivist mathematics with paraconsistent logic?

Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs ...
0
votes
2answers
61 views

Intuitionistic “atomic” proof of negation?

In the view of logic in terms of type theory (cf. the Curry-Howard correspondence), the type $\neg P$ is defined as $P\to False$, and a proof of $\neg P$ is therefore a function that takes a proof of $...
2
votes
1answer
90 views

Strongly constructive proofs: Proofs that don't make use of decidability?

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic: A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
0
votes
0answers
60 views

distributivity of min and max over + and · without the assumption of inverses

$\;$Dear SE$.$Mathematics community, I am trying to prove some properties on a Lattice with a proof assistant and extend these properties by interaction with addition $+$ and multiplication $·$ e.g. ...
2
votes
1answer
82 views

What is an example of constructive vs. nonconstructive type theory?

I am trying to get some basic terminology down related to type theory, and am currently on understanding the difference between "constructive type theories" and "nonconstructive type ...
1
vote
1answer
60 views

Constructible problems for which the solution is non-constructible?

For the sake of this question, I am using the word "constructible" in the sense of constructive mathematics: e.g. a real number is constructible if you can construct a Cauchy sequence for it ...
3
votes
0answers
83 views

Intuitionistic logic's book to self study…

I want to study intuitionistic logic by myself? Can you give some recommendations for the different levels (undergraduate and graduate)?
3
votes
0answers
91 views

Why are the Real Numbers indecomposable according to Wikipedia?

Wikipedia claims that It follows from the indecomposability principle that any property of real numbers that is decided (each real number either has or does not have that property) is in fact trivial ...
4
votes
1answer
96 views

Proof-irrelevance of identity types

In constructive type theories, we make a distinction between extensional and intensional identity types. It's trivial that extensional identity types are proof-irrelevant as the inhabitant of an ...
4
votes
3answers
226 views

Intuitionistically unprovable statements about the natural numbers

Intuitionistic first-order logic is first-order logic without the law of the excluded middle. A statement $P$ can be proven in classical first-order logic precisely when its double negation ...
6
votes
3answers
169 views

Does double negation distribute over implication intuitionistically?

Does the equivalence $$\neg\neg (P \rightarrow Q) \leftrightarrow (\neg\neg P \rightarrow \neg\neg Q)$$ hold in propositional intuitionistic logic? In propositional classical logic the equivalence ...
7
votes
2answers
163 views

Propositional truncation $||$-$||$ and double negation $\neg\neg$

I have a basic question about propositional truncation $||$-$||$ and double negation $\neg\neg$. According to the recursion rule of $||$-$||$, $A\rightarrow B=||A||\rightarrow B$ as long as $B$ is a ...
2
votes
1answer
89 views

$\neg\neg$-Stability

I see that some authors say that there are sets, for example, $\mathbb{N}$ and $\mathsf{Bool}$, that are $\neg\neg$-stable (i.e., satisfying $\neg\neg X\rightarrow X$). I understand what it means when ...
2
votes
1answer
102 views

$\textsf{isStable}(A)\rightarrow\textsf{isProp}(A)$?

I meet both $\neg\neg$-stable and proof-irrelevant types in Harper's handouts on homotopy type theory. I know clearly that proof irrelevance does not imply stability, but does stability imply proof ...
1
vote
1answer
69 views

Converse of $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$

The following proposition in (1) is taken as an axiom in intuitionistic propositional logic. $$(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))\quad\quad(1)$$ ...
2
votes
1answer
71 views

Question about arclength (smooth infinitesimal analysis)

In the original version of this question, I asked about the value of $\sqrt{\epsilon^2}$ in smooth infinitesimal analysis. A helpful hint from Andreas Blass led me to check the definition of root, and ...
1
vote
1answer
50 views

Propositional truncation and information hiding

I have a question regarding propositional truncation $||$-$||$ in homotopy type theory. According to the introduction rule of $||$-$||$, if $a:A$, then $|a|:||A||$. My question is, if $||A||$ is ...
5
votes
1answer
67 views

Actual and potential truth for neo-verificationists

Neo-verificationists such as Martin-Löf and Prawitz make a distinction between actual and potential truth of a proposition, roughly defined as follows: ... that a proposition A is actually true means ...
0
votes
2answers
31 views

Extension of a Signature

I came across the following rule about signature extension in Harper's 1993 classical paper on LF (see page 5, Figure 1). $$\frac{\Sigma:sig\quad\vdash_\Sigma A:Type\quad c\not\in dom(\Sigma)}{\Sigma,...
2
votes
2answers
79 views

Is it possible to show $(\lnot p \implies p) \implies p \vdash (\lnot \lnot p \implies p)$ in constructive logic?

I was given the task of showing that $(\lnot p \implies p) \vdash p$ cannot be proven in constructive logic (that is, a system with no excluded middle, double negation, or $\lnot$-elimination). I'm ...
2
votes
0answers
48 views

Context and Variable Declaration

I am a beginner in type theories. I have a basic question about the notion of context. It is commonly found in a textbook on type theories that a context (sometimes also called an environment) is ...
3
votes
2answers
136 views

Are geometric arguments using infinitesimals valid?

This question pertains to smooth infinitesimal analysis as presented in the book A Primer of Infinitesimal Analysis by John Bell. The book uses intuitionistic logic. Let $\Delta$ denote the set of ...
1
vote
0answers
63 views

Necessity of decidable type checking for formalizing mathematics

If a type theory such as Martin-Löf's dependent type theory (MLTT) is to be used as a foundation for mathematics, decidable type checking is certainly nice to have: it guarantees that for every proof ...
10
votes
0answers
196 views

Constructive proof of approximate Brouwer's Fixed Point Theorem for $\Delta^n$ via Sperner's lemma

Brouwer's Fixed Point Theorem (BFPT) is not provable in Bishop-style constructive mathematics (BISH). For quick orientation, BISH is obtained from classical mathematics by removing the Law of Excluded ...
1
vote
1answer
67 views

Context in Type Theory

I am reading a book on type theory. On page 105, the author says that If one views valid contexts as theories (in the sense of ordinary logics) a consistent context corresponds to a consistent ...
3
votes
1answer
63 views

Given an inhabited type in simply-typed lambda calculus (w/no basics, just variables), is there a combinator of that type that is no longer than it?

Apologies if I've got some of the terminology here wrong, typed lambda calculus is a bit new to me. Let's say we've got a type in simply-typed lambda calculus with no basic types (functions and type ...
2
votes
1answer
57 views

Universal Quantifier in Intuitionistic Logic

I have a very basic question about $\forall$ in intuitionistic first-order logic (IQL). It is well-known that in intuitionistic propositional logic (IPL), (\ref{dnlem}) and (\ref{dndne}) are both ...
0
votes
1answer
58 views

Non-existence of a dischargeable hypothesis

I meet a question about the existence/non-existence of a dischargeable hypothesis. The question is as follows: in intuitionistic logic, if for every proposition $X$, it cannot be the case that $X$ ...
0
votes
0answers
119 views

Is it true that computability = constructivism + law of excluded middle?

It seems to me that (classical) computable mathematics and constructive mathematics follow roughly the same program, i.e. only working with objects which can explicitly be constructed (by an algorithm,...
2
votes
2answers
70 views

Constructive proof of secure hash collision

The SHA3-512 hash algorithm can be considered as a map h from the set F of "files" (finite sequences of octets, each octet being an integer in the range 0 to 255) to the set H of "hashes" (sequences ...
2
votes
2answers
82 views

Is $\{x : x \in \mathbb{R} \land (x \ge 0 \lor x < 0) \} \neq \mathbb{R}$ provable in a constructive setting?

The main thing I'm trying to figure is whether (101) itself is a theorem in a constructive setting, whether it is a meta-theorem, or something else. Andrej Bauer's lecture The Five Stages of ...
8
votes
1answer
422 views

Examples of co-implication (a.k.a co-exponential)

In Dual Intuitionistic Logic and a Variety of Negations: The Logic of Scientific Research Yaroslav Shramko, inspired by Popper, makes an interesting case that co-constructive logic as the logic of ...
0
votes
0answers
33 views

Constructive total inverse function 1/x : R -> R

In constructive mathematics, if we define the real numbers by the quotient of Cauchy rational sequences, then all total constructive functions $f:\mathbb{R}\to\mathbb{R}$ must be continuous. Therefore ...
1
vote
0answers
80 views

Is Physics a Good Argument for Classical Math

(I posted this on philosophy stackexchange as well. Let me know if it belongs there more than here.) Is the success of classic mathematics in predicting the outcome of experiments in our physical ...
1
vote
1answer
25 views

Accessibility relation in non-classical logics: hereditary or not?

Recently, I am reading course materials on intuitionistic and modal logics. I have two questions about the notion of accessibility relation in Kripke semantics for intuitionistic and modal logics. ...
2
votes
1answer
47 views

Definition of proposition in a constructive setting

In a typical discrete math course, we are taught that a proposition is something that is either true or false but not both, which seems to be based on a classical interpretation. How would one go ...

1
2 3 4 5
9