# Tag Info

20

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 ...

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 ...

10

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

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 ...

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 ...

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

Let $T$ be a reasonble theory of arithmetic, say $\mathrm{PA}$. Consider the sequence $$f(m) = \begin{cases} 1 & \text{if m encodes a proof of \vdash_T 0 = 1} \\ 0 & \text{otherwise} \end{cases}$$ The sequence is clearly computable, even primitive recursive and therefore representable in $T$. If there is $m$ such that $f(m) = 1$ then $T$ is ...

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

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

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 ...

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 ...

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 $\... 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 ... 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 ... 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 We certainly do not need very many$W$-types. If we also have universes, we only need one$W\$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no other inductive types (if we discount the fact that standard types constructors, such as products and sum, are defined inductively in Coq).

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