>>428-430
>　どこから一階論理が出てきた？
>　ゲーデルの不完全性定理は自然数論の定理だよ　分かってる？　

いい質問ですね
その答えは下記です
１）一階述語論理は、単純で扱いやすい。基礎論向きだが、表現力に問題あり
２）「近年、二階述語論理は一種の回復の途上にある」下記
　（二階述語論理の問題点をおさえて、使える論理を作ろうと。「計算複雑性理論への応用」があるらしい）

なお、私見だが普通人は数学を、一階述語論理そのものでは考えていないと思う
ただ、論文を書くときは、一階述語論理を主に使うのだが、しかし厳密な一階述語論理に縛られない
グロタンディークは、それじゃない？ 「おれ、一階述語論理には縛られないぞ」じゃないかな？

(参考)
https://ja.wikipedia.org/wiki/%E4%B8%80%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
一階述語論理（英: first-order predicate logic）
本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細はそれぞれの記事を参照。

一階述語論理の表現力
一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 ZFC は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。すなわち、数学の命題は一階述語論理の論理式によって記述することができ、そのように論理式で記述された数学の定理には ZFC の公理からの形式的証明 (formal proof) が存在する。このことが一階述語論理が重要視される理由の一つである。この他にペアノ算術のように単独で形式化する理論もある。

形式的証明
命題論理においては、論理公理 (logical axiom) と呼ぶ論理式の集合と、ある論理式たちから新たな論理式を導出する規則（推論規則）を導入し、論理公理から推論規則の有限回の適用によって得られる論理式全体とトートロジー全体が一致するようにすることができる（命題論理の健全性と完全性）。一階述語論理においても、適切に論理公理と推論規則を導入することで、論理公理から推論規則を使って導出される論理式全体と恒真論理式全体が一致するようにできる。

健全性と完全性
古典一階述語論理は健全かつ完全である

つづく