MATH.18:4.2 - Construct the interpretation

Specify the source objects’ target counterparts and the operations or relations that interpret each required primitive. Give a construction rather than a matching name. If an operation is to be recovered through a defining condition, establish that a result exists and is determined to the degree required by the source.

Respect the domains and arities. A binary operation needs two admitted inputs; a relation needs the participants on which it is asserted. When the source uses equivalence classes, establish that different representatives give equivalent interpreted results. MATH.2 supplies the detailed quotient test.

Extend the interpretation through constructed expressions. Interpret each input, then interpret the operation applied to those inputs. A composite expression is handled by repeating this rule through its construction. MATH.5 develops the extension from generators when the source is presented that way.

An assertion also has a construction. Translate equality, conditions and quantifier ranges. For there exists x in A with P(x), the target must express both the interpreted domain A and the interpreted condition P. Enlarging that range can admit a solution that the original problem excludes; :5.2 works this failure.

When an interpretation uses a basis, representative or another choice, supply it or a means of obtaining it. Determine whether changing the choice changes the result, or only changes a representation with a known comparison.