The liberalized \(\delta\)-rule in free variable semantic tableaux (Q1344882)

The liberalized \(\delta\)-rule in free variable semantic tableaux is studied. This rule was presented by Smullyan. The authors consider a modification of this rule, called the \(\delta+\)-rule, which uses fewer free variables. The relationship between the \(\delta+\)-rule and variations of the \(\delta\)-rule is studied. The problem lies in proving the correctness of the \(\delta+\)-rule. The main result (soundness) is the following: If a sentence \(X\) has a closed tableau \(T\) constructed with \(\delta+\), then \(X\) is not satisfiable.