論理式

数理論理学

ゲーデルの不完全性定理をきちんとやるにあたっては、言語だのモデルだの証明だのをちゃんと定義していかないといけません。面倒だし、私の専門からも少々外れるので私自身うろ覚え気味なのですが。
数学で扱うのは論理式で記述できる事柄だけです。「神は存在するか」とかは他を当たってください。もっともこれはあながちばかげたこととも言い難く、例えばリシャールのパラドックスがなぜ数学に危機をもたらさないかと言えば、そこで使われている命題が論理式で記述できないからに他なりません。そのことはまたあとで。

以降、知っている人には常識かと思いますが、(一階述語論理における)論理式の定義を。

論理式で使われる記号の集合のことを言語といいます(正確じゃないけどいいでしょう)。それには、カッコ（）、等号＝、アンド∧、オア∨、implication⇒、同値⇔、などの論理記号と、x_1, x_2, \cdotsなどの変数記号はほぼ常に含まれます。それ以外に、定数記号c_1, c_2, \cdots、関数記号f_1, f_2, \cdots、関係記号R_1, R_2, \cdotsなどを含むことが出来ます。それぞれの関数記号と関係記号はいくつかの引数をとることが出来ます。これらは別にcやfでなければいけないわけではなく、単に慣習としてこれらの文字を使うことが多いというだけです。
論理式を定義する前に、まず項を以下のように定義します。

  1. 全ての変数記号及び定数記号は項である
  2. fがn変数の関数記号であり、t_1, t_2, \cdots, t_nが項であるとき、f(t_1, t_2, \cdots, t_n)は項である
  3. これらのルールで定まるもののみが項である

えーと。いまいち気持ち悪い定義なんですが、これが標準のようです。まあ、帰納的に定義したい方はご自由に。
項が定義できたあとでは、論理式は以下のように定義できます

  1. t_1, t_2が項であるとき、t_1=t_2は論理式である
  2. Rがn変数の関係記号であり、t_1, t_2, \cdots, t_nが項であるときは、R(t_1, t_2, \cdots, t_nは論理式である
  3. \varphi, \psiが論理式であるとき、\varphi\wedge\psi、\varphi\vee\psi、\varphi\Rightarrow\psi、\varphi\Leftrightarrow\psiはいずれも論理式である
  4. \varphiが論理式であり、vが変数であるとき、(\exists v)\varphiと(\forall v)\varphiは論理式である。
  5. これらのルールで定まるもののみが論理式である

いまいち気持ちが悪(以下略)

…というところまで昔書いたので、とりあえず貼っておきます。やりたいのは、モデル論的に見た数学と、証明論的に見た数学の違いについてちょっと語るってことなんですが。