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.

Filter by
Sorted by
Tagged with
1
vote
0answers
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 ...
3
votes
1answer
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 ...
2
votes
1answer
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 ...
0
votes
1answer
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$ ...
0
votes
0answers
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,...
2
votes
2answers
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 ...
2
votes
2answers
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 ...
8
votes
1answer
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 ...
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
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 ...
1
vote
1answer
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. ...
2
votes
1answer
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 ...
3
votes
2answers
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 ...
7
votes
1answer
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 ...
1
vote
1answer
118 views

Constructive proof of Gödel's incompleteness theorem

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 $\...
1
vote
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 ...
2
votes
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)=\...
8
votes
1answer
85 views

About Gödel-Gentzen negative translation

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 ...
2
votes
1answer
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 ...
3
votes
1answer
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 ...
4
votes
2answers
70 views

How do we prove intuitionistically that free modules of finite rank are projective?

I'm struggling to understand how the following proof can be intuitionistically valid$^1$: Theorem. Let $R$ be a commutative ring. A free module of finite rank $R^n$ is projective. Proof. Let $...
0
votes
1answer
65 views

Constructively founded set of axioms for real analysis

Is there a workable set of axioms for doing real analysis and for which it is proven that there is a model in one of the better researched constructive foundational theories (e.g. CZF or IZF set ...
1
vote
2answers
106 views

Computational intuition on discontinuity

I'm trying to understand what continuity, as in topology, intuitively is. The thing that got me thinking is that, it seems usually hard to define functions that are discontinuous. In other words, most ...
4
votes
0answers
86 views

self-contained vs. non-self-contained notions of realizability

There seem to be two notions of realizability in literature, where in one case the realization of a formula is fully self-contained with respect to providing a proof object for the given formula, ...
6
votes
1answer
104 views

Why is the axiom of countable choice constructively valid?

I am reading Andrej Bauer's Five stages of accepting constructive mathematics. Theorem 1.3 proves that the axiom of choice implies excluded middle. Shortly afterwards Bauer implies that the axiom of ...
4
votes
1answer
141 views

Results on forcing extensions for models of CZF

I regard the research on models of ZFC, forcing extensions and related subjects as pretty promising with respect to coping with the incompleteness of ZFC. However, for certain applications I find ...
0
votes
2answers
63 views

What does a negative superscript mean on a positive Integer number

I am reading Foundations of Constructive Analysis by Errett Bishop. In the first chapter he describes a particular construction of the real numbers. There is a intermediate definition before his ...
3
votes
1answer
62 views

What does intuitionism/constructivism say about this proof?

The Wikipedia article on Euler's totient function lists, in the Growth rate section, the following: $$\varphi(n)<\frac{n}{e^\gamma\log\log n}\quad\text{ for infinitely many }n$$ and says: "The ...
2
votes
1answer
163 views

The free monad over an endofunctor on $\mathcal{Set}$

Let $F$ be an endofunctor on the category $\mathbf{Set}$. How can I construct the free monad over $F$? Can this construction be generalized to other categories than $\mathbf{Set}$?
7
votes
1answer
137 views

Understanding the justification for Troelstra's Uniformity Principle

I'm trying to understand Troelstra's uniformity principle (UP), as laid out in McCarty's article ''Intuitionism in Mathematics'' from the Oxford Handbook of the Philosophy of Mathematics and Logic. ...
0
votes
1answer
61 views

Constructive mathematics plus existence of discontinuous functions

Bishop's constructive mathematics (BISH) is meant to be the intersection of the theories of Brouwer, early Recursion Theory, and classical mathematics, and so it can be modelled by any model for the ...
0
votes
0answers
39 views

How HSAT (Heyting satisfiability) can be proven to be PSPACE-COMPLETE if not every intuitionistic formula has disjunctive or alternative normal form?

There's a proof in R. Statman, Intuitionistic propositional logic is polynomial-space complete. Is it constructive? Would that be possible to formulate HSAT without reffering to second order classic ...
2
votes
1answer
67 views

Undecidability of constructive provability

The paper A Lightweight Double-negation Translation states "However, as not all classical theorems are provable constructively – this question is even undecidable..." Can someone provide me with a ...
2
votes
1answer
54 views

Does constructive dilemma hold in intuitionistic logic?

I mean this law: $ (( p \Rightarrow r) \wedge (q\Rightarrow r) \wedge (p \vee q)) \Rightarrow r$ It seems to me that it does hold for INT. Is there any non-esoteric logic that excludes that law?
0
votes
1answer
84 views

$A \rightarrow \neg \neg A$ in constructive logic with and without explosion

I have been reading about constructive logic and I also recently became aware of minimal logic. My understanding of minimal logic is not clear, and I don't get how it is defined, or what suffices as a ...
2
votes
1answer
92 views

Does the notion of logical independence make sense in constructive mathematics?

I have been learning a bit about constructive mathematics and intuitionistic logic and I think I am correct in understanding that a philosophical difference between constructive and classical logic is ...
1
vote
1answer
56 views

Constructive and Non-constructive Proofs of Proposition

I was reading the wikipedia page for "constructive proof" and I have a question about something one of the authors says in the section "Examples" where two proofs are juxtaposed for the assertion that ...
5
votes
0answers
122 views

How much of the Cantor-Schröder-Bernstein theorem is constructively recoverable if the injections have retractions and decidable images?

I have also cross-posted this question to MO, where it has now been answered. Suppose we have $f : A \to B$ and $g : B \to A$, as well as left inverses $f_r : B \to A$ of $f$ and $g_r : A \to B$ of $...
0
votes
2answers
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 ...
3
votes
2answers
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 ...
0
votes
2answers
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 ...
3
votes
1answer
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 ...
0
votes
1answer
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 ...
2
votes
2answers
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 ...
3
votes
1answer
94 views

Relation between classical implication and intuitionistic implication

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\...
1
vote
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 ...
1
vote
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"...
0
votes
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<...
0
votes
1answer
82 views

Minimum number of splits graph into two sets to delete all edges.

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 ...
3
votes
1answer
85 views

Ultrafilter principle and Axiom of Dependent Choice as 'nonconstructive and constructive' components of the Axiom of Choice

As in the title, in the book 'Handbook of Analysis and its Foundations' by Schechter, the Ultrafilter principle is presented as a nonconstructive component of the Axiom of Choice, while the Axiom of ...

1
2 3 4 5
9