構成的と言えば

中学あたりで習う、背理法で証明できる初等的命題として、「sqrt(2)は無理数」ってのと、「素数は無限個ある」ってやつがあるけど、背理法使わずに初等的に証明するには、どうすればいいのだろう。論理式で書くと、以下のような感じか

(forall (p) (forall (q) (-> (= (* 2 (* p p)) (* q q)) (and (= p 0) (= q 0)))))

(forall (n) (exists (p) (and (< n p) (prime? p))))

素数の方は、丁度(forall (x) (exists (y) (P x y)))の形になってるけど、これの初等的な証明はちょっと思いつかない。

#述語prime?は、素数なら真、非素数なら偽を返す
#解析的なのでよければ、ゼータ関数がs=1で発散するというのでいいんだろうけど