Example tableaux

The tableaux corresponding to the two informal proofs above are given below.

If you look at the corresponding informal proofs you’ll see some extra branching here, reflecting checks on whether various parameters actually refer to anything. They do, since they were introduced as names for things whose existence was asserted by an existential quantifier. In the informal proof this was regarded as so obvious that it didn’t require a comment, but in the tableau this gives rise to branches which we are able to close immediately.

As a third example, consider the tableau proof of \[ [ ( [ ∀ x . ( f x ) ] ∧ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} ) ⊃ ( ∃ x . \{ g x \} ) ] . \]

The one corresponds to the following informal argument: For \[ [ ( [ ∀ x . ( f x ) ] ∧ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} ) ⊃ ( ∃ x . \{ g x \} ) ] \] \({ [ ( [ ∀ x . ( f x ) ] ∧ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} ) ⊃ ( ∃ x . \{ g x \} ) ] }\) to be false in some interpretation \({ [ ( [ ∀ x . ( f x ) ] ∧ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} ) ] }\) would need to be true in that interpretation and \({ ( ∃ x . \{ g x \} ) }\) would need to be false. Then \({ [ ∀ x . ( f x ) ] }\) and \({ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} }\) would both be true. \({ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} }\) asserts the existence of at least one \({ x }\) such that \({ [ ( f x ) ⊃ ( g x ) ] }\). Let \({ a }\) be such a value of \({ x }\). Then \({ [ ( f a ) ⊃ ( g a ) ] }\). We have \({ [ ∀ x . ( f x ) ] }\), i.e. that \({ ( f x ) }\) for every value of \({ x }\). That includes \({ a }\) so \({ ( f a ) }\). \({ ( ∃ x . \{ g x \} ) }\) is false, so \({ ( g a ) }\) is also false. For \({ [ ( f a ) ⊃ ( g a ) ] }\) to be true we need \({ ( f a ) }\) to be false or \({ ( g a ) }\) to be true, but we’ve already seen that \({ ( f a ) }\) is true and \({ ( g a ) }\) is false. The assumption that \({ [ ( [ ∀ x . ( f x ) ] ∧ \{ ∃ x . [ ( f x ) ⊃ ( g x ) ] \} ) ⊃ ( ∃ x . \{ g x \} ) ] }\) is false in some interpretation leads to a contradiction, so it’s true in every interpretation, i.e. the statement is valid.

Although the “=” sign appears in the three tableau above we never actually used any of the equality rules for tableau. The example of \({ ( ∀ x . \{ ∀ y . [ ( x = y ) ⊃ ( y = x ) ] \} ) }\), i.e. the fact that equality is symmetric, shows them in use. Remarkably, it has no branching at all.

In the second to last line we used the second of our equality rules and the \({ ( a = b ) }\) on the left to replace the \({ b }\) in in the \({ ( b = a ) }\) on the right with an \({ a }\), giving an \({ ( a = a ) }\) to the right. The first equality rule allows us to write \({ ( a = a ) }\) on the left as well though, so we obtain our desired contradiction and close the branch.