I love Dijkstra's writing, but I don't think this is his strongest piece. In general parlance, when we say "by piegonhole" we mean "any variant of it". I'd still call what he's doing "piegonhole" lol. You can even further generalize it, e.g. by making expected value arguments.

This is not uncommon: we can say that "by the fundamental theorem of algebra" two polynomials of degree N that agree on N+1 points are identically equal. "By induction" includes Cauchy induction, sometimes with "this and that are the same" we mean "up to isomorphism" and so on.

The advice he ends on is extremely solid, though:

  The moral of the story is that we are much better off with the neutral, general standard procedure: name the unknown(s) so that you can formalize all conditions given or to be established and simplify by formula manipulation.

Wow. I thought the metaphor was stupid when I was taught this in college, and only now, decades later, I find out Dijkstra agreed.

The first time I saw the Pigeonhole Principle was in the following:

Problem: A plane has every point colored red, blue, or yellow. Prove that there exists a rectangle whose vertices are the same color.

Solution: Consider a grid of points, 4 rows by 82 columns. There are 3^4=81 possible color patterns of columns, so by the Pigeonhole Principle, at least two columns have the same color pattern. Also by the Pigeonhole Principle, each column of 4 points must have at least two points of the same color. The two repeated points in the two repeated columns form a rectangle of the same color. QED.

The Pigeonhole Principle is very neat. It would be hard not to use it for the proof.

Partly that article argues against proof by contradiction which does seem to be overused.

That's par for a field whose name seems to have been inspired by "reverse-engineering", which by construction doesn't try to understand products that have not yet reached the market :)

I couldn't see any citations or references in that video or its description. It presents it as him solving the problem himself, but I'm sure other people have written about solving the Game of Life in reverse with SAT solvers prior to this...

Edit: here's a paper on it from 2006, https://link.springer.com/chapter/10.1007/978-3-540-76928-6_...

You’re right on the money. It’s intimately tied to computability theory, complexity theory’s more abstract sibling (I.e. the Halting problem and further Turing degrees). Both rely on the core techniques of diagonalization and reductions. The meat of it can differ a lot because estimating time bounds and determining logical equivalence rapidly become different problem spaces, so it’s not like results in one are really applicable to the other. But a researcher in one will usually be well versed in the other.

I would say that's on the wrong track and that "hard" is the wrong term for what reverse math (RM) tells you about problems. RM studies what axioms you need to prove a given theorem, but it's more like showing that "to pound in a nail of size X you need a hammer of size Y and a smaller hammer just can't do it", than saying pounding in the nail is difficult or complicated. Once you have the big enough hammer, pounding the nail can be very simple.

I'm not sure if you're just choosing intentionally obtuse verbiage or if you're actually saying something completely incoherent.

"Overall Complexity" is a meaningless term without you defining it. I suppose you mean that there is some lower bound limit to the amount of work relative to a model of computation, but this is a trivial statement, because the limit is always at least no work.

We have many problems where we don't know the least upper bound, so even an interesting formulation of your idea is not necessarily true: work need not be conserved at the least upper bound, because reaching the bound may not be possible and epsilon improvement might always be possible.

Finally, algorithmic complexity is the wrong analogy for reverse mathematics anyway.

> Complexity of traveling salesman problem depends on what you consider as the problem space - number of cities or number of connections between cities.

lmao what?