19

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician. To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc: We provide a function $f$ which ...


19

You must be careful here. You are using set-theoretic concepts (cardinal, continuum) outside set theory. There is potential for confusion. Your question can be understood in several ways. Maybe you are asking whether there can be uncountably many terms of a given type. The answer is: obviously not since there are only countably many finite strings, and ...


15

This is the same idea as Andrej's answer but with more details. Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. ...


11

This example is a bit lower in the hierarchy than what Kaveh asks for, but it is an open problem whether the soundness of the uniform $\mathrm{TC}^0$ algorithms for integer division and iterated multiplication by Hesse, Allender, and Barrington can be proved in the corresponding theory $\mathit{VTC}^0$. The argument is pretty elementary, and there should be ...


10

The AKS primality test seems like a good candidate if Wikipedia is to be believed. However, I would expect such an example to be hard to find. Existing proofs are going to be phrased so that they are obviously not done in bounded arithmetic, but they will likely be "adaptable" to bounded arithmetic with more or less effort (usually more).


9

As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is equiconsistent with intuitionistic logic (say, Heyting Arithmetic) has been known for quite some time (already in 1933, e.g. Godel) using a double negation translation. By a more sophisticated argument, it can be shown that Peano ...


8

I agree with both Andrej's and Cody's answer. However, I think it is also worth mentioning why constructivists should care about control operators (call/cc). These operators are usually connected to classical logic because when people looked at their typing rules (Felleisen, Griffin) they noticed that the types have the form of Peirce's Law or double-...


8

Intuitionistic negation is perfectly constructive, because $\lnot A$ is simply an abbreviation for $A \to \bot$ (i.e., "A implies false"). You may be thinking of the principle of double-negation elimination (i.e, $\lnot\lnot A \to A$). This principle is indeed nonconstructive. The reason we call intuitionistic logic constructive is that existentials and ...


8

Agda is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are written as recursive functions with multiple equations that pattern match on the function arguments. So programming and/or proving in Agda is a good way to learn ...


8

I would like to elaborate on Kaveh's answer because I see people wondering about the constructive status of $P = NP$. Levin's algorithm performs a dove-tailing parallel execution of all Turing machines on the given SAT instance. If and when any machine terminates, it is verified whether its output is a solution to the SAT instance. If so, Levin's algorithm ...


7

It is is worth thinking about WHY intuistionistic logic is the natural logic for computation, since all too often people get lost in the technical details and fail to grasp the essence of the issue. Very simply, classical logic is a logic of perfect information: all statements within the system are assumed to be known or knowable as unambiguously true or ...


7

In Extending Type Theory with Forcing by Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, implemented as a type-preserving translation in the style of Bernardy and Lasson's parametricity translation. This means that you can define terms in your usual type ...


6

This problem is equivalent to feedback arc set (in a tournament graph). It is NP-hard.


6

It is not entirely clear what you mean by a nonconstructive proof of P=NP. I am guessing that you are asking if it is possible to prove that there is a polynomial time algorithm for SAT without providing one. That cannot be the case because we can prove that Levin's universal search algorithm for SAT has optimal running time, if P=NP is true (even if it is ...


6

As I said in the comments, intuitionist logic is not the main point. The more important point is having a constructive proof. I think Martin-Löf's type theory is much more relevant to programming language theory than intuitionistic logic and there are experts who have argued that Martin-Löf's work is the main reason for the revival of the general interest in ...


6

I don't understand exactly what you are looking for, I'll try to explain the Curry-Howard correspondence in a nutshell, you'll let me know if it helps. The Curry-Howard correspondence (or isomorphism, if you wish) definitely links the three objects you mention: it actually tells that two of them, IL and $\lambda$c, are the same thing. The term is used ...


5

As Neel points out if you work under the "propositions are types" then you can easily come up with a type whose equality cannot be shown decidable (but it is of course consistent to assume that all types have decidable equality), such as $\mathbb{N} \to \mathbb{N}$. If we understand "proposition" as a more restricted kind of type, then the answer depends on ...


5

If you're going to work only in the internal language then you can just use a proof assistant. There is a minor technicality of having or not having powersets, since proof assistants are typically type theories, but Coq's Prop is consistent with an interpretation of Coq in a topos. You're suggesting however to use the machine as a sort of translation tool ...


5

[Self-advertising follows, but I think that this is relevant.] There are several possible approaches to this questions. One of the ways (that I explored during my PhD thesis in the context of an ML-like language) is to extend the type system with a first-order layer, so that terms of the language can be manipulated as objects of the underlying logic. Of ...


4

Suppose there were a computable $f$ as described in the question. Then we could solve the Halting problem as follows. Given a Turing machine $T$, consider the computable function $g$, defined by $$g(k) = \begin{cases} 1 & \text{if $T$ halts in $\leq k$ steps} \\ 0 & \text{otherwise} \end{cases}$$ This is a computable, nondecreasing and total ...


4

Simple summary: Typed $\lambda$-calculi are a way of presenting intuitionistic logics. Combinatory logic is a presentation of logic (propositional, first-order, higher-order, intuitionistic or otherwise) without binders. Typed $\lambda$-calculi can easily be translated into combinatory logic. Some combinatory logics can easily be translated to typed $\...


3

Real-world cryptographic hash functions like MD5 & SHA are keyless. As such, it makes it quite difficult to apply techniques from theoretical cryptography to reason about their security. The simple reason why: for any keyless hash function, there exists a very small program/adversary which outputs a collision under that hash function; namely, a program ...


3

Intuitionistic logic is not symmetric regarding truth and falsity. There primary notion in intuitionistic logic is constructive truth and proofs not constructive falsity and refutation: a statement is true if there is a proof for it. And then we discuss various ways of constructions of proofs. We don't discuss when a statement is false or how to construct a ...


3

Let me offer the simple, intuitive way that I think about this. If you restrict yourself to closed lambda expressions, you have an equivalent of the combinatory logic. In fact with just a few simple closed lambda expressions you can generate all the others. Closed lambda expressions give you the equivalent of implications where any conclusion/output you ...


2

Let me first state that I'm not sure what are you getting at, I'm not sure how linearity/affinity is relevant. I'll answer the question in 'standard' setting. How would you define how to compare two infinite types lazily? It seems to me that it can't be done automatically since they can eventually diverge. [Checking for nominal equality ("pointer ...


2

Maybe take a look at the textbook Software Foundations, which uses the proof assistant Coq. I don't think the focus is really on "learning constructive math", but it does develop the programming tools. On the other end of the spectrum is the Homotopy Type Theory Book, which is very theoretical about constructive math, but doesn't include programming per se (...


Only top voted, non community-wiki answers of a minimum length are eligible