Distinct witnesses from incompatible unary predicates

ID: distinct-witnesses-from-incompatible-unary-predicates

The displayed first-order sentence requires a domain with at least elements without using logical equality. Distinct patterns disagree on some predicate, so a single element cannot witness both. Conversely, a domain consisting of the binary strings of length , with selecting strings whose th bit is one, realizes every pattern. More generally, requiring any distinct unary predicate types forces at least distinct elements.

New to topics? Read the docs here!