＊ 任意の命題を証明するアルゴリズムは無い。

この前提となっているのは、「アルゴリズム」として、
有限長のものをどんな命題にも先立って与えるとしたら、
ということです。
命題を与えられてからそれを観た後であれこれとアルゴリズムを
生成していって、一般には有限個とは限らずに無限のアルゴリズム
列を作っていきながら判定を試みるというやり方であれば、
どうなるのかについては証明法の範囲外であると思います。
（この場合、「アルゴリズム」の列全体は可算ではないのです）