This is exercise 3.4.16 from Mathematical Logic by Ebbinghaus.
Formulas which are derivable in the following calculus are called Horn formulas:
Horn formulas without free variables are called Horn sentences. Show that if $\phi$ is a Horn sentence and $\mathfrak A_i$ is a model of $\phi$ for $i \in I$, then $\Pi_{i \in I} \mathfrak A_i \models \phi$ (The product's definition can be found here). Hint: State and prove the corresponding result for Horn formulas.
I have been trying to get started on this exercise for an entire hour with not much luck. First of all, are the formulas $\phi,\psi$ in (3) also Horn formulas? It's also not clear what the corresponding general result should be, but here is my attempt:
Since the given result that must be proven involves no free variables, we must also include no free variables in the general result.
To do this, there must be a set of elements in the domain $\Pi_{i \in I} A_i \models \phi$ such that each of the free variables has an interpretation.
Thus we can define an analogous product $\Pi_{i \in I} \mathfrak J_i \models \phi$ that instead of involving structures, it involves the interpretations $\mathfrak J_i$. They are very similar if not the same with the only difference being that this new product interprets free variables.
Thus our analogous result would be: If $\phi$ is a Horn formula and $\mathfrak J_i$ is an interpretation that models $\phi$ for each $i \in I , $ then $\Pi_{i \in I} \mathfrak J_i \models \phi$
But even if I prove this result I don't know how to show that it implies the given result. Can anyone help me out by clearing the fog? Thanks in advance!
I'll say that a formula $\varphi(\cdots)$ has the product property precisely when:
$$ \prod_{i \in I}A_i \models \varphi(\cdots) \iff \text{for all $i$ in $I$, the formula $\varphi(\cdots)$ holds of $A_i$ } $$
I'll say that a formula has the weak product property precisely when:
$$ \text{$\varphi(\cdots)$ holds of all $A_i$} \implies \prod_{i \in I} A_i\models \varphi(\cdots) $$
The contrapositive of the weak product property is:
$$ \text{for some $\vec{x}$, $\prod_{i \in I} A_i, \vec{x} \not\models \varphi(\vec{x})$} \implies \text{for some $i$, $A_i, (x_i) \not\models \varphi((x_i))$} $$
I'll define an atomic formula as a formula with no proper subformulas and allow it to be headed by $\top$, $=$, or a predicate symbol $R$. Taking $\top$ as an atomic formula is not standard but simplifies the proof.)
An atomic equation is an atomic formula headed by $=$.
An atomic non-equation is an atomic formula headed by $\top$ or a user-defined relation $R$.
Let $B$ be $\prod_{i \in I} A_i $.
If $\vec{x}$ is a variable sequence let $(x_i)$ denote the $i$-th component of each element of $\vec{x}$.
Theorem 100: If $\varphi(\cdots)$ has the product property then it has the weak product property.
As proof, note that the weak product property is just one of the directions of a biconditional.
Theorem 101: Atomic equations have the product property.
Suppose $B \not\models t_1(\cdots) = t_2(\cdots)$.
There exists a variable sequence $\vec{x}$ so that $B, \vec{x} \not\models t_1(\vec{x}) = t_2(\vec{x})$.
If this is true, then there must exist some $i$ such that
$$ B, \vec{x} \models t_1(\vec{x})_i \;\;\text{is not the same as}\;\; t_2(\vec{x})_i $$
And hence for some $i$
$$ A_i, (x_i) \not\models t_1((x_i)) = t_2((x_i)) $$
As desired.
Suppose $B \models t_1(\cdots) = t_2(\cdots)$.
Thus for any $\vec{x}$.
$$ B, \vec{x} \models t_1(\vec{x}) = t_2(\vec{x}) $$
Then, for any index $i$, we can take the $i$th component of every element of $B$ as well as the $i$th element of the two terms:
Theorem 102: Atomic non-equations have the product property.
If $\varphi(\cdots)$ is $\top$, then we are done.
Suppose $\varphi$ is headed by $R$, a user-defined predicate of some arity.
Suppose $B \not\models R(\cdots)$.
Thus for some $\vec{x}$, it holds that $B, \vec{x} \not\models R(\vec{x})$.
This means that $\vec{x}$ is not $R^B$, the interpretation of $R$.
However, $B$ is a product, so $R^B$ is defined to be $\cdots \times R^{A_i} \times \cdots$ which is $\prod_{i \in I}(R^{A_i})$
Therefore we can pick an $i$ so that $x_i$ is not in $R^{A_i}$, as desired.
Suppose $B \models R(\cdots)$.
Let $\vec{x}$ be an arbitrary variable sequence.
It holds that $B, \vec{x} \models R(\vec{x})$.
Hence for any $i$ in $I$, it holds that $B_i, (x_i) \models R((x_i))$, i.e. $A_i, (x_i) \models R((x_i))$.
However, $\vec{x}$ was arbitrary, and we can hit any possible variable sequence in $A_i$ using $(x_i)$, so we're done.
Theorem 103: If $\alpha(\cdots)$ is an atomic formula and $\varphi(\cdots)$ has the weak product property, then $(\alpha \to \varphi)(\cdots)$ has the weak product property.
If $\alpha$ is headed by $\top$, then we're done by theorems 101 and 102.
Suppose $\alpha$ is headed by $=$.
Suppose that $B, \vec{x} \not\models t_1(\vec{x}) = t_2(\vec{x}) \to \varphi(\vec{x}) $.
Thus $B, \vec{x} \models t_1(\vec{x}) = t_2(\vec{x})$
But $B, \vec{x} \not\models \varphi(\vec{x})$.
By hypothesis, there exists an $i$ so that $A_i, (x_i) \not\models \varphi(\vec{x})$
By theorem 101, $t_1(\cdots) = t_2(\cdots)$ holds of $A_i, (x_i)$.
Thus $A_i, (x_i) \not\models t_1((x_i)) = t_2((x_i)) \to \varphi((x_i))$ as desired.
Suppose $\alpha$ is headed by a user-defined predicate $R$.
Suppose $B, \vec{x} \not\models R(\vec{x}) \to \varphi(\vec{x})$
Thus $B, \vec{x} \models R(\vec{x})$.
But $B, \vec{x} \not\models \varphi(\vec{x})$.
By hypothesis, there exists an $i$ so that:
$$ A_i, (x_i) \not\models \varphi((x_i)) $$
By theorem 102, $R((x_i))$ holds of $A_i, (x_i)$.
Thus, as desired, $A_i, (x_i) \not\models R((x_i)) \to \varphi((x_i))$.
Theorem 104: If $\alpha(\cdots)$ and $\beta(\cdots)$ both have the weak product property, then so does $(\alpha \land \beta)(\cdots)$.
Suppose $B, \vec{x} \not\models \alpha(\vec{x}) \land \beta(\vec{x})$.
So that means one of $\alpha(\cdots)$ or $\beta(\cdots)$ has to fail here. Suppose without loss of generality that it is $\alpha(\cdots)$, i.e.
$$ B, \vec{x} \not\models \alpha(\vec{x}) $$
By hypothesis, there exists an $i$ so that
$$ A_i, (x_i) \not\models \alpha((x_i)) $$
$\alpha((x_i))$ is already false here, so we can add another conjunct.
$$ A_i, (x_i) \not\models \alpha((x_i)) \land \beta((x_i)) $$
This is what we wanted to show.
Thus $(\alpha \land \beta)(\cdots)$ has the weak product property.
Theorem 105: If $\varphi(\cdots)$ has the weak product property, so does $[\forall z](\varphi(z, \cdots))$.
Suppose $B, \vec{x} \not\models [\forall z](\varphi(z, \vec{x}))$.
There therefore exists an extended variable sequence $\vec{v}$ extending $\vec{x}$, assigning an interpretation to $z$ so that
$$ B, \vec{v} \not\models \varphi(\vec{v}) $$
Thus, by hypothesis, it follows for some $i$ that
$$ A_i, (v_i) \not\models \varphi((v_i)) $$
Let's split $(v_i)$ into $(x_i)$ and an interpretation of $z$ which we will just call $z$.
$$ A_i, z, (v_i) \not\models \varphi(z, (v_i)) $$
Next we replace $z$ with a universal quantifier. We are allowed to do this because we found a counterexample to $\varphi(\bigcirc, (v_i))$ in the structure $A_i$.
$$ A_i, (v_i) \not\models [\forall z](\varphi((v_i))) $$
This is what we wanted to show.
Theorem 106: If $\varphi(\cdots)$ has the weak product property so does $[\exists w](\varphi(w, \cdots))$.
Suppose for all $i$ that
$$ A_i \models [\exists w](\varphi(w, \cdots)) $$
Let $A'_i$ be $A_i$ extended with a fresh function symbol $c$ so that the following holds:
$$ A'_i \models \varphi(c, \cdots) $$
We make this choice in an arbitrary manner across the $A_i$ structures.
We then construct the product $B' = \prod_{i \in I} A'_i$.
By hypothesis,
$$ B' \models \varphi(c, \cdots) $$
Thus
$$ B' \models [\exists w](\varphi(w, \cdots) $$
Note, however, that $c$ is a fresh constant symbol and $B$ is the reduct of $B'$ without $c$. Thus
$$ B \models [\exists w](\varphi(w, \cdots)) $$
This is what we wanted to show.
Theorem 200: Direct product of structures satisfies a Horn sentence.
Properties (1) and (2) hold by theorems 100, 101, 102, and 103.
Property (3) holds by theorem 104.
Property (4) holds by theorem 105.
Property (5) holds by theorem 106.
Thus, as desired, all horn formulas and hence all horn sentences have the weak product property.