Singleton truth-preservation obstruction to expressive completeness (source code)

= Singleton truth-preservation obstruction to expressive completeness

Suppose a <first-order language> has <logical implication> as its only connective and has either or both of the quantifiers, but no primitive falsity. In a singleton structure with every atomic predicate true, all atomic equalities are also true, and <structural induction> makes every formula true. No formula of this language can therefore express a negated equality. Quantifiers cannot repair this failure of expressive completeness, even though they add syntactic operations beyond propositional connectives.