# Questions tagged [constructive-mathematics]

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.

415 questions
Filter by
Sorted by
Tagged with
26 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 ...
48 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 ...
37 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 ...
40 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$ ...
96 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,...
65 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 ...
68 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 ...
279 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 ...
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 ...
69 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 ...
20 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. ...
39 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 ...
63 views

### Is there a constructive proof of this characterisation of convergence of sequences?

The following is a useful characterisation of convergence for sequences in $\mathbb R$: A sequence $(a_n)$ converges to $a$ if and only if every subsequence $(a_{n_k})$ of $(a_n)$ has a subsequence ...
68 views

### Interpretations of Topological Space as a Heyting Algebra

I have recently learned about Heyting algebras which I find quite fascinating, as I am more intuitionistically inclined. One of the main examples of Heyting algebras are given by topological spaces as ...
118 views

Gödel's first incompleteness theorem states that if a consistent theory $T$ extends Peano arithmetic, then there is an explicit formula $\Delta_T$ in the language of arithmetic, that is true in $\... 1answer 62 views ### proving mathematical induction by recursion in type theory? the principle of mathematical induction says: $$\forall P,\quad [P(0) \land\forall n, P(n)\to P(n+1)]\quad \to \quad \forall n, P(n)$$ The proof I've seen for this is by contradiction: Assume that ... 2answers 69 views ### Are constant functions continuous in constructive mathematics? The standard proof that a constant function$c: X \to Y$,$x \mapsto y_0$is continuous proceeds as follows: if$U \subseteq Y$is open, then either$c^{-1}(U)=X$if$y_0 \in U$, or$c^{-1}(U)=\...
85 views

I have a question about Gödel-Gentzen negative translation. According to the Wikipedia article for negative translations, "a sentence $\phi$ may not imply its negative translation $\phi^{\rm N}$". I ...
78 views

### What is the corresponding categorical notion to a non-functorial modality?

Consider the constructive logic with a modality with the following modal axioms: □(a → b) → □ a → □ b ...
46 views

### Term existence property for CZF

For Intuitionistic Zermelo Fraenkel (IZF) set theory, Moczydlowski ("Normalization of IZF with Replacements", 2008) proved that the Term Existence Property (TEP) holds, so if $\exists x. \phi(x)$ is ...
70 views

51 views

### Constructive proof that the sum of a rational and an irrational is irrational

I want to prove this constructively (ie, without using contradiction), and I tried to prove the contrapositive, that if a + b is rational then it can not be the case that WOLOG a is rational and b is ...
162 views

### Proof methods w/o Contradiction (Intuitionistic Frameworks of Math)

Regarding the standard formulation of the division algorithm: If $a,b$ are integers with $b > 0$, then there exists unique $q,r$ such that $a = bq + r$ with $0 \leq r < b$. The standard ...
64 views

### Multiplication with negative multiplier [duplicate]

Multiplication is often expressed as repeated addition. Such as $$5\cdot 3=5+5+5$$ $$-5\cdot 3=(-5)+(-5)+(-5)$$ Above in both the cases multiplier is positive.In case of multiplier is negative how ...
275 views

### Construct Permutation with longest arithmetic progression subsequence of predefined length

A subsequence of sequence A is a sequence that is obtained from A by removing several (zero or more) elements from it. Eg: {1,3,5}, {2,4},{ } are subsequence of sequence {1,2,3,4,5}. An arithmetic ...
71 views

### Are there statements which can be proven by contradiction but not constructively?

Brouwer and the intuitionist mathematicians denied that a proof by contradiction was valid. Is it demonstrable that certain proofs/theorems then become inaccessible, i.e. without using proof by ...
131 views

### ZF+DC as the boundary of constructive mathematics

This is mainly a request for references. I seem to recall hearing somewhere that ZF+DC is "the boundary of constructive mathematics" in the sense that theorems not provable from ZF+DC are ...
94 views

Recently, I have read an article on combining classical and intuitionistic implications. On page 9, in their Proposition 6, the authors say that $$A\Rightarrow((A\Rightarrow B)\rightarrow (A\... 0answers 96 views ### Is there a game semantical countermodel to Markov's Principle? For specificity, let's fix Markov's Principle as$$\forall P : \mathbb N \to 2. \neg(\forall n : \mathbb N. P(n) = 0) \to \exists m : \mathbb N. P(m) = 1.$$I've seen an informal argument that this ... 1answer 89 views ### Piecewise linear functions in constructive mathematics Is is possible to constructively prove that, for any function f:\mathbb{R}\to\mathbb{R} piecewise linear, the absolute value |f|:\mathbb{R}\to\mathbb{R} is also piecewise linear ? "Constructively"... 1answer 56 views ### Something missing in the definition of “doesn't hover”? Definition 1.4 of “A lambda calculus for real analysis” (Paul Taylor) says: Definition 1.4 We say that f:\Bbb R\to \Bbb R doesn't hover if,$$ \text{for any $e<t$,}\qquad \exists x.(e<x<...
You are given a graph with $N$ vertices and $M$ edges. For one operation you can divide vertex set into two sets. After each operation you delete all edges between vertices from different sets. The ...