How a theorem in a mathematical theory can be applied to a model of the mathematical theory?

Question

Jean Dieudonne, one of the most prominent mathematicians of the 20th century, stated[1. p.215] that any mathematical theory is an extension of ZF set theory:

"The theory of sets, so conceived, embraces all mathematical theories, each of which is defined by the assignment of a certain number of letters (the “constants” of the theory) and relations which involve these letters (the “axioms” of the theory): for example, the theory of groups contains two constants, $G$ and $m$ (representing respectively the set on which the group is defined, and the law of composition), and the relations express first that $m$ is a mapping from $G \times G$ to $G$, and second the classical properties of the law of composition.

Then a model $M$ of group theory can be defined as a pair $(S,f)$ where $S,f$ are terms in another mathematical theory $W$, satisfying the axioms of group theory.

Let $B$ be a theorem in the group theory.

How the theorem $B$ can be applied to the model $M$?

Just replace in $B$ the constants $G,m$ with $S,f$ respectively and every defined in group theory name $d$ with $d_M$?

Is there an appropriate metatheorem?

References

[1] Jean Dieudonne. A panorama of pure mathematics as seen by N.Bourbaki. Academic Press, New York, 1982. Also available online at: https://drive.google.com/file/d/1XnxQhXQqmgNOwPFWEShprVhrPruY0HZN/view?usp=drive_link

Answer 1

It seems you come from FoM. Psychologically, it's better to think of a model or structure as a concrete/materialistic/Platonic collection of objects, or it's better to think in terms of naive set theory, rather than axiomatic set theory. But of course, no matter how we think, we still need a language to express the ideas/facts (whatever you want to call them) and in subtle cases to formally clarify certain properties of sets (since naive set theory can be inconsistent), and the language/axiomatic system can be ZF(C).

Given a theorem $T$ from group theory, it should be applied to any group (that is, the theorem states a fact about a group), but the way we state the fact can be formally translated into a theorem in ZF(C). Put in another way, $T$ itself is a syntactic result, and when applied to a model, it becomes a semantic one but still it can be regarded as a syntactic one in ZF(C).

As for a meta-theorem, various statements of soundness makes this more precise such as Theorem 18. Roughly, a theorem is always a true statement when interpreted in a model.

Answer 2

If we accept that every defined name is expressible using only primitive names (it follows from the rule of definition as stated, for example in [2, p.6]) then the following metatheorem(an easy corollary of the Deduction Theorem) in the first-order logic can be used:

Let $T$ be a (first-order) theory, $A,B$ are formulas in $T$,

$FV(A) = {x_1, ..., x_k}, FV(B) \subseteq FV(A)$,

$T + \{c_1, ..., c_k; A(c_1, ..., c_k)\}$ denotes the theory obtained from $T$ by adding to $T$ the new constant symbols $c_1, ..., c_k$ and the formula $A(c_1, ..., c_k)$ as a new axiom, where $A(c_1, ..., c_k)$ denotes the result of replacement in $A$ every $x_i$ with $c_i$,

(a) $T + \{c_1, ..., c_k; A(c_1, ..., c_k)\} \vdash B(c_1, ..., c_k)$,

(b) $T' \vdash A(z_1, ..., z_k)$ where $T'$ denotes an extension of $T$, $z_1, ..., z_k$ are terms in $T'$, then

$T' \vdash B(z_1, ..., z_k)$.

Proof

The Deduction theorem[2,pp. 33-34](Shoenfield on p.33 stated a special case of the theorem; the general case is proved on p.34) in the above notations can be written as:

(DT) $T + \{c_1, ..., c_k; A(c_1, ..., c_k)\} \vdash B(c_1, ..., c_k)$ iff $T \vdash A \rightarrow B$.

Now from (DT) and (a) it follows that:

(c) $T \vdash A \rightarrow B$.

Because $T'$ is an extension of $T$, we have:

(d) $T' \vdash A \rightarrow B$.

Now from (d), (b) we receive:

$T' \vdash B(z_1, ..., z_k)$.

end of Proof.

Now, following Dieudonne, the mathematical theory of groups is the first-order theory $ZF + \{G,m; A(G,m)\}$, where $A(G,m)$ is a conjunction of the group axioms.

Suppose, $ZF + \{G,m; A(G,m)\} \vdash B(G,m)$, where $B(G,m)$ is a theorem in the theory of groups.

Let $(S,f)$ be a model of the theory of groups in a theory $ZF'$, where $ZF'$ is an extension of $ZF$. The formula $A(S,f)$ is a theorem in $ZF'$, where $S,f$ are some terms in $ZF'$. Now, by the just proved metatheorem, the formula $B(S,f)$ is a theorem in $ZF'$.

References

[1] Jean Dieudonne. A panorama of pure mathematics as seen by N.Bourbaki. Academic Press, New York, 1982. Also available online at: https://drive.google.com/file/d/1XnxQhXQqmgNOwPFWEShprVhrPruY0HZN/view?usp=drive_link

[2] Joseph R.Shoenfield. Mathematical logic. Addison-Wesley, 1967 (and the latest printings). Also available online at: https://drive.google.com/file/d/15XVaWPEZORX9c5Ba3LX0eDrC2J5yvXL3/view?usp=drive_link