18 votes
Accepted

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

First, let me say that "constructive" does not imply "all maps are Turing computable". It means “no excluded middle and axiom of choice were used“. In constructive mathematics the ...
Andrej Bauer's user avatar
  • 28.8k
12 votes
Accepted

Law of the Excluded Middle in complexity theory

There are several other non-constructive arguments that work along similar Karp-Lipton-esque lines, such as Santhanam's proof (STOC 2009) that $PromiseMA$ is not in $SIZE(n^k)$ for some $k$, and ...
Ryan Williams's user avatar
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 ...
gasche's user avatar
  • 2,040
6 votes

conversion to DAG

This problem is equivalent to feedback arc set (in a tournament graph). It is NP-hard.
Laakeri's user avatar
  • 1,767
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{...
Andrej Bauer's user avatar
  • 28.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 ...
Andrej Bauer's user avatar
  • 28.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-...
Rodolphe Lepigre's user avatar
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\...
Emil Jeřábek's user avatar
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(...
Andrej Bauer's user avatar
  • 28.8k
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 ...
Andrej Bauer's user avatar
  • 28.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 ...
Łukasz Lew's user avatar
  • 1,187
1 vote

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

To answer very directly: You have a constructive proof in Coq but it is not the case that the enum : nat -> nat is assumed (in Coq) to be computable. In a sense, ...
ezrakilty's user avatar

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