Semantic Tableaux (Predicate Logic)

Builds off Semantic Tableaux in Propositional Logic.

List of Additional Rules

where is a term that is a legal substitution.

where is a fresh variable that has not appeared in the tableau so far

(see Statements and Quantifiers#Negation of Quantifiers)

Tip

Apply the existential and negative universal rules before the universal and negative existential rule

Property

Semantic Tableaux proofs for predicate logic are both sound and complete

Example

Prove:

proof

Example

Prove:

proof

Example

Prove:

proof

Example

Prove:

proof

Example

Prove:

proof