二階述語論理学のタブロー法における例化
お断り
本項は，基本的なタブロー法の操作に習熟した読者を対象としているから，タブロー法において相当に親しまれた用法については特に説明せずに用いる。
特殊な凡例
述語変項：X
述語定項：F
個体変項：x₁,x₂,……
個体定項：a₁,a₂,……
個体記号：t₁,t₂,……
ここでは以上を特に記号と総称する
記号◯を含んだ論理式：A[◯]
A[◯]に現れる全ての◯を，記号●に置換した論理式：A[◯▶︎●]
要旨
引用したテクストでは，「私たちの表記法では，この〈同一あるいは差異〉という関係を，さっきの「a と同一である」の場合のように１つの述語定項であるかのように表すことはできない」として，ややアドホックなニュアンスを醸しながらもこれを解決している。
本項は，二階述語論理学のタブロー法における例化を次のように形式化することで，もっと統一的な説明を目指すものである。
例化規則
普遍例化
∀X(……Xt₁,t₂,……,tn……) の形をした論理式があるとき，その枝の先端に (……A……) を加える。A は，t₁,t₂,……,tn にある全ての個体記号の現れを含み，t₁,t₂,……,tn にない個体記号の現れを含まない，任意の枝分かれタイプの論理式である。
存在例化
∃X(……Xt₁,t₂,……,tn……) の形をした論理式があるとき，その枝の先端に (……A……) を加える。A は，t₁,t₂,……,tn にある全ての個体記号の現れを含み，t₁,t₂,……,tn にない個体記号の現れを含まない，その枝にまだ登場していない枝分かれタイプの論理式である。
付論
述語論理学における x=y は，ひっきょう Exy: x と yは同値だ，という述語記号の中置記法にすぎない。むろん両項は互いに可換旨の規則はよく導入されるが，これも前置記法にしたところで依然として可能であるから，先の定義では ∀R.¬Rab から ¬(a=b∨a≠b) を導出したことの説明が付かないと考えるのは誤りである。
∀R.¬Rab から ¬(a=b∨a≠b) を導出したことの実態は，∀R.¬Rab から ¬(Eab∨¬Eab) を導出したということであるから，これは先にした普遍例化の定義に反する操作ではない。