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 ...
- 29.4k
13
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 ...
- 27.5k
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{...
- 29.4k
6
votes
conversion to DAG
This problem is equivalent to feedback arc set (in a tournament graph). It is NP-hard.
- 1,881
5
votes
Law of the Excluded Middle in complexity theory
I finally managed to track down the paper that I was struggling to recall.
Why are Proof Complexity Lower Bounds Hard? by Ján Pich and Rahul Santhanam, FOCS 2019.
Their main result is:
Theorem 1. ...
- 7,580
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-...
- 321
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(...
- 29.4k
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\...
- 18.2k
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 ...
- 29.4k
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,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, ...
- 11
Only top scored, non community-wiki answers of a minimum length are eligible