# Questions tagged [constructive-mathematics]

The tag has no usage guidance.

25 questions
Filter by
Sorted by
Tagged with
895 views

### Law of the Excluded Middle in complexity theory

A recent blog post by Lance Fortnow discusses non-constructive proofs, where "non-constructive" here means that the law of the excluded middle is used in a substantive way. That is, one ...
1k views

### Yet another constructive (Coq) proof that nat -> nat -> nat is not bijective. How to explain it to myself?

Here is a Coq proof I've came up with: ...
210 views

### Can you define recursive predicates in 2nd order intuitionistic logic?

This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here. Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) ...
143 views

### What is a known sequence for which being constant is not provable?

My question concerns the property of being constant for computable functions ${\mathbb N}\to \{0,1\}$, within any common framework $T$ strong enough to include Heyting arithmetic (and of course not ...
246 views

### Is just one W-type enough for formalizing mathematics?

We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics. Now if we ... 162 views

### Non-trivial existence proof in type theory

What are some examples of existence proofs in Coq/Agda etc., where the constructed natural number is useful from mathematical point of view, but it's non-obvious from the proof what it should be? I am ...
76 views

### Monotonic and bounded sequences throughout computer science

When I refer to the Monotone Convergence Theorem below, I refer to the very simple claim that if a non-decreasing sequence has an upper bound then it converges. I don't refer to the claim from Measure ...
133 views

152 views

### Is the church-style affine calculus of constructions with unrestricted recursion consistent?

Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example: ...
223 views

### Fast way of getting a matrix of sums

We are given an array of variables $A$, along with a matrix $M$. The elements of the matrix $M$ are composed of sums of the variables in $A$. We are allowed to pre-process $A$ in order to find a ...
342 views

### What makes a language (and its type-system) capable of proving theorems about its own terms?

I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded ...
1 vote
85 views

### Equality Theorems with Type Theoretic Proof

I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a ...
113 views

### Mathematical analogy to objects (as in object orientation)? [closed]

Data structures are similar to variables. Algorithms to functions. Objects combine both data and algorithms. Is there a mathematical object / concept that combines variables and functions?
613 views

### About the decidability of sets enumerated in non decreasing order

It is well known that a set of numbers enumerable in nondecreasing order is decidable. However, the typical proof, by cases on the finiteness of the enumerated set, is not constructive. In general, it ...
583 views

### Implementing "Internal" Languages

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured ...
1k views

### Why do constructivists not seem to care too much about call/cc

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
1k views

### What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the ...
919 views

### Equality of decidable proofs?

I want to know if the decidability of equality of two decidable proofs of the same proposition can be proved without any additional axioms in Calculus of Inductive Constructions. Specifically, I want ...
280 views

### Can programming help one understand constructive mathematics?

I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the ...
104 views

### Can I represent a computer program on a Hilbert Curve?

I overheard in discussion tonight: You know - you can represent a computer program as points on a Hilbert Curve. Is there a reference that explains this concept? I can't seem to Google for it.
649 views

### Why is intuitionistic negation nonconstructive?

Can someone simply describe why intuitionistic negation is not constructive and why intuitionistic proof is constructive? in intuitionistic logic the notion of falsity has a 'subordinate' ...
755 views

### Types which correspond to sets of cardinality of continuum

Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)? On the first sight, they aren't, since elements of types are terms and we ...
336 views

### SAT in some DTIME always via a constructive proof?

Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-...
I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t. their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but no proof using only ...