\section{Trump semantics}

Wilfrid Hodges made an important breakthrough when he found a way to define a Tarski-style semantics for independence-friendly logic \cite{Hodges:1997a, Hodges:1997b}. We now recall the necessary details.

\begin{defn} 
Two valuations \(\vec a, \vec b \in\, \^NA\) \emph{agree outside of \(J \subseteq N\)}, denoted \(\vec a \approx_J \vec b\)\index{\(\vec a \approx_J \vec b\)\quad $\vec a$ and $\vec b$ agree outside of $J$|mainidx}, if 
\[
\vec a \restrict (N\setminus J) = \vec b \restrict(N\setminus J).
\]
\end{defn}


\begin{defn} 
Given any set $V$, a \emph{cover} of $V$ is a collection of sets $\mathscr U$ such that \(V = \bigcup\mathscr U\). A \emph{disjoint cover} is a cover whose members are pairwise disjoint.
\end{defn}


\begin{defn} 
Let \(V \subseteq \^NA\), and let $\mathscr U$ be a cover of $V$. Then $\mathscr U$ is called \emph{$J$-saturated}\index{cover!$J$-saturated|mainidx} if every \(U \in \mathscr U\) is closed under $\approx_J$. That is, for every \(\vec a, \vec b \in V\), if \(\vec a \approx_J \vec b\) and \(\vec a \in U \in \mathscr U\), then \(\vec b \in U\).
\end{defn}


\begin{defn} 
Define a partial operation $\bigcup_J$\index{$\bigcup_J \mathscr U$|mainidx} on sets of teams by declaring \(\bigcup_J \mathscr U = \bigcup \mathscr U\) whenever $\mathscr U$ is a $J$-saturated disjoint cover of $\bigcup \mathscr U$ and letting $\bigcup_J \mathscr U$ be undefined otherwise. Thus the formula \(V = \bigcup_J \mathscr U\) asserts that $\mathscr U$ is a $J$-saturated disjoint cover of $V$. We will use the notation \(V_1 \cup_J V_2\)\index{$V_1 \cup_J V_2$|mainidx} to abbreviate \(\bigcup_J \set{V_1, V_2}\).
\end{defn}


\begin{defn} 
A function \(f\colon V \to A\) is \emph{independent of $J$}, denoted \(f\colon V \toind{J} A\)\index{$f\colon V \toind{J} A$ \quad $f$ is independent of $J$|mainidx},  if \(f(\vec{a}) = f(\vec{b})\) whenever \(\vec{a} \approx_J \vec{b}\). 
\end{defn}

\begin{defn} 
Let \(\vec a \in \^NA\). For every \(n < N\) and \(b \in A\), define $\vec a(n:b)$ to be the valuation that is like $\vec a$ except the $n$th value has been changed to $b$, i.e.,
\[
\vec a(n:b) = \vec a \restrict(N\setminus\set{n}) \cup \set{\tuple{n,b}}.
\]
Let \(V,W \subseteq \^NA\) and \(f\colon V \to A\). Define
\begin{align*}
V(n:f) &= \setof{\vec a(n:f(a))}{\vec a \in V}, \\
W(n:A) &= \setof{\vec a(n:b)}{\vec a \in W,\, b \in A}.
\end{align*}

\end{defn}


The next theorem has appeared in many different forms in the literature.
Hodges' original formulation (for IF logic) appears in \cite[Theorem 7.5]{Hodges:1997a}. Dechesne's version for IFG logic appears in \cite[Theorem 5.3.5]{Dechesne:2005}.


\begin{thm}[Hodges] 
\label{trump semantics}
\index{$\A \modeltf \phi[V]$|mainidx}
Let $\phi$ be an IFG$_N$-formula, let $\A$ be a suitable structure, and let \(V,W \subseteq \^NA\).
\begin{itemize}
	\item If $\phi$ is atomic, then  
	\begin{itemize}
		\item[(+)] \(\A \modelt \phi[V]\) if and only if for every \(\vec a \in V\), \(\A \models \phi[\vec a]\),
		\item[($-$)] \(\A \modelf \phi[W]\) if and only if for every \(\vec b \in W\), \(\A \not\models \phi[\vec b]\).	
	\end{itemize}
	\item If $\phi$ is ${\hneg\psi}$, then 
	\begin{itemize}
		\item[(+)] \(\A \modelt {\hneg\psi[V]}\) if and only if \(\A \modelf \psi[V]\),
		\item[($-$)] \(\A \modelf {\hneg\psi[W]}\) if and only if \(\A \modelt \psi[W]\).
	\end{itemize}
	\item If $\phi$ is $\psi_1 \hor{J} \psi_2$, then 
	\begin{itemize}
		\item[(+)] \(\A \modelt \psi_1 \hor{J} \psi_2[V]\) if and only if \(\A \modelt \psi_1[V_1]\) and \( \A \modelt \psi_2[V_2]\) for some \(V = V_1 \cup_J V_2\),
		\item[($-$)] \(\A \modelf \psi_1 \hor{J} \psi_2[W]\) if and only if \(\A \modelf \psi_1[W]\) and \( \A \modelf \psi_2[W]\).
	\end{itemize}
	\item If $\phi$ is $\hexists{v_n}{J}\psi$, then 
	\begin{itemize}
		\item[(+)] \(\A \modelt \hexists{v_n}{J}\psi[V]\) if and only if \(\A \modelt \psi[V(n:f)]\) for some \(f\colon V \toind{J} A\),
		\item[($-$)] \(\A \modelf \hexists{v_n}{J}\psi[W]\) if and only if \(\A \modelf \psi[W(n:A)]\).
	\end{itemize}
\end{itemize}
\end{thm}

\begin{proof}
By two simultaneous inductions on the subformulas of $\phi$. A full proof using the present notation can be found in \cite[Theorem 1.32]{Mann:2007}.
\end{proof}
{"config": "arxiv", "file": "0806.4785/3-Trump_semantics.tex"}