# Tag Info

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

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

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

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

### conversion to DAG

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

• 14.9k

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

### 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 ...
• 10.4k

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

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