if $M_1,M_2$ are two structures for FOL $L$ that differ in interpretations of signs not in statement $A$, then $M_1 \vdash A$ iff $M_2 \vdash A$

Question

Let $L$ be a first order language. Let $A$ be statement, and let $M_1,M_2$ be two structures for $L$.

I want to prove that if $M_1$ and $M_2$ differ in interpretation only of signs that aren't in $A$ then: $M_1 \vdash A$ iff $M_2 \vdash A$

Naturally I would think to prove it by induction on the structure of $A$. However, in first order logic, formulas are created recursively, and not statements. So I can't do that.

Then I thought about using induction on the structure of formulas and the induction claim will be: for every formula without free variables. (because a statement is a formula without free variables).

But here I also have a problem in that step: $A = \exists_x B$, because $x$ might be free in $B$ and thus, I won't be able to use the induction claim.

So my real problem is here is to determine what exactly will be the induction claim.

Help would be appreciated.

Answer 1

As you suspected you have to proceed by induction over the formulas (not necessarily closed).

The trick is to consider the semantics of first-order logic as an assignment of truth functions to open formulas: if $M$ is a $L$-structure and $\varphi(x_1,\dots,x_n)$ is a $L$-formula (with free variables $x_1,\dots,x_n$) then its truth-function is the $$ F_\varphi^M \colon M^n \longrightarrow \{0,1\} $$ where $F_\varphi^M(a_1,\dots,a_n)=1$ if and only if $M \models\varphi(a_1,\dots,a_n)$, or equivalently if $M,a_1,\dots,a_n \models \varphi(x_1,\dots,x_n)$, where $M,a_1,\dots,a_n$ is the $L \cup \{x_1,\dots,x_n\}$-structure that interprets the symbols of $L$ as in $M$ and the constants $x_1,\dots,x_n$ with $a_1,\dots,a_n$ respectively

What you need to show is that for every formula $\varphi$ you have that $F_\varphi^{M_1}$ and $F_\varphi^{M_2}$ are equal.

This is the statement to be proven by induction on the complexity of the formulas.

Of course in the special case where $\varphi$ is a closed formula, and so the relative functions $F_\varphi^{M_1}$ and $F_{\varphi}^{M_2}$ are $0$-ary functions (that is they are constants), the theorem states that the formula has the same truth value in the two models.

Hope this helps.

Answer 2

As you seem to recognize, the subset of closed formulas is not inductively defined (at least not in the "natural" way). (Open) Formulas are an inductively defined set. This situation happens often, and the resolution is called "strengthening the induction hypothesis". I feel that this is often subtly misleadingly presented. A typical presentation makes it look like we attempt an induction and that the problem was that our induction hypothesis was too weak and so we strengthen it. What usually (always?) actually happening is that we trying to do induction on something that isn't inductively defined in the first place, and "strengthening the induction hypothesis" is really formulating the correct induction hypothesis for an actual (more general) inductively defined set.

That said, you still need to figure out what the general theorem is for the inductively defined set containing the subset you care about which will specialize to the theorem you care about on that subset. In this case, that theorem is simply that the interpretation of (the potentially open) formula $A$ with respect to $M_1$ is the same as the interpretation of $A$ with respect to $M_2$ under the assumptions you gave (including the one on domains in the comments). The proof by induction is completely straightforward and largely just a reflection that interpretations are defined in a compositional manner.