0.1 Exclusivity

We are now in the position to prove the main result of this Chapter, namely that clause complementation satisfies the boolean rules of negation, in the form of exclusivity and exhaustivity. We remark that this holds due to the fact that context schemata allow to pose only ‘well-behaved’ goals. For example, consider the query G ≡ ¬even(0) → even(s(s(0))), which is such that both ; ·; · ⊢_{even} G and ; ·; · ⊢_{¬even} Not_{G}(G) are provable. By definition of schema satisfaction, this is not a legal query. Similarly, the following counterexample to exhaustivity ; ·; · ⊢_{even} ∀x : nat. even(x) is not allowed. Moreover, the Context Preservation Theorems (Theorem ?? and ??) guarantees that, from allowed run-time contexts and goals, only allowed subgoals are generated. We will need the following obvious fact:

Lemma 0.1 If Γ ⊢ M : A and M is rigid, so is every N such that N ∈ (Γ ⊢ Not(M)).

Proof: By a straightforward induction on the structure of Γ ⊢ Not(M). □

We use Γ; D ⊢_{P} Not_{G}(G) for Γ ⊢ Not_{G}(G) = G′ and Γ; D ⊢_{P} G′; also, Γ; D ⊢_{P} Not_{D}(D)>>¬Q for Not_{D}(D) = D′ and Γ; D ⊢_{P} D′>>¬Q; similarly for Notα. We use P to denote the conjunction of a positive program P^{+} and its negation P^{−} = Not_{D}(P^{+}).

Theorem 0.2 (Exclusivity) Let ⊧_{S^{a}} aug_{D}(P) and Γ; D < S^{a}. For every goals such that Γ; D \ G < S^{a}, it is not the case that both Γ; D ⊢_{P} G and Γ; D ⊢_{P} Not_{G}(G).

Proof: We generalize this to;

1 It is not the case that there is S^{+} :: Γ; D ⊢_{P} G and there is S^{−} :: Γ; D ⊢_{P} Not_{G}(G).

2.1 Let D ⊑ def(q, P): It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} Not_{D}(D)>>Not_{G}(Q). By mutual induction on the structure of I^{+} and S^{+}, by assuming their existence:

Case:

I^{+} = \frac{>>⊥}{Γ; D ⊢_{P} ⊥_{q}>>Q}

But there can be no proof of ¬Q from Not_{D}(⊥_{q}) = ⊤_{q}.

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} [σ]G \\ & >> → \\ Γ; D ⊢_{P} ∀(q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(∀(q \overline{N_{n}} ← G))>>¬q \overline{M_{n}}:
Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}}  By sub-derivation
· ⊢ \overline{M_{n}} ∈ ∥\overline{N_{n}}∥ (∗)  By definition of of ∥ ∥
S_{1}^{+} :: Γ; D ⊢_{P} [σ]G  By sub-derivation
Γ; D ⊢_{P} ⋀_{\overline{S_{n}}∈·⊢Not(\overline{N_{n}})} ∀(¬q \overline{S_{n}} ← ⊤) ∧ ∀(¬q \overline{N_{n}} ← Not_{G}(G))>>¬q \overline{M_{n}}  By rule Not_{D} →
Subcase: Γ; D ⊢_{P} ⋀_{\overline{S_{n}}∈·⊢Not(\overline{N_{n}})} ∀(¬q \overline{S_{n}} ← ⊤)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ∀(¬q \overline{S_{n}} ← ⊤)>>¬q \overline{M_{n}} for some \overline{S_{n}}  By inversion
Γ; D ⊢_{P} [θ](¬q \overline{S_{n}}) ← ⊤>>¬q \overline{M_{n}} for some θ  By inversion
Γ; D ⊢_{P} [θ]\overline{S_{n}} =^{·} \overline{M_{n}}  By inversion
· ⊢ \overline{M_{n}} ∈ ∥Not(\overline{N_{n}})∥  By definition of ∥ ∥
⊥  By term exclusivity with (∗)
Subcase: Γ; D ⊢_{P} ∀(¬q \overline{N_{n}} ← Not_{G}(G))>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{G}([σ]G)  By inversion
⊥  By IH 1 w.r.t. S_{1}^{+}

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q Γ; D ⊢_{P} D_{2}>>Q \\ & >>⊕ \\ Γ; D ⊢_{P} (D_{1} ⊕ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(D_{1} ⊕ D_{2})>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By sub-derivation
Γ; D ⊢_{P} D_{2}>>Q  By sub-derivation
Γ; D ⊢_{P} Not_{D}(D_{1}) ∧ Not_{D}(D_{2})>>¬Q  By rule Not_{D}⊕
Subcase: Γ; D ⊢_{P} Not_{D}(D_{1})>>¬Q  By inversion
⊥  By IH 2.1
Subcase: Γ; D ⊢_{P} Not_{D}(D_{2})>>¬Q  By inversion
⊥  By IH 2.1

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q \\ & >>∧ \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(D_{1} ∧ D_{2})>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By sub-derivation
Γ; D ⊢_{P} Not_{D}(D_{1}) ⊕ Not_{D}(D_{2})>>¬Q  By rule Not_{D}∧
Γ; D ⊢_{P} Not_{D}(D_{1})  By inversion
⊥  By IH 2.1

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{2}>>Q \\ & >>∧ \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(D_{1} ∧ D_{2})>>¬Q:

Γ; D ⊢_{P} D_{2}>>Q  By inversion
Γ; D ⊢_{P} Not_{D}(D_{1}) ⊕ Not_{D}(D_{2})>>¬Q  By rule Not_{D}∧
Γ; D ⊢_{P} Not_{D}(D_{2})>>¬Q  By inversion
⊥  By IH 2.1

2.2 Let D ⊑ def(q, P) and D′ ⊑ def(q, D). It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} Notα(D′)>>¬Q. By simultaneous induction on the structure of I^{+} and I^{−} and mutual induction on the structure of S^{+}:

No case for I^{+} ends in >>⊤

Case:

I^{+} = \frac{>>At}{Γ; D ⊢_{P} ⊥_{q}>>Q}

But by schema satisfaction there can be no formula in the dynamic definition of q.

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} [σ]\overline{S_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} [σ]G \\ & >> → \\ Γ; D ⊢_{P} ∀(q \overline{S_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(∀(q \overline{T_{n}} ← H))>>¬q \overline{M_{n}}, where ∀(q \overline{T_{n}} ← H) ⊑ def(q, D).

Γ; D ⊢_{P} [σ]\overline{S_{n}} =^{·} \overline{M_{n}}  By sub-derivation
Γ; D ⊢_{P} [σ]S_{i} =^{·} M_{i} for every 1 ≤ i ≤ n (∗)  By sub-derivation

Γ; D ⊢_{P} (⋀_{x∈dom(Γ)} Not_{x}^{C}(q \overline{T_{n}}) ∧ (⋀_{1≤i≤n,xR^{i}q} Not_{x}^{i}(q \overline{T_{n}}))) ∧ ∀(¬q \overline{T_{n}}) ← Not_{G}(G)>>¬q \overline{M_{n}} By rule Notα →

Subcase: Γ; D ⊢_{P} Not_{x}^{C}(q \overline{T_{n}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{1≤j≤n} ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q [e_{x}/Z_{j}]\overline{Z_{n}}>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{j}  By inversion
⊥  From line (∗) and S_{j} rigid
Subcase: Γ; D ⊢_{P} ⋀_{1≤i≤n,xR^{i}q} Not_{x}^{i}(q \overline{T_{n}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{x}^{i}(q \overline{T_{n}})>>¬q \overline{M_{n}}  By inversion

Γ; D ⊢_{P} ⋀_{1≤j≤n} ⋀_{N∈Γ⊢Not(T_{j})}(∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q [e_{x}/Z_{i}, N/Z_{j}]\overline{Z_{n}})>>¬q \overline{M_{n}}

By rule Not_{x}^{i} →

Γ; D ⊢_{P} e_{x} =^{·} M_{i}  By inversion
⊥  From line (∗) and S_{i} rigid
Subcase: Γ; D ⊢_{P} ∀(¬q \overline{T_{n}} ← Not_{G}(H))>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} [θ]\overline{T_{n}} =^{·} \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{j} for some 1 ≤ j ≤ n  By complementable clause
⊥  From line (∗) and S_{i} rigid

Case: I^{+} ends in >> →, I^{−} ends in >>⊥: But there can be no proof of ¬Q from Γ ⊢ Notα(⊥_{q}) = ⊤_{q}. Case: I^{+} ends in >> →, I^{−} ends in >>⊤:

Subcase: Γ = · or for all x ∈ dom(Γ), for all i, 1 ≤ i ≤ n it is not the case that xR^{i}q: then

Γ ⊢ Notα(⊤_{q}) = ⊤_{q} and an be no proof of ¬Q from ⊤_{q}.

Subcase: else Γ ⊢ Notα(⊤_{q}) = ⋀_{x∈dom(Γ)}(⋀_{1≤i≤n,xR^{i}q} Not_{x}^{C}(⊤_{q})); fix x, i:

Γ; D ⊢_{P} Not_{x}^{C}(⊤_{q})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{1≤i≤n} ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q [e_{x}/Z_{j}]\overline{Z_{n}}>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{j}  By inversion
⊥  Above line and rigidity restriction on S_{j} (∗).

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q Γ; D ⊢_{P} D_{2}>>Q \\ & >>⊕ \\ Γ; D ⊢_{P} (D_{1} ⊕ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢ Notα(D′)>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By sub-derivation
⊥  By IH 2.2

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q \\ & >>∧_{1} \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢ Notα(D′)>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By sub-derivation
⊥  By IH 2.2

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{2}>>Q \\ & >>∧_{2} \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢ Notα(D′)>>¬Q: Symmetric to the above. Case:

I^{−} = Γ; D ⊢_{P} Notα(D′_{1})>>¬Q >>∧_{1} Γ; D ⊢_{P} Notα(D′_{1} ⊕ D′_{2})>>¬Q

and I^{−} ends in Γ; D ⊢ D>>Q. By IH 2.2 Case:

I^{−} = Γ; D ⊢_{P} Notα(D′_{2})>>¬Q >>∧_{2} Γ; D ⊢_{P} Notα(D′_{1} ⊕ D′_{2})>>¬Q

and I^{−} ends in Γ; D ⊢ D>>Q. By IH 2.2.

Case:

I^{−} = Γ; D ⊢_{P} Notα(D′_{1})>>¬Q Γ; D ⊢_{P} Notα(D′_{2})>>¬Q >>⊕ Γ; D ⊢_{P} Notα(D′_{1} ∧ D′_{2})>>¬Q

and I^{−} ends in Γ; D ⊢ D>>Q. By IH 2.2.

2.3 Let D ⊑ def(q, D) and D′ ⊑ def(q, P). It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} Not_{D}(D′)>>¬Q. By simultaneous induction on the structure of I^{+} and I^{−} and mutual induction on the structure of S^{+}: note that by the restriction to complementable programs, some SPE e_{x} occurs in D.

No case for for I^{+} ends in >>⊤.

No case for for I^{+} ends in >>⊥, since by the restriction to complementable clauses, ⊥ cannot occur as an assumption.

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} [σ]\overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} [σ]H \\ & >> → \\ Γ; D ⊢_{P} ∀(q \overline{N_{e_{x}}^{i}} ← H)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Not_{D}(∀(q \overline{S_{n}} ← G))>>¬q \overline{M_{n}}.

Γ; D ⊢_{P} [σ]\overline{N_{e_{x}}^{i}} =^{·} \overline{M_{n}}  By sub-derivation
Γ; D ⊢_{P} e_{x} =^{·} M_{i} (∗) for some 1 ≤ i ≤ n  By sub-derivation
Γ; D ⊢_{P} ⋀_{\overline{T_{n}}∈·⊢Not(\overline{S_{n}})} ∀(¬q \overline{T_{n}} ← ⊤) ∧ ∀(¬q \overline{S_{n}} ← Not_{G}(G))>>¬q \overline{M_{n}}  By rule Not_{D} →
Subcase: Γ; D ⊢_{P} ⋀_{\overline{T_{n}}∈·⊢Not(\overline{S_{n}})} ∀(¬q \overline{T_{n}} ← ⊤)>>q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ∀(¬q \overline{T_{n}} ← ⊤)>>q \overline{M_{n}} for some \overline{T_{n}} ∈ · ⊢ Not(\overline{S_{n}})  By inversion
Γ; D ⊢_{P} [θ](¬q \overline{T_{n}} ← ⊤)>>¬q \overline{M_{n}} for some θ  By inversion
Γ; D ⊢_{P} [θ]\overline{T_{n}} =^{·} \overline{M_{n}}  By inversion
Γ; D ⊢_{P} [θ]T_{i} =^{·} M_{i}  By inversion
⊥  (∗) and Lemma 0.1 on above line
Subcase: Γ; D ⊢_{P} ∀(¬q \overline{S_{n}} ← Not_{G}(G))>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} [θ′]\overline{S_{n}} =^{·} \overline{M_{n}}  By inversion
Γ; D ⊢_{P} [θ′]S_{i} =^{·} M_{i}  By inversion
⊥  From line (∗) and S_{i} rigid.

No case for I^{+} ends in >> →, I^{−} ends in >>⊥: if ⊤_{q} is the only definition for q, then by schema satisfaction ∀(q \overline{S_{n}} ← G) could not be an assumption.

Case: I^{+} ends in >> →, I^{−} ends in >>⊥: ditto.

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q \\ & >>∧_{1} \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢ Not_{D}(D′)>>¬Q:

Γ; D ⊢_{P} D_{1}>>Q  By sub-derivation
⊥  By IH 2.2

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{2}>>Q \\ & >>∧_{2} \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢ Not_{D}(D′)>>¬Q: Symmetric to the above.

Case:

I^{−} = Γ; D ⊢_{P} Not_{D}(D′_{1})>>¬Q >>∧_{1} Γ; D ⊢_{P} Not_{D}(D′_{1} ⊕ D′_{2})>>¬Q

and I^{−} ends in Γ; D ⊢ D>>Q. By IH 2.2

Case:

I^{−} = Γ; D ⊢_{P} Not_{D}(D′_{2})>>¬Q >>∧_{2} Γ; D ⊢_{P} Not_{D}(D′_{1} ⊕ D′_{2})>>¬Q

and I^{−} ends in Γ; D ⊢ D>>Q. By IH 2.2.

Case:

I^{−} = Γ; D ⊢_{P} Not_{D}(D′_{1})>>¬Q Γ; D ⊢_{P} Not_{D}(D′_{2})>>¬Q >>⊕ Γ; D ⊢_{P} Not_{D}(D′_{1} ∧ D′_{2})>>¬Q

and I^{−} ends in Γ; D ⊢ D>>Q. By IH 2.2.

2.4 Let D ⊑ def(q, D) and D′ ⊑ def(q, D). There are two main cases, according to whether D and D′ belong to the same block (and in this case it suffice to consider D ≡ D′) or not:

1. It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} Notα(D)>>¬Q. By mutual induction on the structure of I^{+} and S^{+}.

Case:

I^{+} = \frac{>>At}{Γ; D ⊢_{P} ⊥_{q}>>Q}

But there can be no proof of ¬Q from Notα(⊥_{q}) = ⊤_{q}.

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} [σ]G \\ & >> → \\ Γ; D ⊢_{P} ∀(q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(∀(q \overline{N_{n}} ← G))>>¬q \overline{M_{n}}.

S_{1}^{+} :: Γ; D ⊢_{P} [σ]G  By sub-derivation
Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}}  By sub-derivation

Γ; D ⊢_{P} (⋀_{x∈dom(Γ)} Not_{x}^{C}(q \overline{N_{n}}) ∧ (⋀_{1≤i≤n,xR^{i}q} Not_{x}^{i}(q \overline{N_{n}}))) ∧ ∀(¬q \overline{N_{n}}) ← Not_{G}(G)>>¬q \overline{M_{n}}

By rule Notα →

Γ; D ⊢_{P} [σ]N_{i} =^{·} M_{i} (+) for all 1 ≤ i ≤ n  By inversion
Γ ⊢ M_{i} ∈ ∥N_{i}∥ (∗) for all 1 ≤ i ≤ n  By inversion

Subcase: [σ]N_{i} ≢ e_{x}, [σ]N_{i} rigid:

Γ; D ⊢_{P} Not_{x}^{C}(q \overline{N_{n}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{1≤i≤n} ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q [e_{x}/Z_{j}]\overline{Z_{n}}>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{j}  By inversion
⊥  Above line and (+).

Subcase: [σ]N_{i} ≡ e_{x}:

Γ; D ⊢_{P} (⋀_{1≤i≤n,xR^{i}q} Not_{x}^{i}(q \overline{N_{n}})))>>[σ]¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{x}^{i}(\overline{N_{n}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{1≤i≤n} ⋀_{N∈Γ⊢Not(M_{i})} ∀(¬q [e_{x}/Z_{i}, N/Z_{j}]\overline{Z_{n}} ← ⊤)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{N∈Γ⊢Not(M_{i})} ∀(¬q [e_{x}/Z_{i}, N/Z_{j}]\overline{Z_{n}} ← ⊤)>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} M_{i} =^{·} [θ]N  By inversion
Γ ⊢ M_{i} ∈ ∥N∥ for some N ∈ Γ ⊢ Not(N_{i})  By definition of ∥ ∥
⊥  By term exclusivity (??) with line (∗)
Subcase: Γ; D ⊢_{P} ¬∀(q \overline{N_{n}} ← Not_{G}(G))>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} Not_{G}([σ]G)  By inversion
⊥  By IH 1 on S_{1}^{+}

Case: I^{+} ends in >>⊕, >>∧, >>∀: by IH 2.4.1 similarly to case 2.1 with Notα in place of Not_{D}.

2. It is not the case that I^{+} :: Γ; D ⊢_{P} D>>Q and I^{−} :: Γ; D ⊢_{P} Notα(D′)>>¬Q. By simultaneous

induction on the structure of I^{+} and I^{−}: No case for I^{+} ends in >>⊤. No case for I^{+} ends in >>⊥, by restriction to complementable clauses andschema satisfaction. No case for I^{+} ends in >> →, I^{−} ends in >>⊥, as above.

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} [σ]G \\ & >> → \\ Γ; D ⊢_{P} ∀(q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(∀(q \overline{S_{n}} ← G′))>>¬q \overline{M_{n}}, from a different block.

S_{1}^{+} :: Γ; D ⊢_{P} [σ]G  By sub-derivation
Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}}  By sub-derivation

Γ; D ⊢_{P} (⋀_{x∈dom(Γ)} Not_{x}^{C}(q \overline{S_{n}}) ∧ (⋀_{1≤i≤n,xR^{i}q} Not_{x}^{i}(q \overline{S_{n}}))) ∧ ∀(¬q \overline{S_{n}}) ← Not_{G}(G′)>>¬q \overline{M_{n}}

By rule Notα →

Γ; D ⊢_{P} [σ]N_{i} =^{·} M_{i} (+) for all 1 ≤ i ≤ n  By inversion
Γ ⊢ M_{i} ∈ ∥N_{i}∥ (∗) for all 1 ≤ i ≤ n  By inversion

Subcase: [σ]N_{i} ≢ e_{x}, [σ]N_{i} rigid:

Γ; D ⊢_{P} Not_{x}^{C}(q \overline{N_{n}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{1≤i≤n} ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q [e_{x}/Z_{j}]\overline{Z_{n}}>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{j}  By inversion
⊥  Above line and (+).

Subcase: [σ]N_{i} ≡ e_{x}:

⊥  Above line and (+).
Subcase: Γ; D ⊢_{P} ¬∀(q \overline{S_{n}} ← Not_{G}(G′))>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} [σ]\overline{S_{n}} =^{·} \overline{M_{n}}  By inversion
⊥  Above line and (+).

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}} Γ; D ⊢_{P} [σ]G \\ & >> → \\ Γ; D ⊢_{P} ∀(q \overline{N_{n}} ← G)>>q \overline{M_{n}} \end{aligned}

and I^{−} ends in Γ; D ⊢_{P} Notα(⊤_{q}))>>¬q \overline{M_{n}}, from a different block.

S_{1}^{+} :: Γ; D ⊢_{P} [σ]G  By sub-derivation
Γ; D ⊢_{P} [σ]\overline{N_{n}} =^{·} \overline{M_{n}}  By sub-derivation

Γ; D ⊢_{P} ⋀_{x∈dom(Γ)}(⋀_{1≤i≤n,xR^{i}q} Not_{x}^{C}(⊤_{q})>>¬q \overline{M_{n}}

By rule Notα⊤

Γ; D ⊢_{P} [σ]N_{i} =^{·} M_{i} (+) for all 1 ≤ i ≤ n  By inversion
Γ ⊢ M_{i} ∈ ∥N_{i}∥ (∗) for all 1 ≤ i ≤ n  By inversion
[σ]N_{i} ≢ e_{x}, [σ]N_{i} rigid: Γ; D ⊢_{P} Not_{x}^{C}(q \overline{N_{n}})>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} ⋀_{1≤i≤n} ∀Z_{1} :A_{1}…. ∀Z_{n}:A_{n}. ¬q [e_{x}/Z_{j}]\overline{Z_{n}}>>¬q \overline{M_{n}}  By inversion
Γ; D ⊢_{P} e_{x} =^{·} M_{j}  By inversion
⊥  Above line and (+).

Case:

I^{+} = \begin{aligned}Γ; D ⊢_{P} D_{1}>>Q \\ & >>∧_{1} \\ Γ; D ⊢_{P} (D_{1} ∧ D_{2})>>Q \end{aligned}

and I^{−} ends in Γ; D ⊢ Notα(D′)>>¬Q:
Γ; D ⊢_{P} D_{1}>>Q  By sub-derivation
⊥  By IH 2.4.2

Case: I^{+} ends in >>∧_{1}, >>⊕, I^{−} ends in >>∧_{i}, >>⊕: analogously by IH 2.4.2. 1 By induction on the structure of S^{+}.

Case:

S^{+} = Γ; D ⊢_{P} def(q, P ∧ D)>>Q ⊢ atm Γ; D ⊢_{P} Q

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(Q):

Γ; D ⊢_{P} def(q, P ∧ D)>>Q  By sub-derivation
Γ; D ⊢_{P} ¬Q  By rule Not_{G}At
Γ; D ⊢_{P} def(¬q, P ∧ D)>>¬Q  By inversion
⊥  By IH 2.i, i ∈ {1, 2, 3, 4} according to static or dynamic definition

Case:

S^{+} = \begin{aligned}Γ; D ⊢_{P} G_{1} Γ; D ⊢_{P} G_{2} \\ & ⊢ ∧ \\ Γ; D ⊢_{P} G_{1} ∧ G_{2} \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(G_{1} ∧ G_{2})

Γ; D ⊢_{P} G_{1}  By sub-derivation
Γ; D ⊢_{P} G_{2}  By sub-derivation
Γ; D ⊢_{P} Not_{G}(G_{1}) ∨ Not_{G}(G_{2})  By rule Not_{G}∧
Subcase: Γ; D ⊢_{P} Not_{G}(G_{1})  By inversion
⊥  By IH 1
Subcase: Γ; D ⊢_{P} Not_{G}(G_{2})  By inversion
⊥  By IH 1

Case:

S^{+} = \begin{aligned}Γ; D ⊢_{P} G_{1} \\ & ⊢ ∨ \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(G_{1} ∨ G_{2})

Γ; D ⊢_{P} G_{1}  By sub-derivation
Γ; D ⊢_{P} Not_{G}(G_{1}) ∧ Not_{G}(G_{2})  By rule Not_{G}∨
Γ; D ⊢_{P} Not_{G}(G_{1})  By inversion
⊥  By IH 1

Case:

S^{+} = \begin{aligned}Γ; D ⊢_{P} G_{2} \\ & ⊢ ∨ \\ Γ; D ⊢_{P} G_{1} ∨ G_{2} \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(G_{1} ∨ G_{2}). Symmetrical.

Case:

S^{+} = \begin{aligned}(Γ, y:A); D ⊢_{P} [y/x]G′ \\ & ⊢∀^{∗} \\ Γ; D ⊢_{P} ∀x:a. G′ \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(∀x:a. G′):
(Γ, y:A); D ⊢_{P} [y/x]G′  By sub-derivation
(Γ, y:A); D ⊢_{P} Not_{G}([y/x]G′)  By rule Not_{G}∀
⊥  By IH 1

Case:

S^{+} = \begin{aligned}Γ; (D ∧ D′) ⊢_{P} G′ \\ & ⊢ → \\ Γ; D ⊢_{P} D′ → G′ \end{aligned}

and S^{−} ends in Γ; D ⊢_{P} Not_{G}(D′ → G′):
Γ; (D ∧ D′) ⊢_{P} G′  By sub-derivation
Γ; D ⊢_{P} D′ → Not_{G}(G′)  By rule Not_{G} →
Γ; (D ∧ D′) ⊢_{P} Not_{G}(G′)  By inversion
⊥  By IH 1

Case: The (dis)equality case follows from the decidability of the (dis)equality judgment.

□

Note that the proof goes through as there is no ‘bad’ interaction between the static and dynamic definition of a predicate; namely in sub-case 2.2 there is no overlap between a clause from def(q, P) and def(¬q, D) since in every atomic assumption there must be an occurrence of a new parameter and every term at the same position in a program clause head must be rigid. Symmetrically for 2.3. Sub-case 2.4 holds analogously to the first case 2.1, which is based on term exclusivity (Corollary ??). In the latter case, it suffices to consider, for D ⊑ def(q, P), only Γ; D ⊢_{P} D>>Q and Γ; D ⊢_{P} Not_{D}(D)>>¬Q, because the positive definition is a conjunction, while the negative one is a disjunction; the same remark applies when the definition is dynamic (2.4). The condition for programs to require clause heads with rigid terms may seem too restrictive; the natural way to relax it, requiring that only one of those terms which occur in the same position of a parameter in each assumption needs to be rigid, turns out to be inconsistent; consider the following example:

plam : p (lam E) (lam F) ← ∀x:exp. p (E x) (F x).
papp : p (app E_{1} E_{2}) F.

Augmentation will insert the clause ∀(¬p x H ∧ ¬p H′ x), which now overlaps with papp. As a result both p (lam(λx:exp. app x x)) (lam(λy:exp. y)) and its negation are provable. As we remarked earlier, the rigidity condition applies only to predicate definitions which are mutually recursive to non-Horn ones. Thus, any such program which uses a ‘catch-all’ clause is those positions is forbidden; nevertheless it is easy to avoid catch-all clauses via explicit coercion or (sometimes) partial evaluation. Finally, we remark that any other (decidable) condition which avoids overlap between static and dynamic clauses will do; the one we have proposed is statically checkable, certainly not ‘ad hoc’ and has been dictated by the practice of logical frameworks.