Finally, for languages with finite Herbrand bases, we have the Domain Closure (DC) rule. For a language with object constants σ_{1}, ... , σ_{n}, the rule is written as shown below. If we believe a schema is true for every instance, then we can infer a universally quantified version of that schema.
Domain Closure 
φ[σ_{1}] 
... 
φ[σ_{n}] 

∀ν.φ[ν] 
For example, in a language with four object constants a and b and c and d, we can derive the conclusion ∀x.φ[x] whenever we have φ[a] and φ[b] and φ[c] and φ[d].
