Appendix D Abstractors

The abstractors extend the syntax, especially the set of ASK-formulas, while keeping the interpretation domain unchanged. In information systems, this is mainly used to enhance the expressivity of queries, while keeping the description language unchanged. This is usually done by adding more abstract/general formulas (e.g., intervals, boolean connectives).

D.1 Top/1

Addition of a top to the syntax of a logic.

D.1.1 Parameters

X ∈ L:: the logic to which a top is to be added.

D.1.2 Syntax

AS =_def AS_X ⊎ {1}
TELL =_def TELL_X
ASK =_def ASK_X ⊎ {1}

D.1.3 Semantics

domain:

I = I_X.

satisfaction:

i ⊨ f =_def

⎧
⎨
⎩

true	if f = 1
i ⊨_X f	if f ∈ AS_X

D.1.4 Operations

subsumption:

f ⊑ g =_def

⎧
⎨
⎩

true	if g = 1
⊤_X ⊑_X g	if f = 1 g ∈ AS_X
f ⊑_X g	if f, g ∈ AS_X

tautology:

⊤ =_def 1.

contradiction:

⊥ =_def ⊥_X.

conjunction:

f ⊓ g =_def

⎧
⎨
⎩

f	if g = 1
g	if f = 1
f ⊓_X g	if f, g ∈ AS_X

disjunction:

f ⊔ g =_def

⎧
⎨
⎩

{1}	if f = 1 g = 1
f ⊔_X g	if f, g ∈ AS_X

D.1.5 Properties

df ⇐ df_X
st' ⇐ st'_X

Proof: d ∈ TELL ⇒ d ∈ TELL_X
⇒ M_X(d) ≠ ∅ (st'_X)
⇒ M(d) ≠ ∅. ■
sg' ⇐ sg'_X

Proof: d ∈ TELL ⇒ d ∈ TELL_X ⇒ Card(M_X(d)) = 1 (sg'_X)
⇒ Card(M(d)) = 1. ■
cs_⊑⇐ cs_{⊑_X} cp_{⊤_X}

Proof: f ⊑ g implies
- either g = 1:
  ⇒ M(g) = I ⇒ M(f) ⊆ M(g).
- or f = 1, g ∈ AS_X, ⊤_X ⊑_X g (def(⊤_X)):
  ⇒ M_X(⊤_X) ⊆ M_X(g) (cs_{⊑_X})
  ⇒ I_X ⊆ M_X(g) (cp_{⊤_X})
  ⇒ M(f) ⊆ M(g) = I.
- or f,g ∈ AS_X, f ⊑_X g:
  ⇒ M_X(f) ⊆ M_X(g) (cs_{⊑_X})
  ⇒ M(f) ⊆ M(g).
Hence in all cases M(f) ⊆ M(g). ■
cp_⊑⇐ cp_{⊑_X} reduced.top_X

Proof: M(f) ⊆ M(g) implies
- either g = 1:
  ⇒ f ⊑ g.
- or f = 1, g ∈ AS_X:
  ⇒ M(f) = I ⊆ M(g)
  ⇒ ∩_{k ∈ ∅}M(k) ⊆ ∪_{l ∈ {g}}M(l)
  ⇒ ∅ ⊑_X^* {g} (reduced.top_X)
  ⇒ ⊤_X ⊑ g ⇒ f ⊑ g.
- or f, g ∈ AS_X:
  ⇒ M_X(f) ⊆ M_X(g)
  ⇒ f ⊑_X g (cp_{⊑_X})
  ⇒ f ⊑ g.
Hence in all cases f ⊑ g. ■
cp'_⊑⇐ cp'_{⊑_X}

Proof: Let d ∈ TELL, x ∈ ASK.
M(f) ⊆ M(g) implies
- either g = 1:
  ⇒ d ⊑ x.
- or d ∈ TELL_X, x ∈ ASK_X:
  ⇒ M_X(d) ⊆ M_X(x)
  ⇒ d ⊑_X x (cp'_{⊑_X})
  ⇒ d ⊑ x.
Hence in all cases d ⊑ x. ■
cp_⊤

Proof: M(⊤) = M(1) = I. ■
cs_⊥⇐ cs_{⊥_X}

Proof: M(⊥) = M(⊥_X) = M_X(⊥_X) = ∅ (cs_{⊥_X}). ■
defst_⊓⇐ defst_{⊓_X}

Proof: Assume M(f) ∩ M(g) ≠ ∅.
If f = 1 or g = 1, then f ⊓ g is defined. Otherwise, f, g ∈ AS_X
⇒ M_X(f) ∩ M_X(g) ≠ ∅
⇒ def(f ⊓_X g) (defst_{⊓_X})
⇒ def(f ⊓ g). ■
cs_⊓⇐ cs_{⊓_X}
cp_⊓⇐ cp_{⊓_X}
cs_⊔⇐ cs_{⊔_X}
cp_⊔⇐ cp_{⊔_X}
reduced(F,G) ⇐ 1 ∈ G (1 ∉ G reduced_X(F \ {1}, G))
reduced ⇐ reduced_X
reduced.bot ⇐ reduced.bot_X
reduced.bot' ⇐ reduced.bot'_X
reduced.top ⇐ reduced.top_X
reduced' ⇐ reduced'_X

Proof: Let us consider 2 cases:
- either 1 ∈ G:
  ⇒ ∃ g ∈ G: ⊤ ⊑ g
  ⇒ F ⊑^* G.
- or 1 ∉ G:
  ∩_{f ∈ F}M(f) ⊆ ∪_{g ∈ G}M(g)
  ⇒ ∩_{f ∈ F \ {1}}M(f) ⊆ ∪_{g ∈ G}M(g)
  ⇒ F \ {1} ⊑_X^* G (reduced_X(F \ {1},G))
  ⇒ F ⊑^* G (definition of ⊑^*).
Hence in all cases ∩_{f ∈ F}M(f) ⊆ ∪_{g ∈ G}M(g) ⇒ F ⊑^* G. ■

D.2 Interval/1

The intervals over values that are formulas of another logic. This supposes the sub-logic has an ordering over its interpretations, and has its operations ≤ and ⋜ defined.

D.2.1 Parameters

V ∈ L:: a logic of values, equiped with operators ≤, and ⋜, and whose semantics is equipped with an ordering ≤.

D.2.2 Syntax

AS =_def AS_V × AS_V
ASK =_def ASK_V × ASK_V
TELL =_def {(d,d) ∣ d ∈ TELL_V}

Formula (a,b), where a,b ∈ AS_V, is only well-formed when a ≤_V b or a ⋜_V b (ensures the interval is not empty).

D.2.3 Semantics

domain:: I =_def I_V
ordering:: i ≤ j =_def i ≤_V j)
satisfaction:: i ⊨ (a,b) =_def ∃ i_a ∈ M_V(a), i_b ∈ M_V(b): i_a ≤_V i ≤_V i_b

D.2.4 Operations

subsumption:: (a₁,b₁) ⊑ (a₂,b₂) =_def a₂ ≤_V a₁ b₁ ⋜_V b₂

D.2.5 Properties

df ⇐ df_V
st ⇐ st_V cs_{≤_V} cs_{⋜_V}
st' ⇐ st'_V cs_{≤_V} cs_{⋜_V}
Proof: (a,b) ∈ AS ⇒ a,b ∈ AS_V (a ≤_V b a ⋜_V b)
⇒ M_V(a) ≠ ∅ M_V(b) ≠ ∅. (st_V)
Now,
- either a ≤_V b:
  ⇒ ∀ i_b ∈ M_V(b): ∃ i_a ∈ M_V(a): i_a ≤_V i_b (cs_{≤_V})
  ⇒ ∃ i_b ∈ M_V(b), i_a ∈ M_V(a): i_a ≤_V i_b (M_V(b) ≠ ∅)
  ⇒ ∃ i ∈ M((a,b)) ⇒ M((a,b)) ≠ ∅.
- or a ⋜_V b:
  ⇒ ∀ i_a ∈ M_V(a): ∃ i_b ∈ M_V(b): i_a ≤_V i_b (cs_{⋜_V})
  ⇒ ∃ i_a ∈ M_V(a), i_b ∈ M_V(b): i_a ≤_V i_b (M_V(a) ≠ ∅)
  ⇒ ∃ i ∈ M((a,b)) ⇒ M((a,b)) ≠ ∅. ■
sg' ⇐ sg'_V

Proof: Let (d,d) ∈ TELL. Suppose some interpretation i ∈ I s.t. i ⊨ (d,d)
⇒ ∃ i_a,i_b ∈ M_V(d): i_a ≤_V i ≤_V i_b
⇒ i_d ≤_V i ≤_V i_d, where i_d is the unique model of d (sg'_V)
⇒ i = i_d.
Hence M((d,d)) = M_V(d) = {i_d}. ■
cs_⊑⇐ cs_{≤_V} cs_{⋜_V}

Proof: (a₁,b₁) ⊑ (a₂,b₂)
⇒ a₂ ≤ a₁ b₁ ⋜ b₂
⇒ ∀ i₁ ∈ M_V(a₁): ∃ i₂ ∈ M_V(a₂): i₂ ≤ i₁ (cs_{≤_V})
∀ i₁ ∈ M_V(b₁): ∃ i₂ ∈ M_V(b₂): i₁ ≤ i₂ (cs_{⋜_V})
Now i ⊨ (a₁,b₁)
⇒ ∃ i₁ ∈ M_V(a₁): i₁ ≤ i
∃ i₁ ∈ M_V(b₁): i ≤ i₁
⇒ ∃ i₁ ∈ M_V(a₁), i₂ ∈ M_V(a₂): i₂ ≤ i₁ ≤ i
∃ i₁ ∈ M_V(b₁), i₂ ∈ M_V(b₂): i ≤ i₁ ≤ i₂
⇒ ∃ i₂ ∈ M_V(a₂): i₂ ≤ i ∃ i₂ ∈ M_V(b₂): i ≤ i₂
⇒ i ⊨ (a₂,b₂).

Hence M((a₁,b₁)) ⊆ M((a₂,b₂)). ■
cp_⊑⇐ cp_{≤_V} cp_{⋜_V}

Proof: M((a₁,b₁)) ⊆ M((a₂,b₂))
⇒ ∀ i ∈ I: i ⊨ (a₁,b₁) ⇒ i ⊨ (a₂,b₂)
⇒ ∀ i ∈ I: (∃ i_a ∈ M_V(a₁): i_b ∈ M_V(b₁): i_a ≤ i ≤ i_b)
⇒ (∃ i_a ∈ M_V(a₂): i_b ∈ M_V(b₂): i_a ≤ i ≤ i_b)
⇒ ∀ i ∈ M_V(a₁): (∃ i_a ∈ M_V(a₁), i_b ∈ M_V(b₁): i_a ≤ i ≤ i_b) ⇒ ∃ i₂ ∈ M_V(a₂): i₂ ≤ i
Then choose i_a = i = i_b:
⇒ ∀ i₁ ∈ M_V(a₁): ∃ i₂ ∈ M_V(a₂): i₂ ≤ i₁
⇒ a₂ ≤ a₁ (cp_{≤_V}).

Similarly, we get the similar result with b₂ (cp_{⋜_V}):
∀ i₁ ∈ M_V(b₁): ∃ i₂ ∈ M_V(b₂): i₁ ≤ i₂
⇒ b₁ ⋜ b₂.
These 2 propositions are the definition of (a₁,b₁) ⊑ (a₂,b₂), which terminates the proof. ■

D.3 Bounds/1 ⊇ λ X.Sum(X,Sum({−∞},{+∞}))

Add bounds w.r.t. the ordering over formulas (as used by Interval). These bounds are added as both formulas and interpretations. This functor is defined as an extension of the combinator given in the section title ({−∞} stands for the logic functor Unit where −∞ is the only formula). This means it inherits everything from this combinator, and possibly redefines part of it.

D.3.1 Parameters

X ∈ L:: a logic of values.

D.3.2 Semantics

ordering:

i ≤ j =_def ∨

⎧
⎨
⎩

i = −∞

j = +∞

i,j ∈ I_X i ≤_X j

D.3.3 Operations

lower ordering:

f ≤ g =_def ∨

⎧
⎪
⎨
⎪
⎩

g = 0

f = −∞

g = +∞

f,g ∈ AS_X f ≤_X g

upper ordering:

f ⋜ g =_def ∨

⎧
⎪
⎨
⎪
⎩

f = 0

f = −∞

g = +∞

f,g ∈ AS_X f ⋜_X g

D.3.4 Properties

cs_≤⇐ cs_{≤_X} st

Proof: f ≤ g implies:
- either g = 0: M(g) = ∅ ⇒ ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j.
- or f = −∞:
  ∀ j ∈ M(g): −∞ ≤ j ⇒ ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j.
- or g = +∞: then,
  - f = −∞: ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j (i=−∞, j=+∞)
  - f = +∞: ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j (i=j=+∞)
  - f ∈ AS_X: M(f) = M_X(f) ≠ ∅ (st_X)
    ⇒ ∃ i ∈ M(f): i ≤ +∞
    ⇒ ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j.
- or f, g ∈ AS_X f ≤_X g:
  ⇒ ∀ j ∈ M_X(g): ∃ i ∈ M_X(f): i ≤_X j (cs_{≤_X})
  ⇒ ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j. (Sum).
Hence in all cases, ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j. ■
cp_≤⇐ cp_{≤_X} st_X

Proof: f ¬ ≤g implies
- either f = 0 g ≠ 0:
  - g = −∞: M(g) ≠ ∅
  - g = +∞: M(g) ≠ ∅
  - g ∈ AS_X: M(g) = M_X(g) ≠ ∅ (st_X)
  Hence in all cases, M(g) ≠ ∅, and M(f) = ∅
  ⇒ ∃ j ∈ M(g): ∀ i ∈ M(f): i ¬ ≤j.
- or f = +∞ g = −∞: ∃ j ∈ M(g): ∀ i ∈ M(f): i ≤ j
- or f = +∞ g ∈ AS_X: M(g) = M_X(g) ≠ ∅ (st_X)
  ⇒ ∃ j ∈ M(g): +∞ ¬ ≤j
  ⇒ ∃ j ∈ M(g): ∀ i ∈ M(f): i ¬ ≤j.
- or f ∈ AS_X g = −∞:
  ⇒ ∀ i ∈ M(f): i ¬ ≤−∞
  ⇒ ∃ j ∈ M(g): ∀ i ∈ M(f): i ¬ ≤j.
- or f, g ∈ AS_X f ¬ ≤_X g:
  ⇒ ∃ j ∈ M_X(g): ∀ i ∈ M_X(f): i ¬ ≤_X j (cp_{≤_X})
  ⇒ ∃ j ∈ M(g): ∀ i ∈ M(f): i ¬ ≤j. (Sum)
Hence in all cases, ¬ ∀ j ∈ M(g): ∃ i ∈ M(f): i ≤ j. ■
cs_⋜⇐ cs_{⋜_X} st

Proof: f ⋜ g implies:
- either f = 0: M(f) = ∅ ⇒ ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j.
- or g = +∞:
  ∀ i ∈ M(f): i ≤ +∞ ⇒ ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j.
- or f = −∞: then,
  - g = +∞: ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j (i=−∞, j=+∞)
  - g = −∞: ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j (i=j=−∞)
  - g ∈ AS_X: M(g) = M_X(g) ≠ ∅ (st_X)
    ⇒ ∃ j ∈ M(g): −∞ ≤ j
    ⇒ ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j.
- or f, g ∈ AS_X f ⋜_X g:
  ⇒ ∀ i ∈ M_X(f): ∃ j ∈ M_X(g): i ≤_X j (cs_{⋜_X})
  ⇒ ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j. (Sum).
Hence in all cases, ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j. ■
cp_⋜⇐ cp_{⋜_X} st_X

Proof: f ¬ ⋜g implies
- either f ≠ 0 g = 0:
  - f = −∞: M(f) ≠ ∅
  - f = +∞: M(f) ≠ ∅
  - f ∈ AS_X: M(f) = M_X(f) ≠ ∅ (st_X)
  Hence in all cases, M(f) ≠ ∅, and M(g) = ∅
  ⇒ ∃ i ∈ M(f): ∀ j ∈ M(g): i ¬ ≤j.
- or f = +∞ g = −∞: ∃ i ∈ M(f): ∀ j ∈ M(g): i ≤ j
- or f ∈ AS_X g = −∞: M(f) = M_X(f) ≠ ∅ (st_X)
  ⇒ ∃ i ∈ M(f): i ¬ ≤−∞
  ⇒ ∃ i ∈ M(f): ∀ j ∈ M(g): i ¬ ≤j.
- or f = +∞ g ∈ AS_X:
  ⇒ ∀ j ∈ M(g): +∞ ¬ ≤j
  ⇒ ∃ i ∈ M(f): ∀ j ∈ M(g): i ¬ ≤j.
- or f, g ∈ AS_X f ¬ ⋜_X g:
  ⇒ ∃ i ∈ M_X(f): ∀ j ∈ M_X(g): i ¬ ≤_X j (cp_{⋜_X})
  ⇒ ∃ i ∈ M(f): ∀ j ∈ M(g): i ¬ ≤j. (Sum)
Hence in all cases, ¬ ∀ i ∈ M(f): ∃ j ∈ M(g): i ≤ j. ■

D.4 Prop/1

The boolean closure of a given logic. It can also be seen as the usual propositional logic, whose atoms are replaced by the formulas of a logic given as a parameter.

D.4.1 Parameters

A ∈ L:: a logic, whose formulas play the role of atoms in propositional logic.

D.4.2 Syntax

AS is the smallest set of formulas that contains AS_A (atoms), 1 (true), 0 (false), and is closed by the application of the unary operator ¬ (negation), and the binary operators (conjunction) and (disjunction). ASK is the subset of propositions whose atoms are all in ASK_A. TELL is the subset of propositions, whose negative atoms are all in ASK_A, whose positive atoms are all in TELL_A ∪ ASK_A, and such that every conjunctive clause contains a positive literal in TELL_A. Positive atoms are those under the scope of an even number of negations; and negative atoms are those under the scope of an odd number of negations.

D.4.3 Semantics

domain:

I = I_A.

satisfaction:

i ⊨ a	=_def	i ⊨_A a
i ⊨ 1	=_def	true
i ⊨ 0	=_def	false
i ⊨ ¬ f	=_def	i ¬ ⊨f
i ⊨ f g	=_def	i ⊨ f and i ⊨ g
i ⊨ f g	=_def	i ⊨ f or i ⊨ g

D.4.4 Operations

subsumption:

f ⊑ g is true iff there exists a proof of the sequent ⊢ ¬ f g in the sequent calculus of Table D.1.

In the rules, Δ is always a set of literals (i.e., atomic formulas or negations of atomic formulas), Γ is a sequence of propositions, L is a literal, X is a proposition, β is the disjunction of β₁…β_n, α is the conjunction of α₁…α_n, and L denotes the negation of L (a := ¬ a and ¬ a := a). The tautology 1 is equivalent to the empty conjunction, and the contradiction 0 is equivalent to the empty disjunction.

⊤ -Axiom: ¬ b, Δ ⊢ Γ if def_{⊤_A} and ⊤_A ⊑_A b

⊥-Axiom: a, Δ ⊢ Γ if def_{⊥_A} and a ⊑_A ⊥_A

⊑-Axiom: a, ¬ b, Δ ⊢ Γ if a ⊑_A b

⊓ -Rule:

a ⊓_A b, Δ ⊢ Γ

a, b, Δ ⊢ Γ
if def_⊓(a,b)

⊔ -Rule:

¬(a ⊔_A b), Δ ⊢ Γ

¬ a, ¬ b, Δ ⊢ Γ


¬ ¬ -Rule:

Δ ⊢ X, Γ

Δ ⊢ ¬ ¬ X, Γ

           literal-Rule:

L
, Δ ⊢ Γ

Δ ⊢ L, Γ

β -Rule:

Δ ⊢ β₁, …, β_n, Γ

Δ ⊢ β, Γ

           α -Rule:

Δ ⊢ α₁, Γ … Δ ⊢ α_n, Γ

Δ ⊢ α, Γ

Table D.1: Sequent calculus for deduction in propositional logic.

conjunction:

f ⊓ g =_def f g.

disjunction:

f ⊔ g =_def f g.

tautology:

⊤ =_def 1.

contradiction:

⊥ =_def 0.

D.4.5 Properties

Definition 9 A sequent Δ ⊢ Γ is valid iff ∩_{δ ∈ Δ}M(δ) ⊆ ∪_{γ ∈ Γ}M(γ).

Definition 10 The expression Trees(Δ ⊢ Γ) denotes the set of all fully developed trees whose root is the sequent Δ ⊢ Γ.

Definition 11 A fully developed tree t is said open, denoted by open(t), iff it contains an open sequent (necessary a leaf from definition of an open sequent), i.e. ∃ A, B ⊢ ∈ t: open(A,B).

df ⇐ df_A
cs_⊑⇐ cs_{⊑_A} ∧ cp_{⊓_A} ∧ cs_{⊔_A} ∧ cp_{⊤_A} ∧ cs_{⊥_A}

Proof:
- Let us show that ⊑-Axiom is valid:
  a ⊑_A b ⇒ M_A(a) ⊆ M_A(b) cs_{⊑_A}
  ⇒ M(a) ⊆ M(b) ⇒ ∀ i ∈ I: i ⊨ a ⇒ i ⊨ b
  ⇒ ∀ i ∈ I: i ¬ ⊨a ∨ i ¬ ⊨¬ b Semantics of negation
  ⇒ the sequent a, ¬ b, Δ ⊢ Γ is valid.
  
  The ⊤-Axiom and ⊥-Axiom are valid as a corollary: replace a by ⊤_A for ⊤-Axiom, and b by ⊥_A for ⊥-Axiom, along with cp_{⊤_A} and cs_{⊥_A}.
- Let us show that the ⊓-Rule preserves validity. Assume that a ⊓_A b is defined and the sequent a ⊓_A b, Δ ⊢ Γ is valid, then for all i ∈ I
  - either ∃ X ∈ Γ: i ⊨ X ⇒ the sequent a, b, Δ ⊢ Γ is valid
  - or ∃ L ∈ Δ: i ¬ ⊨L ⇒ the sequent a, b, Δ ⊢ Γ is valid
  - or i ¬ ⊨a ⊓_A b ⇒ i ∉ M(a ⊓_A b) ⇒ i ∉ M_A(a ⊓_A b)
    ⇒ i ∉ M_A(a) ∩ M_A(b) (cp_{⊓_A})
    ⇒ i ∉ M_A(a) ⇒ i ∉ M(a) ⇒ i ¬ ⊨a
    ⇒ the sequent a, b, Δ ⊢ Γ is valid.
- Let us show that the ⊔-Rule preserves validity. Assume the sequent ¬(a ⊔_A b), Δ ⊢ Γ is valid, then for all i ∈ I
  - either ∃ X ∈ Γ: i ⊨ X ⇒ the sequent ¬ a, ¬ b, Δ ⊢ Γ is valid
  - or ∃ L ∈ Δ: i ¬ ⊨L ⇒ the sequent ¬ a, ¬ b, Δ ⊢ Γ is valid
  - or ∃ c ∈ a ⊔_A b:i ¬ ⊨¬ c
    ⇒ ∃ c ∈ a ⊔_A b: i ⊨ c
    ⇒ ∃ c ∈ a ⊔_A b: i ∈ M(c)
    ⇒ ∃ c ∈ a ⊔_A b: i ∈ M_A(c)
    ⇒ i ∈ ∪_{c ∈ a ⊔_A b}M_A(c)
    ⇒ i ∈ M_A(a) ∪ M_A(b) (cs_{⊔_A})
    ⇒ i ¬ ⊨¬ a i ¬ ⊨¬ b
    ⇒ ¬ a, ¬ b, Δ ⊢ Γ is valid.
- It is easy to recognize that the inference rules ¬ ¬-Rule, β-Rule, α-Rule and literal-Rule also preserve validity. As a consequence, every provable sequent is valid.
  
  Now for any f,g ∈ AS, if f ⊑ g then ⊢ ¬ f g is a provable sequent
  ⇒ this sequent is valid
  ⇒ ∩_{δ ∈ ∅}M(δ) ⊆ ∪_{γ ∈ {¬ f g}}M(γ) ⇒ M(¬ f g) = I
  ⇒ (I \ M(f)) ∪ M(g) = I ⇒ M(f) ⊆ M(g).
  
  This proves cs_⊑.
■
cp_⊑(f,g) ⇐ cs_{⊓_A} ∧ cp_{⊔_A} ∧

∀ t ∈ Trees(⊢ ¬ f ∨ g):
open(t) ⇒ ∃ A,B ⊢ ∈ t: open_A(A,B) ∧ reduced_A(A,B)
Proof:
- We first prove that the backward-chaining interpretation of the above inference system terminates for all root sequent. For this proof we need a total ordering of sequents. Every formula being either a literal L, a double negation ¬ ¬ X, a conjunction α or a disjunction β, one defines an integral measure m for every formula in AS_prop(A) as follows: m(α) = 1 + m(α₁) + m(α₂), m(¬ ¬ X) = 1 + m(X), m(β) = 1 + m(β₁) + m(β₂), and m(L) = 1.
  
  This measure is extended to sequences of propositions Γ, to sequences of literals Δ, and to full sequents Δ ⊢ Γ as follows: m(Γ) = Σ_{X ∈ Γ} m(X), m(Δ) = Σ_{L ∈ Δ} m(L), m(Δ ⊢ Γ) = (m(Γ),m(Δ)).
  
  Finally, sequents are totally ordered according to a lexicographic ordering < on N². We observe that for every deduction rule Seq₁/Seq₂, m(Seq₁) < m(Seq₂) holds. So, every proof tree is finite. In other words, the backward-chaining procedure always terminates.
- Now, one proves that ⊓-Rule preserves non-validity. Let us assume that a ⊓_A b, Δ ⊢ Γ is not valid.
  Then ∃ i ∈ I: (i ⊨ a ⊓_A b and ∀ L ∈ Δ: i ⊨ L and ∀ X ∈ Γ: i ¬ ⊨X)
  ⇒ ∃ i ∈ I: (i ⊨ a and i ⊨ b and ∀ L ∈ Δ: i ⊨ L and ∀ X ∈ Γ: i ¬ ⊨X cs_{⊓_A}
  ⇒ the sequent a, b, Δ ⊢ Γ is not valid.
- Now, one proves that ⊔-Rule preserves non-validity. Let us assume that ¬(a ⊔_A b), Δ ⊢ Γ is not valid.
  Then ∃ i ∈ I: (∀ c ∈ a ⊔_A b: i ⊨ ¬ c, ∀ L ∈ Δ: i ⊨ L, ∀ X ∈ Γ: i ¬ ⊨X)
  ⇒ ∃ i ∈ I: ∀ c ∈ a ⊔_A b: i ¬ ⊨c
  ⇒ ∃ i ∈ I: ¬ ∃c ∈ a ⊔_A b: i ⊨ c
  ⇒ ∃ i ∈ I: i ∉ ∪_{c ∈ a ⊔_A b}M(c)
  ⇒ ∃ i ∈ I: i ∉ M(a) ∪ M(b) (cp_{⊔_A})
  ⇒ ∃ i ∈ I: i ⊨ ¬ a, i ⊨ ¬ b
  ⇒ ¬ a, ¬ b, Δ ⊢ Γ is not valid.
- It is easy to check that ¬ ¬-Rule, α-Rule, β-Rule and literal-Rule also preserve non-validity.
- If f ⊑ g then ∃ t ∈ Trees(⊢ ¬ f ∨ g): ¬ open(t), i.e. t is a proof of ⊢ ¬ f ∨ g
  ⇒ f ⊔ g Definition of ⊑
  ⇒ M(f) ⊆ M(g) cs_⊑
  ⇒ M(f) ⊆ M(g) ⇒ f ⊑ g ⇒ cp_⊑(f,g).
  
  Else f ¬ ⊑g, which implies ∀ t ∈ Trees(⊢ ¬ f ∨ g): open(t)
  ⇒ ∃ A,B ⊢ ∈ t: open_A(A,B) ∧ reduced_A(A,B) from hypotheses
  ⇒ ∃ A,B ⊢ ∈ t: ∩_{a ∈ A}M_A(a) ¬ ⊆∪_{b ∈ B}M_A(b) Definition of reduced
  ⇒ ∃ A,B ⊢ ∈ t: ∩_{a ∈ A}M(a) ∩ ∩_{b ∈ B}M(¬ b) ¬ ⊆∪_{x ∈ ∅}M(x)
  ⇒ there is a non-valid sequent A,B ⊢ in t Definition 9
  ⇒ the sequent ⊢ ¬ f ∨ g is non-valid because all rules preserves the non-validity (see above)
  ⇒ M(f) ¬ ⊆M(g).
  Hence cp_⊑ (the absence of proof entails the non-validity). ■
cp_⊑⇐ cs_{⊓_A} cp_{⊔_A} reduced_A

Proof: To be done (should be easy from previous and next proofs).
cp'_⊑⇐ cs_{⊓_A} cp_{⊔_A} reduced'_A

Proof: Let f ∈ TELL, g ∈ ASK and t ∈ Trees(¬ f g).

From the inference rules, it follows that forall A,B⊢ ∈ t, A contains only positive atoms of f and negative atoms of g. Reciprocally, B contains only negative atoms of A and positive atoms of g. Hence B is included in ASK_A, and A is included in TELL_A ∪ ASK_A. Moreover, from the definitions of syntax and inference rules, we also have that A always contains an atom in TELL_A. In summary
∀ A,B⊢ ∈ t: (∃ a ∈ A: a = ⊥_A a ∈ TELL_A) (∀ a ∈ A: a ∈ TELL_A ∪ ASK_A ∪ {⊥_A}) (∀ b ∈ B: b ∈ ASK_A)
⇒ ∀ A,B⊢ ∈ t: reduced_A(A,B) (reduced'_A)
⇒ open(t) ⇒ ∃ A,B⊢ ∈ t: open_A(A,B) reduced_A(A,B)
⇒ ∀ t ∈ Trees(⊢ ¬ f g): open(t) ⇒ ∃ A,B⊢ ∈ t: open_A(A,B) reduced_A(A,B)
⇒ cp(f,g). (cs_{⊓_A}, cp_{⊔_A}) ■
def_⊓∧ cs_⊓∧ cp_⊓
def_⊔∧ cs_⊔∧ cp_⊔
def_⊤∧ cp_⊤
def_⊥∧ cs_⊥
reduced(F,G) ⇐ ∀ f ∈ F, g ∈ G: cp_⊑(f,g)
reduced ⇐ cp_⊑
reduced' ⇐ cp'_⊑

Proof: Assume we have F ¬ ⊑^* G, closed_⊓(F), closed_⊔(G).
Then neither conjunction on F, nor disjunction on G can be applied. As these operations are totally defined in Prop, we have F = {f}, and G = {g}.
Then we also have f ¬ ⊑g Definition of ⊑^*
⇒ M(f) ¬ ⊆M(g) if cp_⊑(f,g)
⇒ ∩_{f ∈ F}M(f) ¬ ⊆∪_{g ∈
G}M(g). ■