20 votes
Accepted

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

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 ...
  • 26.8k
11 votes

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

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 ...
  • 13.3k
9 votes

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

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

Can programming help one understand constructive mathematics?

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 ...
  • 231
7 votes
Accepted

Implementing "Internal" Languages

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 ...
  • 1,910
6 votes

conversion to DAG

This problem is equivalent to feedback arc set (in a tournament graph). It is NP-hard.
  • 1,432
6 votes
Accepted

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

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{...
  • 26.8k
6 votes
Accepted

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

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,...
5 votes
Accepted

Equality of decidable proofs?

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 ...
  • 26.8k
5 votes

Implementing "Internal" Languages

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 ...
  • 26.8k
5 votes

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

[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-...
4 votes

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

$\let\eq\leftrightarrow$Based on the comments, I’m interpreting the argument of $\psi$ as a “nullary predicate”. You can define $I$ by the formulas $$\begin{align*} I(n)&\iff\exists W\,((0\in W\eq\...
4 votes

About the decidability of sets enumerated in non decreasing order

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(...
  • 26.8k
4 votes

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

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

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

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 ...
  • 2,874
3 votes

Is just one W-type enough for formalizing mathematics?

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 ...
  • 26.8k
2 votes
Accepted

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

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 ...
  • 1,157
2 votes

Can programming help one understand constructive mathematics?

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....
  • 7,090

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