PLP の述語
集合 (述語の項を表す)とブール代数
(PLPの結果の成功または失敗を表す)に対して
を(項の)述語と呼びます。
これを拡張して可算集合 (変数を表す)に対して
としたものも述語と呼びます。
有限個の述語の集合を とおきます。
の各元
に対して
という形のものの全体(各 は
の元)を
とおきます。
PLP の論理式
PLP の論理式全体の集合 を定義していきます。
の元は
の元となります。
と
が
の元ならば
、
、
は の元となります。
が
の元で
が
に現れる自由変数ならば
、
は の元となります。
以上を満たす最小のものを と定義します。
「 に現れる自由変数」をまだ定義していないので「
に現れる自由変数全体の集合
」を以下のように定義します。
、
、
、
、
、
。
が空集合のとき
を閉論理式と呼びます。
次に PLP の動作を証明と考えるために必要な証明の理論について考えていきます。