一階述語論理
φ {\displaystyle \phi } が論理式で x {\displaystyle x} が変数ならば、 ( ∀ x φ ) {\displaystyle (\forall x\phi )} , ( ∃ x φ ) {\displaystyle (\exists x\phi )} は論理式である。
上記の 1. と 2. と 3. によって論理式とされるものだけが論理式である。
例. 再び自然数論の言語を考える。定義から、
[ ( S 0 + S 0 ) = S S 0 ] {\displaystyle [(S0+S0)=SS0]} , [ ( 0 + x 5 ) = S 0 ] {\displaystyle [(0+x_{5})=S0]}
はすべて原子論理式(したがって論理式)であり、
{ ¬ [ ( S 0 + S 0 ) = S S 0 ] } {\displaystyle \{\lnot [(S0+S0)=SS0]\}} , { [ ( 0 + x 5 ) = S 0 ] ∧ [ ( S 0 + S 0 ) = S S 0 ] } {\displaystyle \{[(0+x_{5})=S0]\land [(S0+S0)=SS0]\}} , { ∀ x 5 [ ( 0 + x 5 ) = S 0 ] } {\displaystyle \{\forall x_{5}[(0+x_{5})=S0]\}} , { ∃ x 2 [ ( 0 + x 5 ) = S 0 ] } {\displaystyle \{\exists x_{2}[(0+x_{5})=S0]\}}
Σ を論理式の集合とし、φ を論理式とする。Σ に属するすべての論理式 ψ に対して M(ψ, s) = 1 であるような任意の構造 M と M の個体の割り当て関数 s が M(φ, s) = 1 をみたすとき、φ は Σ の論理的帰結 (logical consquence) であるといい、 Σ ⊨ φ {\displaystyle \Sigma \vDash \varphi } と書く。論理式 φ と ψ が { φ } ⊨ ψ {\displaystyle \{\varphi \}\vDash \psi } かつ { ψ } ⊨ φ {\displaystyle \{\psi \}\vDash \varphi } をみたすとき、φ と ψ は論理的に同値 (logically equivalent) であるという。また、φ が ∅ の論理的帰結である場合、すなわち任意の構造 M と M の個体の割り当て関数 s に対して M(φ, s) = 1 であるとき、φ は恒真 (valid) であるという。φ と ψ が論理的に同値であることは、(φ ↔ ψ) が恒真であることと同値である。
このようなとき、 x 5 {\displaystyle x_{5}} は論理式 ( 0 + x 5 ) = S 0 {\displaystyle (0+x_{5})=S0} における自由変数 (free variable) であると言われる。正式には、各論理式 φ {\displaystyle \phi } に対して、" φ {\displaystyle \phi } における自由変数全体の集合" f r ( φ ) {\displaystyle fr(\phi )} を次のように再帰的に定義する:
φ {\displaystyle \phi } が原子論理式ならば、 f r ( φ ) {\displaystyle fr(\phi )} は記号列 φ に現れるすべての変数からなる集合である。
f r [ ( ¬ φ ) ] = f r ( φ ) {\displaystyle fr[(\lnot \phi )]=fr(\phi )} 。
f r [ ( φ ∧ ψ ) ] = f r [ ( φ ∨ ψ ) ] = f r [ ( φ ⇒ ψ ) ] = f r [ ( φ ⇔ ψ ) ] = f r ( φ ) ∪ f r ( ψ ) {\displaystyle fr[(\phi \land \psi )]=fr[(\phi \lor \psi )]=fr[(\phi \Rightarrow \psi )]=fr[(\phi \Leftrightarrow \psi )]=fr(\phi )\cup fr(\psi )} 。
推論規則とは、あるいくつかの論理式から別の論理式を導出するための規則である。これは正確には、論理式全体の集合の上の関係として定義される。推論規則には様々なものが考えられるが、ここで用いる推論規則はモーダス・ポーネンス (modus ponens) と呼ぶ規則と全称化 (generalization) と呼ぶ規則の二つである。