Netscape open sourced to try and head off Internet Explorer as a 'last throw of the dice'? Chrome based originally on WebKit from Safari which was forked off KHTML from KDE's konqueror, came along years later.
I didn't know and not mentioned in the article is that there are two different programs in reverse mathematics, one relating to classical mathematics, the other relating to complexity questions. Claude says this: not sure about accuracy
Let me clarify the relationship between PV₁ and reverse mathematics systems, as there are actually two different research programs here:
Two Different Programs
1. Classical Reverse Mathematics (over RCA₀)
The standard reverse mathematics program, pioneered by Harvey Friedman and Stephen Simpson, works over second-order arithmetic and studies which set existence axioms are needed to prove theorems of ordinary mathematics. The main systems form the "Big Five":
RCA₀ (Recursive Comprehension Axiom)
WKL₀ (Weak König's Lemma)
ACA₀ (Arithmetic Comprehension Axiom)
ATR₀ (Arithmetic Transfinite Recursion)
Π¹₁-CA₀ (Π¹₁ Comprehension Axiom)
2. Bounded Reverse Mathematics (over PV₁ or similar)
This is a separate program studying computational complexity rather than computability. It analyzes which theorems require which computational resources.
And there's no clever trick you can do using eg hash functions or compression to shortcut the process? Of course the proofs that hash functions have collisions and there is no universal compression algorithm use the pigeonhole principle..
The shortcuts all revolve around the cases when the strings are different.
If we just do a zipper compare and the first pair of bits happens to differ, we are done, having looked at only two bits.
Similarly, we compute hash functions that sample only a small number of bits out of each string, and the hash codes don't match, we are done.
The worst case occurs when the strings turn out to be identical. We cannot make the correct verdict that the strings are identical without examining every bit; any bit we don't look at could be the same or different, and so we cannot announce a decision.
I wrote as my comment kind of as a rhetorical question, but perhaps in retrospect the connection between the string comparison problem the pigeonhole principle is not so surprising in the end.
