Canonical first-order structure (source code)

= Canonical first-order structure
{title2=$A=\{t^{\mathcal A}:t\text{ a closed term}\}$}

A <canonical first-order structure> is generated by closed-term names: each element is the interpretation of a <closed term>. In a <first-order language> without <function symbols> this says each element is named by a constant. The constant-name convention for <canonical first-order structures> agrees with this one in the function-free setting. <Logical equality> identifies different names for the same element.