Logic Grid Puzzles are popular in magazines and newspapers. In such puzzles, the reader is asked to deduce an answer to a question from a set of clues in some scenario. For example, the scenario may be as follows: five guys are having drinks in a room. The clues are often information like "They all come from different countries", "The British is in blue" or "People in red don't drink alcohol". The question may be "What does the German drink?". The reader usually tries to deduce the answer by filling out a matrix with the clues, like the right one.Puzzles of this kind involve turning an implicit characterisation (i.e. the clues) into an explicit one (i.e. a direct answer to the question). In formal logic, we may define a relation explicitly with a formula. More precisely, given a theory $S$ (i.e. a set of sentences), an n-ary relation $R(x_1,...,x_n)$ is explicitly defined by $\Phi$ w.r.t. $S$ if$$S \models \forall x_1,...,x_n: R(x_1,...,x_n)\equiv\Phi(x_1,...,x_n),$$where $\Phi(x_1,...,x_n)$ is a formula that doesn't refer to $R$. (If $A,B$ are theories, $A\models B$ means that every model of $A$ is also a model of $B.$) In contrast, a theory referring to a relation may not uniquely determine that relation. Intuitively, a theory characterises a relation $R$ iff we cannot find two models of the theory that are only different in their interpretations of the symbol $R$. More formally, if $S$ is a theory of vocabulary $\tau$, then $S$ implicitly defines a non-logical symbol $R\in\tau$ iff for all structures $A$ of vocabulary $\tau\setminus\{R\}$, there exist at most one relation $R^A$ over the domain of $A$ such that $A$ becomes a model of $S$ by interpreting $R$ to $R^A$. There are several equivalent ways to express this concept (e.g. this and this), but we shall use the following one for our convenience of proof:
Definition. A theory $S$ implicitly defines an n-ary relation $R(x_1,...,x_n)$ if$$S\cup S' \models \forall x_1,...,x_n: R(x_1,...,x_n)\equiv R'(x_1,...,x_n),$$where $S'$ is obtained by replacing every occurrence of $R$ in $S$ with a fresh relation symbol $R'$.
If a $R$ is explicitly defined by $\Phi$ w.r.t. $S$, then it is clear that $R$ can also be implicitly defined by $S$. The converse result is proved by Beth for first-order logic.
Theorem. (Beth's Definability Theorem for FOL) If a first-order property is implicitly definable then it can also be defined explicitly.
Beth's result is a corollary of Craig's Interpolation Theorem.
Lemma. If $A$ is a theory and $A\models \varphi$, then there is a finite set $A'\subseteq A$ such that $A'\models \varphi.$
Proof of lemma. Note that $A\models \varphi$ if and only if $A\cup \{\neg \varphi\}$ is unsatisfiable. By the compactness theorem, there is a finite subset $E\subseteq A\cup \{\neg \varphi\}$ that is unsatisfiable. If $\neg \varphi\not\in E$ then let $A' = E$. Otherwise, let $A' = E\setminus\{\neg \varphi\}$. Then $A'$ is the desired set. ◻
Proof of Beth's theorem. Suppose we have$$S\cup S' \models \forall x_1,...,x_n: R(x_1,...,x_n)\equiv R'(x_1,...,x_n).$$By the above lemma, we can assume w.l.o.g. that $S,S'$ are finite. Let $X=\bigwedge S$ and $X'=\bigwedge S'$. Our assumption implies that $$X\wedge X' \rightarrow \forall x_1,...,x_n: R(x_1,...,x_n)\equiv R'(x_1,...,x_n)$$is valid. By introducing fresh variables $p_1,...,p_n$, we can rewrite the above sentence to $X\wedge X' \rightarrow (R(p_1,...,p_n)\equiv R'(p_1,...,p_n))$, which is further equivalent to$$(X\wedge R(p_1,...,p_n)) \rightarrow (X' \rightarrow R'(p_1,...,p_n)).$$Since $X$ doesn't contain $R'$, and $X'$ doesn't contain $R$, by Craig's theorem there exist a formula $\Phi(p_1,...,p_n)$ containing neither $R$ nor $R'$, such that both$$(X\wedge R(p_1,...,p_n)) \rightarrow \Phi(p_1,...,p_n) \quad\mbox{and}\quad \Phi(p_1,...,p_n) \rightarrow (X' \rightarrow R'(p_1,...,p_n))$$ hold. Note that the latter can be rewritten to $\Phi(p_1,...,p_n) \rightarrow (X \rightarrow R(p_1,...,p_n))$ by replacing every occurrences of $R'$ with $R.$ It follows from the currying law that$$X \rightarrow (R(p_1,...,p_n) \rightarrow \Phi(p_1,...,p_n))\quad\mbox{and}\quad X \rightarrow (\Phi(p_1,...,p_n) \rightarrow R(p_1,...,p_n))$$are valid. Conjuncting the two formulas leads to $$X \rightarrow (R(p_1,...,p_n) \equiv \Phi(p_1,...,p_n)),$$ which further implies that $$S \models \forall x_1,...,x_n: R(x_1,...,x_n) \equiv \Phi(x_1,...,x_n).$$ This concludes the proof of the theorem. ◻
Craig's interpolation can be computed via syntactical transformation, as is shown in Craig's 1957 paper. Hence, we can always construct an explicit definition out of an implicit one. Since explicit definition is a syntactical notion (i.e. defined with a formula) while implicit definition tends to be more semantical (i.e. defined with a theory), Beth's theorem indicates that the syntactical definability of first-order logic is "complete" in some sense.
No comments:
Post a Comment