Lecture 7 (2.12.96)

Material of this and subsequent lectures:

• [Ma3] J.A. Makowsky, Draft chapter of Interpretations, Translations and Reductions (for the Handbook of Logic in CS)

The Feferman-Vaught Theorems

The problem

• Cartesian product $A \times B$ of two structures A and B;
• Disjoint union $A \sqcup B$ of two structures A and B.
• Question: Given a formula $\phi$ in FOL, can we determine $A \times B \models \phi$ from the formulas true in A and the formulas true in B alone ?
• Question: Given a formula $\phi$ in FOL(q) of quantifier rank q, can we determine $A \times B \models \phi$ from the formulas FOL(q) true in A and the formulas true in B alone ?

Horn formulas

• Definition of Horn formulas: $\phi$ is a Horn formulas if it is in prenex normal form (PNF) with boolean part a disjunction of atomic or negated atomic formulas and at most one not negated.
• Theorem:(Exercise) If $\phi$ is a Horn formula and $A \models \phi$ and $B \models \phi$ then $A \times B =models \phi$. We say that $\phi$ is preserved under products.
• If we allow also infinite structures the converse also holds, i.e. if $\phi$ is preserved under products, then $\phi$ is equivalent to a Horn formula.
• In general, FOL formulas are not preserved under products.

Using games

• Let $Th_q(A)$ denote the set of FOL(q)-sentences true in A.
• Theorem:(Exercise) Given $\phi$ in FOL(q). Then $A \sqcup B \models \phi$ depends only on $Th_q(A)$ and $Th_q(B)$, but not on the structures A and B.
• Proof: Let A, A', B, B' such that $Th_q(A)=Th_q(A')$ and $Th_q(B)=Th_q(B')$. So player II has a winning strategy in the EF-game of lenghth q on A, A' or B, B' respectively. This strategy can be lifted to $A \sqcup B$ and $A' \sqcup B'$. Hence $Th_q(A \sqcup B)= Th_q(A' \sqcup B')$. therefore $\phi \in Th_q(A \sqcup B)$ iff $\phi \in Th_q(A' \sqcup B')$.

Using translation schemes

Next lecture: Lecture 8
Draft of chapter on translation schemes: Chapter of Handbook