一階述語論理
一階述語論理は、数学のほぼ全領域を形式化するのに十分な表現力を持っている。実際、現代の標準的な集合論の公理系 ZFC は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。すなわち、数学の命題は一階述語論理の論理式によって記述することができ、そのように論理式で記述された数学の定理には ZFC の公理からの形式的証明 (formal proof) が存在する。このことが一階述語論理が重要視される理由の一つである。この他にペアノ算術のように単独で形式化する理論もある。
M(∀x φ, s) = 1 ⇔ すべての m ∈ |M| に対して M(φ, s[x|m]) = 1 。 M(∃x φ, s) = 1 ⇔ ある m ∈ |M| に対して M(φ, s[x|m]) = 1 。 ただし、s[x|m] は変数 x には m を割り当て、x 以外の変数に対しては s と同じ個体を割り当てる関数を表す。
M(φ, s) = 1 であるとき M は s によって φ を充足するという。
特に φ が文である場合は、すべての個体の割り当て関数 s に対して M(φ, s) = 1 であるか、すべての個体の割り当て関数 s に対して M(φ, s) = 0 であるかのいずれかであることが示される。そこで、前者の場合に φ は M において真であるといい、後者の場合に φ は M において偽であるという。すなわち、構造 M と文 φ に対して、
φ は M において真 (true) ⇔ 任意の M の個体の割り当て関数 s に対して、M(φ, s) = 1 。
φ は M において偽 (false) ⇔ 任意の M の個体の割り当て関数 s に対して、M(φ, s) = 0 。
と定義する。φ が M において真であるとき、M は φ のモデル (model) であるともいう。また、M が文の集合 Σ のすべての要素のモデルであるとき、単に M は Σ のモデルであるという。
モーダス・ポーネンスとは、φ と (φ → ψ) から ψ を導出してよいという規則である。これは、論理式全体の集合の上の関係としては次のように定義することができる:
MP = { (φ, (φ → ψ), ψ) | φ と ψ は論理式 } 。
(φ1, φ2, φ3) ∈ MP であるとき、φ3 は φ1, φ2 からのモーダス・ポーネンスによる導出であるという。
x 1 {\displaystyle x_{1}} , x 5 {\displaystyle x_{5}} , 0 {\displaystyle 0} , S x 1 {\displaystyle Sx_{1}} , S 0 {\displaystyle S0} , S S 0 {\displaystyle SS0} , + S 0 S 0 {\displaystyle +S0S0} , + 0 x 5 {\displaystyle +0x_{5}} , ⋅ S x 1 + 0 x 5 {\displaystyle \cdot Sx_{1}+0x_{5}}
はすべて項である。 + S 0 S 0 {\displaystyle +S0S0} や + 0 x 5 {\displaystyle +0x_{5}} といった前置記法は読みにくいため、これらの項を表すのに、通常使われている S ( 0 ) + S ( 0 ) {\displaystyle S(0)+S(0)} や 0 + x 5 {\displaystyle 0+x_{5}} のような表現(中置記法)が用いられることもある。したがって ⋅ S x 1 + 0 x 5 {\displaystyle \cdot Sx_{1}+0x_{5}} は中置記法では S ( x 1 ) ⋅ ( 0 + x 5 ) {\displaystyle S(x_{1})\cdot (0+x_{5})} のように表される。