"Zooming down the slippy slope" George Boolos

"Logic Logic Logic" p354-364

Soritie Paradoxの変種の"Wang's paradox"（「すべての自然数は小さな数である」）において、数学的帰納法を使わずとも、任意の自然数nに対して、nが「小さい」ことを証明できるというのは有名な話である。では、例えば1000000が「小さな数」であることを証明するのに、何回推論をすればいいのか？私は1000000回強必要だと思っていたが、強い証明力のある体系(PAとか、ほかにもMateのnatural deduction的な体系とか)では、70回ぐらいで証明できる！つまり、

1. ０は小さい数である
2. １は小さい数である
3. ２は小さい数である
4. ４は小さい数である
5. ８は小さい数である
6. etc.

と２のn乗でやっていけばよい。こういう風に、Wang paradoxにおける証明の複雑さと証明の長さの話につなげる。Boolos本人はたぶん、計算の実行可能性を使って「小さな数」を定義しようとしていたのかもしれないが、Mateの体系では強力すぎてすべての自然数が「小さな数」であることを簡単に証明できてしまう（n<2^kに対しck^2のオーダーの証明の長さになる）のであった。残念。