述語論理のタブロー法

先日のやつより、以下の量化子に対するタブロー規則が得られる。

• からが得られる。aは任意のパラメータでよい

• からTφ(a)が得られる。aはまだ使われてないパラメータでなければならない。

• F∀xφ(x)からTφ(a)が得られる。aはまだ使われてないパラメータでなければならない。

• F∃xφ(x)からTφ(a)が得られる。aは任意のパラメータでよい