Congruence relation on a first-order structure (source code)

= Congruence relation on a first-order structure
{title2=$a_i\sim b_i\Longrightarrow f(\vec a)\sim f(\vec b)$}

A <congruence relation on a first-order structure> is an <equivalence relation> compatible with each interpreted <function> and relation. Equivalent input <finite tuple>[tuples] give equivalent <function> outputs, and an <atomic formula>[atomic relation] has the same <truth value> on equivalent input <finite tuple>[tuples]. This compatibility makes the <functions> and relations well-defined on the <quotient set>. In a Henkin <term model> with <logical equality>[equality], membership of a formal <logical equality>[equality] in the maximal <consistent first-order theory>[consistent] theory gives precisely the <equivalence relation> used for this <quotient set>[quotient].