X.3.5 Exercise. Let MM be a nonempty set and RβŠ†MΓ—MR\subseteq M\times M a binary relation over MM. Let Ma={b∣Rab}M_a = \{b\mid Rab\} and D={b∣¬Rbb}D = \{b\mid \neg Rbb\}. And let RΞΎaR\xi a be true if and only if ΞΎ\xi is the GΓΆdel number of a program PP such that P:aβ†’βˆžP: a\rightarrow\text{∞}.

A subset AA of MM is decidable if there is a program which for all a∈Ma\in M halts and outputs a truthy value if a∈Aa\in A.

  1. DD is distinct from all MaM_a.

    For any a∈Ma\in M, either RaaRaa or ¬Raa\neg Raa. If RaaRaa, then a∉Da\not\in D and a∈Maa\in M_a. If ¬Raa\neg Raa, then a∈Da\in D and a∉Maa \not\in M_a. So aa cannot be an element of both MaM_a and DD, so the two sets must differ by at least aa.

  2. All decidable subsets of MM occur among MaM_a.

    For any decidable subset AA of MM, let PP be a decision procedure for AA. Let Pβ€²P' be a program which for a∈Ma\in M halts if and only if PP decides a∉Aa\not\in A. Supposing ΞΎPβ€²\xi_{P'} is Pβ€²P''s GΓΆdel number, MΞΎP′≑AM_{\xi_{P'}}\equiv A.

  3. DD is undecidable.

    Per (1) and (2).

  4. The set Ξ haltβ€²={P∣P:ΞΎPβ†’halt}\Pi_{\text{halt}'}=\{P \mid P:\xi_P\rightarrow \text{halt}\} is undecidable.

    Suppose Ξ haltβ€²\Pi_{\text{halt}'} was decidable by a program PP. Then DD is decidable with PP (For an input a∈Ma\in M, if aa is the GΓΆdel number for a program PaP_a, use PP to determine if PaP_a is an element of Ξ haltβ€²\Pi_{\text{halt}'}. If Pa∈Πhaltβ€²P_a\in\Pi_{\text{halt}'}, then a∉Da\not\in D. If Pa∉Πhaltβ€²P_a\not\in\Pi_{\text{halt}'}, a∈Da\in D.). But this contradicts (3), so Ξ haltβ€²\Pi_{\text{halt}'} is undecidable.

  5. There is not a program which decides if an arbitrary program halts.

    If there were Ξ haltβ€²\Pi_{\text{halt}'} would be decidable, a contradiction to (4).

X.1.10 Exercise. Let A1\mathbb{A}_1 and A2\mathbb{A}_2 be finite alphabets such that A1βŠ†A2\mathbb{A}_1 \subseteq \mathbb{A}_2, and suppose WβŠ†A1βˆ—W \subseteq \mathbb{A}_1^*. Show WW is decidable (enumerable) with respect to A1\mathbb{A}_1 if and only if it is decidable (enumerable) with respect to A2\mathbb{A}_2.

Because A1\mathbb{A}_1 and A2\mathbb{A}_2 are alphabets, A1βˆ—\mathbb{A}_1^* and A2βˆ—\mathbb{A}_2^* are enumerable by 1.5 (p. 150). Let EA2βˆ—\mathfrak{E}_{\mathbb{A}_2^*} be a procedure which enumerates A2βˆ—\mathbb{A}_2^*. A2βˆ—βˆ–A1βˆ—\mathbb{A}_2^*\setminus\mathbb{A}_1^* is enumerable by a procedure which filters out elements of EA2βˆ—\mathfrak{E}_{\mathbb{A}_2^*}'s output containing only elements of A1\mathbb{A}_1. A1βˆ—\mathbb{A}_1^* is decidable with respect to A2βˆ—\mathbb{A}_2^* by Theorem 11.8 (p. 151) by the enumerability of A2βˆ—βˆ–A1βˆ—\mathbb{A}_2^*\setminus\mathbb{A}_1^* and A1βˆ—\mathbb{A}_1^*. Let DA2βˆ—β†’A1βˆ—\mathfrak{D}_{\mathbb{A}_2^*\rightarrow\mathbb{A}_1^*} be a decision procedure for A1βˆ—\mathbb{A}_1^* with respect to A2βˆ—\mathbb{A}_2^*. Suppose WW is decidable with respect to A1\mathbb{A}_1. Call DA1βˆ—β†’W\mathfrak{D}_{\mathbb{A}_1^*\rightarrow W} that decision procedure. Then WW is decidable with respect to A2\mathbb{A}_2 with a decision procedure which checks its input satisfies DA2βˆ—β†’A1βˆ—\mathfrak{D}_{\mathbb{A}_2^*\rightarrow\mathbb{A}_1^*} and DA1βˆ—β†’W\mathfrak{D}_{\mathbb{A}_1^*\rightarrow W}. Suppose WW is decidable with respect to A2\mathbb{A}_2. Call DA2βˆ—β†’W\mathfrak{D}_{\mathbb{A}_2^*\rightarrow W} that decision procedure. Because A1βŠ†A2\mathbb{A}_1\subseteq\mathbb{A}_2, DA2βˆ—β†’W\mathfrak{D}_{\mathbb{A}_2^*\rightarrow W} is also a decision procedure for WW with respect to A1\mathbb{A}_1. So WW is decidable with respect to A1\mathbb{A}_1.

5.10 Exercise. Show (a) The relation <\lt ("less-than") is elementarily definable in (R,+,β‹…,0)(\mathbb{R}, +, \cdot, 0), i.e., there is a formula Ο†βˆˆL2{+,β‹…,0}\varphi \in L_2^{\{+,\cdot,0\}} such that for all a,b∈Ra, b \in \mathbb{R},

(R,+,β‹…,0)βŠ¨Ο†[a,b]↔a<b.(\mathbb{R}, +, \cdot, 0) \models \varphi[a,b] \leftrightarrow a \lt b.

(b) The relation <\lt is not elementarily definable in (R,+,0)(\mathbb{R}, +, 0).

Proof. (a) is easily satisfied by Ο†=βˆƒk∈R,a+kβ‹…k≑b∧a≑̸b\varphi=\exists k\in\mathbb{R},a+k\cdot k\equiv b\land a\not\equiv b.

For (b) consider the automorphism Ο€(x)=βˆ’x\pi(x)=-x. I'll derive a contradiction. Say there were a Ο•\phi satisfying a<b↔(R,+,0)βŠ¨Ο†[a,b]a\lt b\leftrightarrow (\mathbb{R}, +, 0) \models \varphi[a,b].

a<b↔(R,+,0)βŠ¨Ο†[a,b]↔(RΟ€,+Ο€,0Ο€)βŠ¨Ο†[Ο€(a),Ο€(b)]byΒ IsomorphismΒ Lemma.↔(R,+,0)βŠ¨Ο†[βˆ’a,βˆ’b]as π isΒ anΒ automorphism.β†”βˆ’a<βˆ’b\begin{aligned} a\lt b&\leftrightarrow(\mathbb{R}, +, 0) \models \varphi[a,b] \\ &\leftrightarrow (\mathbb{R}^\pi, +^\pi, 0^\pi) \models \varphi[\pi(a),\pi(b)] \quad &\text{by Isomorphism Lemma.} \\ &\leftrightarrow (\mathbb{R}, +, 0) \models \varphi[-a,-b] \quad &\text{as } \pi \text{ is an automorphism.} \\ &\leftrightarrow -a\lt -b \end{aligned}

But a<bβ†”βˆ’a<βˆ’ba\lt b \leftrightarrow -a\lt -b is a contradiction, so <\lt is not elementarily definable in (R,+,0)(\mathbb{R}, +, 0).

4.15 Exercise. Let II be a nonempty set. For every i∈Ii \in I, let Ai\mathfrak{A}_i be an SS-structure. We write ∏i∈IAi\prod_{i\in I} \mathfrak{A}_i for the direct product of the structures Ai\mathfrak{A}_i, that is, the SS-structure A\mathfrak{A} with domain

A:=∏I∈iAi:={g∣g:I→⋃i∈IAiΒ andΒ βˆ€i∈I:g(i)∈Ai},A := \prod_{I\in i} A_i := \{ g \mid g : I \to \bigcup_{i \in I} A_i \text{ and } \forall i\in I: g(i) \in A_i \},

which is determined by the following conditions (where for g∈∏i∈IAig \in \prod_{i\in I} A_i we also write ⟨g(i)∣i∈I⟩\langle g(i) | i \in I \rangle):

For nn-ary R∈SR \in S and g1,…,gn∈∏i∈IAi,g_1, \dots, g_n \in \prod_{i \in I} A_i,

RAg1,⋯ ,gnβ†”βˆ€i∈I,RAig1(i),…,gn(i);R^{\mathfrak{A}}g_1, \dotsm, g_n \leftrightarrow \forall i\in I, R^{\mathfrak{A}_i} g_1(i), \dots, g_n(i);

For nn-ary f∈Sf \in S and g1,…,gn∈∏i∈IAi,g_1, \dots, g_n \in \prod_{i \in I} A_i,

fA(g1,⋯ ,gn):=⟨fAi(g1(i),…,gn(i))∣i∈I⟩;f^{\mathfrak{A}} (g_1, \dotsm, g_n) := \langle f^{\mathfrak{A}_i} (g_1(i), \dots, g_n(i)) \mid i \in I\rangle;

and cA:=⟨cAi∣i∈I⟩c^{\mathfrak{A}} := \langle c^{\mathfrak{A}_i} \mid i \in I\rangle for c∈S.c \in S.

Show: If tt is an S-term with var(t)βŠ†{v0,…,vnβˆ’1}\text{var}(t) \subseteq \{v_0, \dots, v_{n-1}\} and if g0,…,gnβˆ’1∈∏i∈IAi,g_0, \dots, g_{n-1} \in \prod_{i \in I} A_i, then the following holds:

tA[g0,…,gnβˆ’1]=⟨tAi[g0(i),…,gnβˆ’1(i)]∣i∈I⟩.t^{\mathfrak{A}}[g_0, \dots, g_{n-1}] = \langle t^{\mathfrak{A}_i}[g_0(i), \dots, g_{n-1}(i)] \mid i \in I \rangle.

Proof. I'll use induction on S-terms.

t=xt=x: Suppose j∈0,…,(nβˆ’1)j \in 0,\dots,(n-1) is the index in the variable assignment list corresponding to xx. As tt is a variable and variables take on the value assigned to them when interpreted, tAi[g0(i),…,gnβˆ’1(i)]=gj(i)t^{\mathfrak{A}_i}[g_0(i), \dots, g_{n-1}(i)]=g_j(i). Thus,

tA[g0,…,gnβˆ’1]=gj=⟨gj(i)∣i∈I⟩=⟨tAi[g0(i),…,gnβˆ’1(i)]∣i∈I⟩\begin{aligned} t^{\mathfrak{A}}[g_0, \dots, g_{n-1}] &=g_j \\ &=\langle g_j(i) \mid i\in I\rangle \\ &=\langle t^{\mathfrak{A}_i}[g_0(i), \dots, g_{n-1}(i)] \mid i\in I\rangle \end{aligned}

t=ct=c: As tt is a constant, var(t)=βˆ…\text{var}(t)=\varnothing. Thus by the Coincidence Lemma (p. 34), variable assignments don't change the value of tt under interpretation.

tA[g0,…,gnβˆ’1]=cA=⟨cAi∣i∈I⟩=⟨tAi[g0(i),…,gnβˆ’1(i)]∣i∈I⟩\begin{aligned} t^{\mathfrak{A}}[g_0, \dots, g_{n-1}] &= c^{\mathfrak{A}} \\ &=\langle c^{\mathfrak{A}_i} \mid i \in I\rangle \\ &=\langle t^{\mathfrak{A}_i}[g_0(i), \dots, g_{n-1}(i)] \mid i\in I\rangle \end{aligned}

t=ft1…tnt=ft_1\dots t_n: First, for a S-interpretation J\mathfrak{J}, J(ft1…tn)\mathfrak{J}(ft_1\dots t_n) is fJJ(t1)…J(tn)f^{\mathfrak{J}}\mathfrak{J}(t_1)\dots\mathfrak{J}(t_n); I make use of this in the first step below. Second, per the induction hypothesis, tA[g0,…,gnβˆ’1](i)t^{\mathfrak{A}}[g_0, \dots, g_{n-1}](i) is tAi[g0(i),…,gnβˆ’1(i)]t^{\mathfrak{A_i}}[g_0(i), \dots, g_{n-1}(i)]; I make use of this in the second step below.

tA[g0,…,gnβˆ’1]=fAt1A[g0,…,gnβˆ’1]…tnA[g0,…,gnβˆ’1]=⟨fAit1A[g0,…,gnβˆ’1](i)…tnA[g0,…,gnβˆ’1](i)∣i∈I⟩=⟨fAit1Ai[g0(i),…,gnβˆ’1(i)]…tnAi[g0(i),…,gnβˆ’1(i)]∣i∈I⟩=⟨tAi[g0(i),…,gnβˆ’1(i)]∣i∈I⟩\begin{aligned} &t^{\mathfrak{A}}[g_0, \dots, g_{n-1}] \\ &=f^{\mathfrak{A}}t_1^{\mathfrak{A}}[g_0, \dots, g_{n-1}]\dots t_n^{\mathfrak{A}}[g_0, \dots, g_{n-1}] \\ &=\langle f^{\mathfrak{A_i}}t_1^{\mathfrak{A}}[g_0, \dots, g_{n-1}](i)\dots t_n^{\mathfrak{A}}[g_0, \dots, g_{n-1}](i) \mid i\in I\rangle \\ &=\langle f^{\mathfrak{A_i}} t_1^{\mathfrak{A_i}}[g_0(i), \dots, g_{n-1}(i)]\dots t_n^{\mathfrak{A_i}}[g_0(i), \dots, g_{n-1}(i)] \mid i\in I\rangle \\ &=\langle t^{\mathfrak{A}_i}[g_0(i), \dots, g_{n-1}(i)] \mid i\in I\rangle \end{aligned}

This concludes the proof via induction on S-terms.

4.16 Exercise. Formulas which are derivable in the following calculus are called Horn formulas.

  1. For n∈Nn \in \mathbb{N} and atomic S-formulas Ο•1,…,Ο•n,Ο•\phi_1, \dots, \phi_n, \phi:
    (¬ϕ1βˆ¨β‹―βˆ¨Β¬Ο•nβˆ¨Ο•)\frac{}{(\neg\phi_1 \lor \dots \lor \neg\phi_n \lor \phi)}
  2. For n∈Nn \in \mathbb{N} and atomic S-formulas Ο•1,…,Ο•n\phi_1, \dots, \phi_n:
    ¬ϕ1βˆ¨β‹―βˆ¨Β¬Ο•n\frac{}{\neg\phi_1 \lor \dots \lor \neg\phi_n}
  3. For Horn formulas Ο•\phi and ψ\psi:
    Ο•,ψ(Ο•βˆ§Οˆ)\frac{\phi, \psi}{(\phi \land \psi)}
  4. For Horn formula Ο•\phi:
    Ο•βˆ€xΟ•\frac{\phi}{\forall x \phi}
  5. For Horn formula Ο•\phi:
    Ο•βˆƒxΟ•\frac{\phi}{\exists x \phi}

Horn formulas without free variables are called Horn sentences. Show: If Ο•\phi is a Horn sentence and βˆ€i∈I\forall i\in I Ai\mathfrak{A}_i is a model of Ο•\phi, then for A:=∏i∈IAi\mathfrak{A}:=\prod_{i \in I} \mathfrak{A}_i, AβŠ¨Ο•\mathfrak{A} \models \phi.

Proof. I'll use induction on Horn formulas. First, a lemma.

Lemma 1. For atomic S-formula ψ\psi, AβŠ¨Οˆβ†”βˆ€i∈I,Ai⊨ψ\mathfrak{A}\models\psi\leftrightarrow\forall i\in I,\mathfrak{A}_i\models\psi.

I show this is true for both forms of atomic S-formula.

ψ=t1≑t2\psi=t_1\equiv t_2: Recall from Exercise 4.15 A(t)=⟨Ai(t)∣i∈I⟩\mathfrak{A}(t) = \langle \mathfrak{A}_i(t) \mid i \in I \rangle.

A(ψ)↔A(t1)≑A(t2)β†”βŸ¨Ai(t1)∣i∈IβŸ©β‰‘βŸ¨Ai(t2)∣i∈IβŸ©β†”βˆ€i∈I,Ai(t1)≑Ai(t2)β†”βˆ€i∈I,Ai⊨ψ\begin{aligned} \mathfrak{A}(\psi) &\leftrightarrow \mathfrak{A}(t_1)\equiv\mathfrak{A}(t_2) \\ &\leftrightarrow \langle \mathfrak{A}_i(t_1) \mid i \in I \rangle \equiv \langle \mathfrak{A}_i(t_2) \mid i \in I \rangle \\ &\leftrightarrow \forall i\in I,\mathfrak{A}_i(t_1)\equiv\mathfrak{A}_i(t_2) \\ &\leftrightarrow \forall i\in I,\mathfrak{A}_i\models\psi \end{aligned}

ψ=Rt1…tn\psi=Rt_1\dots t_n: Another consequence of Exercise 4.15 is A(t)(i)\mathfrak{A}(t)(i) is ⟨Ai(t)∣i∈I⟩(i)\langle \mathfrak{A}_i(t) \mid i \in I \rangle(i) is Ai(t)\mathfrak{A}_i(t) which I use in the 3rd step below.

A(ψ)↔RAA(t1)…A(tn)β†”βˆ€i∈I,RAiA(t1)(i)…A(tn)(i)β†”βˆ€i∈I,RAiAi(t1)…Ai(tn)β†”βˆ€i∈I,Ai⊨ψ\begin{aligned} \mathfrak{A}(\psi) &\leftrightarrow R^\mathfrak{A}\mathfrak{A}(t_1)\dots\mathfrak{A}(t_n) \\ &\leftrightarrow \forall i\in I,R^{\mathfrak{A}_i}\mathfrak{A}(t_1)(i)\dots\mathfrak{A}(t_n)(i) \\ &\leftrightarrow \forall i\in I,R^{\mathfrak{A}_i}\mathfrak{A}_i(t_1)\dots\mathfrak{A}_i(t_n) \\ &\leftrightarrow \forall i\in I,\mathfrak{A}_i\models\psi \end{aligned}

Now, induction on Horn formulas.

ψ=(¬ϕ1βˆ¨β‹―βˆ¨Β¬Ο•nβˆ¨Ο•)\psi=(\neg\phi_1 \lor \dots \lor \neg\phi_n \lor \phi):

Note:

βˆ€i∈I,βˆƒm≀n,AiβŠ¨Β¬Ο•mβ†”βˆ€i∈I,βˆƒm≀n,Β¬AiβŠ¨Ο•mβ†’βˆƒi∈I,βˆƒm≀n,Β¬AiβŠ¨Ο•mβ†”βˆƒm≀n,βˆƒi∈I,Β¬AiβŠ¨Ο•mβ†”βˆƒm≀n,Β¬βˆ€i∈I,AiβŠ¨Ο•mβ†”βˆƒm≀n,Β¬AβŠ¨Ο•m(byΒ LemmaΒ 1.)β†”βˆƒm≀n,AβŠ¨Β¬Ο•m\begin{aligned} \forall i\in I,\exists m\leq n,\mathfrak{A}_i\models \neg\phi_m &\leftrightarrow \forall i\in I,\exists m\leq n,\neg\mathfrak{A}_i\models \phi_m \\ &\rightarrow \exists i\in I,\exists m\leq n,\neg\mathfrak{A}_i\models \phi_m \\ &\leftrightarrow \exists m\leq n,\exists i\in I,\neg\mathfrak{A}_i\models \phi_m \\ &\leftrightarrow \exists m\leq n,\neg \forall i\in I,\mathfrak{A}_i\models \phi_m \\ &\leftrightarrow \exists m\leq n,\neg \mathfrak{A}\models \phi_m \quad (\text{by Lemma 1.}) \\ &\leftrightarrow \exists m\leq n,\mathfrak{A}\models \neg\phi_m \\ \end{aligned}

Which together with Lemma 1 and the observation AβŠ¨Οˆβ†”βˆƒm≀n,AβŠ¨Β¬Ο•m∨AβŠ¨Β¬Ο•\mathfrak{A}\models \psi\leftrightarrow\exists m\leq n,\mathfrak{A}\models \neg\phi_m\lor\mathfrak{A}\models \neg\phi means:

βˆ€i∈I,AiβŠ¨Οˆβ†”βˆ€i∈I,βˆƒm≀n,AiβŠ¨Β¬Ο•m∨AiβŠ¨Β¬Ο•β†’βˆƒm≀n,AβŠ¨Β¬Ο•m∨AβŠ¨Ο•β†”A⊨ψ\begin{aligned} \forall i\in I,\mathfrak{A}_i\models \psi &\leftrightarrow \forall i\in I,\exists m\leq n,\mathfrak{A}_i\models \neg\phi_m\lor\mathfrak{A}_i\models \neg\phi \\ &\rightarrow \exists m\leq n,\mathfrak{A}\models \neg\phi_m \lor \mathfrak{A}\models \phi \\ &\leftrightarrow \mathfrak{A}\models \psi \end{aligned}

ψ=¬ϕ1βˆ¨β‹―βˆ¨Β¬Ο•n\psi=\neg\phi_1 \lor \dots \lor \neg\phi_n:

βˆ€i∈I,AiβŠ¨Οˆβ†”βˆ€i∈I,βˆƒm≀n,AiβŠ¨Β¬Ο•mβ†’βˆƒm≀n,βˆƒi∈I,AiβŠ¨Β¬Ο•mβ†”βˆƒm≀n,βˆƒi∈I,Β¬AiβŠ¨Ο•mβ†”βˆƒm≀n,Β¬βˆ€i∈I,AiβŠ¨Ο•mβ†”βˆƒm≀n,Β¬AβŠ¨Ο•m(byΒ LemmaΒ 1.)β†”βˆƒm≀n,AβŠ¨Β¬Ο•m↔A⊨ψ\begin{aligned} \forall i\in I,\mathfrak{A}_i\models \psi &\leftrightarrow \forall i\in I, \exists m\leq n,\mathfrak{A}_i\models \neg\phi_m \\ &\rightarrow \exists m\leq n,\exists i\in I,\mathfrak{A}_i\models \neg\phi_m \\ &\leftrightarrow \exists m\leq n,\exists i\in I,\neg\mathfrak{A}_i\models \phi_m \\ &\leftrightarrow \exists m\leq n,\neg\forall i\in I,\mathfrak{A}_i\models \phi_m \\ &\leftrightarrow \exists m\leq n,\neg\mathfrak{A}\models \phi_m \quad (\text{by Lemma 1.}) \\ &\leftrightarrow \exists m\leq n,\mathfrak{A}\models \neg\phi_m \\ &\leftrightarrow \mathfrak{A}\models \psi \end{aligned}

ψ=(Ο•βˆ§Ο†)\psi=(\phi \land \varphi):

βˆ€i∈I,AiβŠ¨Οˆβ†”βˆ€i∈I,AiβŠ¨Ο•βˆ§AiβŠ¨Ο†β†”AβŠ¨Ο•βˆ§AβŠ¨Ο†(byΒ induction)↔A⊨ψ\begin{aligned} \forall i\in I,\mathfrak{A}_i\models \psi &\leftrightarrow \forall i\in I,\mathfrak{A}_i\models \phi \land \mathfrak{A}_i\models \varphi \\ &\leftrightarrow \mathfrak{A}\models \phi \land \mathfrak{A}\models \varphi \quad (\text{by induction}) \\ &\leftrightarrow \mathfrak{A}\models \psi \end{aligned}

ψ=βˆ€xΟ•\psi=\forall x \phi:

Lemma 2. AaxβŠ¨Οˆβ†”βˆ€i∈I,Aa(i)x⊨ψ\mathfrak{A}\frac{a}{x}\models\psi\leftrightarrow\forall i\in I,\mathfrak{A}\frac{a(i)}{x}\models\psi

This follows from Exercise 4.15, which establishes (with different notation) Aax(t)β‰‘βŸ¨Aia(i)x(t)∣i∈I⟩\mathfrak{A}\frac{a}{x}(t)\equiv\langle\mathfrak{A}_i\frac{a(i)}{x}(t)\mid i\in I\rangle. This can be propogated through Lemma 1 and the other steps of this proof to see it holds for Ο•\phi.

βˆ€i∈I,AiβŠ¨βˆ€xΟ•β†”βˆ€i∈I,βˆ€a∈Ai,AiaxβŠ¨Ο•β†”βˆ€a∈A,βˆ€i∈I,Aia(i)xβŠ¨Ο•β†”βˆ€a∈A,AaxβŠ¨Ο•(byΒ LemmaΒ 2.)↔AβŠ¨βˆ€xΟ•\begin{aligned} \forall i\in I,\mathfrak{A}_i\models \forall x\phi &\leftrightarrow \forall i\in I,\forall a \in A_i,\mathfrak{A}_i\frac{a}{x}\models\phi \\ &\leftrightarrow \forall a \in A,\forall i\in I,\mathfrak{A}_i\frac{a(i)}{x}\models\phi \\ &\leftrightarrow \forall a \in A,\mathfrak{A}\frac{a}{x}\models\phi \quad (\text{by Lemma 2.}) \\ &\leftrightarrow \mathfrak{A}\models \forall x \phi \end{aligned}

ψ=βˆƒxΟ•\psi=\exists x \phi:

βˆ€i∈I,AiβŠ¨βˆƒxΟ•β†”βˆ€i∈I,βˆƒa∈Ai,AaxβŠ¨Ο•β†”βˆƒa∈A,βˆ€i∈I,Aa(i)xβŠ¨Ο•β†”βˆƒa∈A,AaxβŠ¨Ο•(byΒ LemmaΒ 2.)↔AβŠ¨βˆƒxΟ•\begin{aligned} \forall i\in I,\mathfrak{A}_i\models \exists x\phi &\leftrightarrow \forall i \in I,\exists a\in A_i,\mathfrak{A}\frac{a}{x}\models\phi \\ &\leftrightarrow \exists a\in A,\forall i\in I,\mathfrak{A}\frac{a(i)}{x}\models\phi \\ &\leftrightarrow \exists a\in A,\mathfrak{A}\frac{a}{x}\models\phi \quad (\text{by Lemma 2.}) \\ &\leftrightarrow \mathfrak{A}\models \exists x \phi \end{aligned}

This concludes the proof via induction on Horn formulas.

4.14 Exercise. A set Ξ¦\Phi of sentences is called independent if there is no Ο•βˆˆΞ¦\phi \in \Phi such that Ξ¦βˆ–{Ο•}βŠ¨Ο•\Phi \setminus \{\phi\} \models \phi. Show that the set of group axioms and the set of axioms for equivalence relations are independent. (p. 36)

I'll start with equivalence relations, their axioms being:

  1. βˆ€x,Rxx\forall x, Rxx
  2. βˆ€xy,Rxyβ†’Ryx\forall xy, Rxy \rightarrow Ryx
  3. βˆ€xyz,(Rxy∧Ryz)β†’Rxz\forall xyz, (Rxy \land Ryz) \rightarrow Rxz

This exercise asks for a proof none of the axioms of equivalence relations are redundant. Letting (1)(1), (2)(2), and (3)(3) correspond to the axioms above and setting Ξ¦={(1),(2),(3)}\Phi = \{(1), (2), (3)\}, we'd like to show:

βˆ„Ο•βˆˆΞ¦,Ξ¦βˆ–Ο•βŠ¨Ο•\nexists \phi \in \Phi, \Phi \setminus \phi \models \phi

Which unrolls to three cases.

  1. ¬{(2),(3)}⊨(1)\lnot \{(2), (3)\} \models (1)
  2. ¬{(1),(3)}⊨(2)\lnot \{(1), (3)\} \models (2)
  3. ¬{(1),(2)}⊨(3)\lnot \{(1), (2)\} \models (3)

B⊨β\Beta \models \beta, read "B\Beta models β\beta", is true if all interpretations which are true for the sentences in B\Beta are also true for β\beta. To show ¬B⊨β\lnot \Beta \models \beta, it is sufficent to find an interpretation which is true for the sentences in B\Beta and false for β\beta. As we're dealing with relations, we look for relations which satisfy only two of the three axioms.

A relation on a set XX is a subset RR of XΓ—XX\times X. RxyRxy is true ↔(x,y)∈R\leftrightarrow (x,y)\in R. Three relations then satisfying the expressions above are:

R1=βˆ…R2={(1,1),(2,2),(1,2)}R3={(1,1),(2,2),(3,3),(2,1),(1,2),(1,3),(3,1)}R_1=\varnothing \\ R_2=\{(1,1), (2,2), (1,2)\} \\ R_3=\{(1,1), (2,2), (3,3), (2,1), (1,2), (1,3), (3,1)\}

For R1R_1 suppose the domain is non-empty. In this case, the second and third axioms are vacuously true, but (1)(1) is not satisfied. R2R_2 satisfies the first and third axiom, but violates the second one as (1,2)∈R2(1,2)\in R_2 but (2,1)βˆ‰R2(2,1)\notin R_2. R3R_3 satisfies the first and second axiom, but voilates the third one as (2,1)∈R3∧(1,3)∈R3(2,1)\in R_3 \land (1,3) \in R_3 but (2,3)βˆ‰R3(2,3)\notin R_3. Thus, the axioms of equivalence relations are independent.

For ¬{(2),(3)}⊨(1)\lnot \{(2), (3)\} \models (1) there is a more general solution.

Lemma 1. For RR satisfying the second and third axiom of equivalence relations, if (x,y)∈R(x,y)\in R, then (y,y)∈R(y,y)\in R and (x,x)∈R(x,x)\in R.

Proof: Suppose (x,y)∈R(x,y)\in R and RR satisfies the second and third axiom of equivalence relations.

  1. By the second axiom, (x,y)∈Rβ†’(y,x)∈R(x,y)\in R \rightarrow (y,x)\in R.
  2. By the third axiom, (x,y)∈R∧(y,x)∈Rβ†’(x,x)∈R(x,y)\in R \land (y,x)\in R \rightarrow (x,x)\in R.
  3. By the third axiom, (y,x)∈R∧(x,y)∈Rβ†’(y,y)∈R(y,x)\in R \land (x,y)\in R \rightarrow (y,y)\in R.

RR is not reflexive if βˆƒx,(x,x)βˆ‰R\exists x,(x,x)\notin R. By Lemma 1, for RR satisfying the second and third axiom to not also satisfy the first axiom, there must exist xx not in the domain or range of RR. Thus, starting from a relation RR satisfying all three axioms, one can generate Rβ€²R' satisfying only the second and third by selecting BβŠ†AB\subseteq A and Rβ€²={p∣p∈R∧pβˆ‰BΓ—B}R'=\{p \mid p\in R \land p \notin B\times B\}. Setting B=AB=A yields βˆ…\varnothing i.e. R1R_1 above.

Independence of Group Axioms

A 2-ary function ff is a group over the domain AA if it satisfies identity, inverse, and associativity. These are satisfied if for some constant ee in AA:

  1. βˆ€x,fxe≑x\forall x, fxe \equiv x, i.e. identity.
  2. βˆ€x,βˆƒxβˆ’1,fxxβˆ’1≑e\forall x, \exists x^{-1}, fxx^{-1}\equiv e, i.e. inverse.
  3. βˆ€xyz,fxfyz≑ffxyz\forall xyz, fxfyz\equiv ffxyz, i.e. associativity.

As with equivalence relations, there are three cases.

  1. Β¬{(2),(3)}⊨(1)\lnot \{(2), (3)\} \models (1). For the group addition over the integers, ee would normally take on the value 00, but without (1)(1) ee can be 11 (i.e. xβˆ’1=βˆ’x+1x^{-1}=-x+1). With this new value of ee, (2)(2) and (3)(3) are satisfied, but (1)(1) is not.
  2. Β¬{(1),(3)}⊨(2)\lnot \{(1), (3)\} \models (2). For fab=aΓ—bfab=a\times b over the set Q2Γ—2\mathbb{Q}^{2 \times 2} of matricies with rational entries, ee is (1001)\begin{pmatrix}1 & 0 \\0 & 1\end{pmatrix}, matrix multiplication is associative, but not all matricies are invertable.

For the third case, Β¬{(1),(2)}⊨(3)\lnot \{(1), (2)\} \models (3), we'd like to find an operation and domain which satisfies identity and inverse but not associativity. Let the domain AA be {a,b,e}\{a,b,e\} and let f:AΓ—Aβ†’Af:A\times A \rightarrow A be defined as follows:

abeaebabaebeabe\begin{array}{c|ccc} & a & b & e \\ \hline a & e & b & a \\ b & a & e & b \\ e & a & b & e \\ \end{array}

fabfab corresponds to the value in row aa and column bb, i.e. bb. From the table, xβˆ’1x^{-1} is xx, left and right identity are satisfied, but associativity is not satisfied.

ffaba≠fafbafba≠faaa≠e\begin{aligned} ffaba &\neq fafba \\ fba &\neq faa \\ a &\neq e \end{aligned}

So the axioms of group theory are independent.


Thanks Pete for the book recomendation.