Appendix E Adaptors

The Adaptors help to make a logic satisfy some properties. They are usually inserted lately in the process of designing a logic, after the syntax and semantics structures have been stabilized. So, they do not usually change a lot the syntax, but may change the semantics in a significant way (while preserving the existing structure).

E.1 Set/1

This functor extends the interpretation domain of a logic to its powerset. This has the side effect of replacing the need for the property reduced by the weaker property reduced.right. A common use example is between the functor Prop and a concrete domain or a logic of values.

E.1.1 Parameters

E ∈ L:: a logic of elements.

E.1.2 Syntax

AS = AS_E
TELL =_def TELL_E
ASK =_def ASK_E

E.1.3 Semantics

domain:: I = 2^I_E \ {∅}.
satisfaction:: i ⊨ f =_def ∃ i_E ∈ i: i ⊨_E f.

E.1.4 Operations

subsumption:: f ⊑ g =_def f ⊑_E g,
tautology:: ⊤ =_def ⊤_E,
contradiction:: ⊥ =_def ⊥_E,
disjunction:: f ⊔ g =_def f ⊔_E g.

E.1.5 Properties

df ⇐ df_E
st(f) ⇐ st_E(f)
st ⇐ st_E
st' ⇐ st'_E
Proof: st_E(f) ⇒ M_E(f) ≠ ∅
⇒ ∃ i_E ∈ I_E: i_E ⊨_E f
⇒ ∃ i = {i_E} ∈ I: i ⊨ f
⇒ M(f) ≠ ∅ ⇒ st(f). ■
cs_⊑⇐ cs_{⊑_E}
Proof: f ⊑ g ⇒ f ⊑_E g
⇒ M_E(f) ⊆ M_E(g) (cs_{⊑_E})
⇒ ∀ i_E: i_E ⊨_E f ⇒ i_E ⊨_E g
⇒ ∀ i ∈ I: (∃ i_E ∈ i: i_E ⊨_E f) ⇒ (∃ i_E ∈ i: i_E ⊨_E g)
⇒ ∀ i ∈ I: i ⊨ f ⇒ i ⊨ g
⇒ M(f) ⊆ M(g). ■
cp_⊑⇐ cp_{⊑_E}
Proof: M(f) ⊆ M(g) ⇒ ∀ i ∈ I: i ⊨ f ⇒ i ⊨ g
⇒ ∀ i ∈ I: (∃ i_E ∈ i: i_E ⊨_E f) ⇒ (∃ i_E ∈ I: i_E ⊨_E g)
⇒ ∀ {i_E} ∈ I: i_E ⊨_E f ⇒ i_E ⊨_E g
⇒ M_E(f) ⊆ M_E(g) ⇒ f ⊑_E g (cp_{⊑_E})
⇒ f ⊑ g. ■
cp_⊤⇐ cp_{⊤_E}
Proof: M_E(⊤_E) = I_E (cp_{⊤_E})
⇒ ∀ i_E ∈ I_E: i_E ⊨_E ⊤_E
⇒ ∀ i ∈ I: ∃ i_E ∈ i: i_E ⊨_E ⊤_E
⇒ ∀ i ∈ I: i ⊨ ⊤_E
⇒ M(⊤) = M(⊤_E) = I. ■
cs_⊥⇐ cs_{⊥_E}
Proof: M_E(⊥_E) = ∅ (cp_{⊥_E})
⇒ ∀ i_E ∈ I_E: i_E ¬ ⊨_E ⊥_E
⇒ ∀ i ∈ I: ∀ i_E ∈ i: i_E ¬ ⊨_E ⊥_E
⇒ ∀ i ∈ I: i ¬ ⊨⊤_E
⇒ M(⊥) = M(⊥_E) = ∅. ■
cs_⊓
cp_⊓
cs_⊔⇐ cs_{⊔_E}
Proof: Let f, g ∈ AS
⇒ f,g ∈ AS_E
⇒ ∪_{h ∈ f ⊔_E g}M_E(h) ⊆ M_E(f) ∪ M_E(g) (cs_{⊔_E})
⇒ ∀ i_E ∈ I_E: (∃ h ∈ f ⊔_E g: i_E ⊨_E h) ⇒ i_E ⊨_E f i_E ⊨_E g
⇒ ∀ i ∈ I: (∃ i_E ∈ i, h ∈ f ⊔_E g: i_E ⊨_E h) ⇒ (∃ i_E ∈ i: i_E ⊨_E f i_E ⊨_E g)
⇒ ∀ i ∈ I: (∃ h ∈ f ⊔_E g, i_E ∈ i: i_E ⊨_E h) ⇒ (∃ i_E ∈ i: i_E ⊨_E f) (∃ i_e ∈ i: i_E ⊨_E g)
⇒ ∀ i ∈ I: (∃ h ∈ f ⊔ g: i ⊨ h) ⇒ i ⊨ f i ⊨ g
⇒ ∪_{h ∈ f ⊔ g}M(h) ⊆ M(f) ∪ M(g). ■
cp_⊔⇐ cp_{⊔_E}
Proof: The proof can be derived from the previous proof for cs_⊔ by replacing ⊆ by ⊇, and ⇒ by ⇐. ■
reduced(F,G) ⇐ ∀ f ∈ F: reduced_E({f},G)
reduced ⇐ reduced.right
reduced' ⇐ reduced.right

Proof: ∩_{f ∈ F}M(f) ⊆ ∪_{g ∈ G}M(g) closed_⊔(G)
⇒ closed_{⊔_E}(G)
and ∀ i ∈ I: (∀ f ∈ F: i ⊨ f) ⇒ (∃ g ∈ G: i ⊨ g)
⇒ ∀ i ∈ I: (∀ f ∈ F: ∃ i_E ∈ i: i_E ⊨_E f) ⇒ (∃ g ∈ G: ∃ i_E ∈ i: i_E ⊨_E g)
⇒ ∀ i ∈ I: (∀ f ∈ F: ∃ i_E ∈ i: i_E ∈ M_E(f)) ⇒ (∃ i_E ∈ i: i_E ∈ ∪_{g ∈ G}M_E(g)).

Now suppose that ∀ f ∈ F: M_E(f) ¬ ⊆∪_{g ∈ G}M_E(g)
⇒ ∀ f ∈ F: ∃ i_E: i_E ⊨_E f i_E ∉ ∪_{g ∈ G}M_E(g)
This allows to build an i ∈ I s.t. ∀ f ∈ F: ∃ i_E ∈ i: i_E ⊨_E f i_E ∉ ∪_{g ∈ G}M_E(g), i.e. i contains an i_E for each f ∈ F, and only that.
⇒ (∀ f ∈ F: ∃ i_E ∈ i: i_E ∈ M_E(f)) ¬ (∃ i_E ∈ i: i_E ∈ ∪_{g ∈ G}M_E(g), which contradicts the above implication for all i ∈ I.

Hence ∃ f ∈ F: M_E(f) ⊆ ∪_{g ∈ G}M_E(g)
⇒ ∃ f ∈ F: {f} ⊑_E^* G) (reduced_E({f},G))
So we have one of the following:
- def(⊥_E) f ⊑_E ⊥_E ⇒ def(⊥) f ⊑ ⊥ ⇒ F ⊑^* G)
- ∃ g ∈ G: def(⊤_E) ⊤_E ⊑_E g ⇒ ∃ g ∈ G: def(⊤) ⊤ ⊑ g ⇒ F ⊑^* G
- ∃ g ∈ G: f ⊑_E g ⇒ ∃ g ∈ G: f ⊑ g ⇒ F ⊑^* G
In conclusion we have F ⊑^* G in all cases, which terminates this proof. ■

E.2 Bottom/1

This functor adds a bottom to the language, and make it the result of the conjunction of a TELL-formula and a non-subsuming ASK-formula. This functor is useful to ensure the property reduced', given the properties sg', and cp'_⊑.

E.2.1 Parameters

X ∈ L:: a logic, whose TELL-formulas have a single model.

E.2.2 Syntax

AS =_def AS_X ⊎ {0}.
TELL =_def TELL_X.
ASK =_def ASK_X.

E.2.3 Semantics

domain:: I =_def I_X.
satisfaction:: i ⊨ f =_def i ⊨_X f, for all f ∈ AS_X.

E.2.4 Operations

subsumption:

f ⊑ g =_def

⎧
⎨
⎩

true	if f = 0
f ⊑_X g	if f,g ∈ AS_X
false	otherwise

tautology:

⊤ =_def ⊤_X.

contradiction:

⊥ =_def 0.

conjunction:

f ⊓ g =_def

⎧
⎪
⎨
⎪
⎩

0	if	f = 0
0	if	g = 0
0	if	f ∈ TELL g ∈ ASK f ¬ ⊑g
0	if	g ∈ TELL f ∈ ASK g ¬ ⊑f
f ⊓_X g	if	f,g ∈ AS_X

E.2.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)) (sg'_X)
⇒ Card(M(d)) = 1. ■
cs_⊑⇐ cs_{⊑_X}

Proof: Let f, g ∈ TELL, such that f ⊑ g. Then
- either f = 0: M(f) = ∅ ⇒ M(f) ⊆ M(g),
- or f, g ∈ AS_X, and f ⊑_X g: M_X(f) ⊆ M_X(g) (cs_{⊑_X})
  ⇒ M(f) ⊆ M(g). ■
cp'_⊑⇐ cp'_{⊑_X}

Proof: Let d ∈ TELL, x ∈ ASK, such that M(d) ⊇ M(x).
Then d ∈ TELL_X, x ∈ ASK_X, M_X(d) ⊆ M_X(x)
⇒ d ⊑_X x (cp'_{⊑_X})
⇒ d ⊑ x. ■
cp_⊤⇐ cp_{⊤_X}

Proof: M(⊤) = M(⊤_X) = M_X(⊤_X) = I_X (cp_{⊤_X}) = I. ■
cs_⊥

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

Proof: Let f,g ∈ AS, s.t. M(f) ∩ M(g) ≠ ∅. Then f ≠ 0, and g ≠ 0, because M(0) = ∅. So, f,g ∈ AS_X, and M_X(f) ∩ M_X(g) ≠ ∅
⇒ def(f ⊓_X g) (defst_{⊓_X})
⇒ def(f ⊓ g). ■
cs_⊓⇐ cs_{⊓_X}

Proof: Let f,g ∈ AS s.t. f ⊓ g is defined:
- f = 0: M(0) = ∅,
- g = 0: idem,
- f ∈ TELL, g ∈ ASK, f ¬ ⊑g: idem,
- f ∈ ASK, g ∈ TELL, g ¬ ⊑f: idem,
- f,g ∈ AS_X: M_X(f ⊓_X g) ⊆ M_X(f) ∩ M_X(g) (cs_{⊓_X})
  ⇒ M(f ⊓_X g) ⊆ M(f) ∩ M(g). ■
cp_⊓⇐ cp_{⊓_X} sg'_X cp'_{⊑_X}

Proof: Let f,g ∈ AS s.t. f ⊓ g is defined:
- f = 0: M(f) = M(0) = ∅ ⇒ M(f) ∩ M(g) = ∅,
- g = 0: idem,
- f ∈ TELL, g ∈ ASK, f ¬ ⊑g: f ∈ TELL_X, g ∈ ASK_X, f ¬ ⊑_X g
  ⇒ M_X(f) ¬ ⊆M_X(g) (cp'_{⊑_X})
  ⇒ M_X(f) ∩ M_X(g) = ∅ (sg'_X)
  ⇒ M(f) ∩ M(g) = ∅,
- f ∈ ASK, g ∈ TELL, g ¬ ⊑f: idem,
- f,g ∈ AS_X: M_X(f ⊓_X g) ⊇ M_X(f) ∩ M_X(g) (cp_{⊓_X})
  ⇒ M(f ⊓_X g) ⊇ M(f) ∩ M(g). ■
reduced' ⇐ df_X sg'_X cs_{⊑_X} cp'_{⊑_X}

Proof: Let F, G ⊆ AS, s.t. ∩_{f ∈ F} M(f) ⊆ ∪_{g ∈ G}M(g), F ⊆ TELL ∪ ASK ∪ {⊥}, F ∩ (TELL ∪ {⊥}) ≠ ∅, closed_⊓(F), and G ⊆ ASK.
- either ⊥ = 0 ∈ F: ∃ f ∈ F: f ⊑ ⊥ (because 0 ⊑ 0)
  ⇒ F ⊑^* G,
- or F ⊆ TELL ∪ ASK = TELL_X ∪ ASK_X = ASK_X, ∃ d ∈ F: d ∈ TELL: (df_X)
  ⇒ ∀ f ∈ F: d ⊑_X f d ¬ ⊑_X f
  ⇒ ∀ f ∈ F: d ⊑ f (d ∈ TELL_X f ∈ ASK_X d ¬ ⊑_X f)
  ⇒ ∀ f ∈ F: d ⊑ f def(d ⊓ f)
  ⇒ ∀ f ∈ F: d ⊑ f (closed_⊓(F))
  ⇒ ∀ f ∈ F: M(d) ⊆ M(f) (cs_{⊑_X})
  ⇒ ∩_{f ∈ F}M(f) = M(d) = M_X(d) = {i_d}. (sg'_X)
  Now, ∩_{f ∈ F} M(f) ⊆ ∪_{g ∈ G}M(g)
  ⇒ i_d ∈ ∪_{g ∈ G}M(g)
  ⇒ ∃ g ∈ G: g ∈ ASK_X, i_d ∈ M_X(g)
  ⇒ ∃ d ∈ F, g ∈ G: d ∈ TELL_X, g ∈ ASK_X, M_X(d) ⊆ M_X(g)
  ⇒ ∃ d ∈ F, g ∈ G: d ⊑_X g (cp'_{⊑_X})
  ⇒ ∃ d ∈ F, g ∈ G: d ⊑ g
  ⇒ F ⊑^* G. ■

E.3 Single/1

This functor ensures that the property sg' is satisfied. The property df is required on the argument logic in order to satisfy the partial completeness cp'_⊑. This functor is based on the epistemic closure [Fer06], which is itself derived from the logic AIK (All I Know [Lev90]).

E.3.1 Parameters

X ∈ L:: a logic.

E.3.2 Syntax

AS	→	AS_X ∣ [AS_X]
TELL	→	[TELL_X]
ASK	→	ASK_X ∣ [TELL_X]

The square brackets denote the modal operator O that is specific to AIK. The usual modal operator K implicitly applies in other cases.

E.3.3 Semantics

domain:

I =_def 2^I_X.

satisfaction:

i ⊨ f	=_def	i ⊆ M_X(f)	,	M(f)	=_def	2^M_X(f)
i ⊨ [f]	=_def	i = M_X(f)	,	M([f])	=_def	{M_X(f)}

E.3.4 Operations

subsumption:

⊑	g	[g]
f	f ⊑_X g	false
[f]	f ⊑_X g	f ≡_X g

tautology:

⊤ =_def ⊤_X.

E.3.5 Properties

df
st'

Proof: Trivial from the definition of semantics. ■
sg'

Proof: Trivial from the definition of semantics. ■
cs_⊑⇐ cs_{⊑_X}

Proof: Let f,g ∈ AS, s.t. f ⊑ g. Then
- either f,g ∈ AS_X: f ⊑_X g
  ⇒ M_X(f) ⊆ M_X(g) (cs_{⊑_X})
  ⇒ 2^M_X(f) ⊆ 2^M_X(g) ⇒ M(f) ⊆ M(g),
- or f = [f'] ∈ [AS_X], g ∈ AS_X: f' ⊑_X g
  ⇒ M_X(f') ⊆ M_X(g) (cs_{⊑_X})
  ⇒ {M_X(f')} ⊆ 2^M_X(g) ⇒ M(f) ⊆ M(g),
- or f = [f'], g = [g'] ∈ [AS_X]: f' ≡_X g' ⇒ f' ⊑_X g' g' ⊑ f'
  ⇒ M_X(f') ⊆ M(g') M_X(g') ⊆ M(f') (cs_{⊑_X})
  ⇒ M_X(f') = M_X(g') ⇒ M(f) = M(g). ■
cp'_⊑⇐ df_X cp'_{⊑_X}

Proof: Let d = [d'] ∈ TELL, d' ∈ TELL_X, x ∈ ASK, s.t. M(d) ⊆ M(f). There are 2 cases:
- either x ∈ ASK_X: {M_X(d')} ⊆ 2^M_X(x)
  ⇒ M_X(d') ⊆ M_X(x) ⇒ d' ⊑_X x (cp'_{⊑_X})
  ⇒ d ⊑ x,
- or x = [x'] ∈ [TELL_X], x' ∈ TELL_X: {M_X(d')} ⊆ {M_X(x')}
  ⇒ M_X(d') ⊆ M_X(x') M_X(x') ⊆ M_X(d')
  ⇒ d' ⊑_X x' x' ⊑_X d' (df_X, cp'_{⊑_X})
  ⇒ d' ≡_X x' ⇒ d ⊑ x. ■
cp_⊤⇐ cp_{⊤_X}

Proof: M(⊤) = M(⊤_X) = 2^M_X(⊤_X) = 2^I_X (cp_{⊤_X}) = I. ■

E.4 Id/1

This functor ensures that the property df is satisfied. This is done by adding an identifier in descriptors, and in interpretations. As every identifier maps to only one TELL-sub-formula, it becomes possible to have a complete entailment between TELL-formulas, and so to include them in the set of ASK-formulas.

E.4.1 Parameters

X ∈ L:: a logic.

E.4.2 Syntax

AS =_def AS_X ∪ (N × AS_X)
TELL =_def N × TELL_X
ASK =_def ASK_X ∪ (N × TELL_X)
In addition to these definitions, we state the following invariant:

∀ (n,f), (m,g) ∈ AS: n = m ⇒ f = g.

E.4.3 Semantics

domain:

I =_def N × I_X.

satisfaction:

(m,i) ⊨ f	=_def	i ⊨_X f	,	M(f)	=_def	N × M_X(f)
(m,i) ⊨ (n,f)	=_def	m=n i ⊨_X f	,	M((n,f))	=_def	{n} × M_X(f)

E.4.4 Operations

subsumption:

⊑	g	(m,g)
f	f ⊑_X g	false
(n,f)	f ⊑_X g	n = m

tautology:

⊤ =_def ⊤_X.

contradiction:

⊥ =_def ⊥_X.

E.4.5 Properties

df
st ⇐ st_X
st' ⇐ st'_X
sg' ⇐ sg'_X

Proof: Let (n,f) ∈ TELL.
M((n,d)) = {n} × M_X(d)
⇒ Card(M((n,d)) = Card(M_X(d)) = 1. (d ∈ TELL_X, sg'_X) ■
cs_⊑⇐ cs_{⊑_X}

Proof: Let f,g ∈ AS, s.t. f ⊑ g. Then
- either f,g ∈ AS_X: f ⊑_X g
  ⇒ M_X(f) ⊆ M_X(g) (cs_{⊑_X})
  ⇒ N × M_X(f) ⊆ N × M_X(g) ⇒ M(f) ⊆ M(g),
- or f = (n,f') ∈ N × AS_X, g ∈ AS_X: f' ⊑_X g
  ⇒ M_X(f') ⊆ M_X(g) (cs_{⊑_X})
  ⇒ {n} × M_X(f') ⊆ N × M_X(g) ⇒ M(f) ⊆ M(g),
- or f = (n,f'), g = (m,g') ∈ N × AS_X: n=m ⇒ f' = g' (invariant)
  ⇒ M_X(f') = M_X(g') ⇒ {n} × M_X(f') = {m} × M_X(g') (n = m)
  ⇒ M(f) = M(g). ■
cp'_⊑⇐ cp'_{⊑_X}

Proof: Let d = (n,d') ∈ TELL, d' ∈ TELL_X, x ∈ ASK, s.t. M(d) ⊆ M(x). There are 2 cases:
- either x ∈ ASK_X: {n} × M_X(d') ⊆ N × M_X(x)
  ⇒ M_X(d') ⊆ M_X(x) ⇒ d' ⊑_X x (cp'_{⊑_X})
  ⇒ d ⊑ x,
- or x = (m,x') ∈ N × TELL_X, x' ∈ TELL_X: {n} × M_X(d') ⊆ {m} × M_X(x')
  ⇒ n = m M_X(d') ⊆ M_X(x')
  ⇒ d ⊑ x. ■
cp_⊤⇐ cp_{⊤_X}

Proof: M(⊤) = M(⊤_X) = N × M_X(⊤_X) = N × I_X (cp_{⊤_X}) = I. ■
cs_⊥⇐ cs_{⊥_X}

Proof: M(⊥) = M(⊥_X) = N × M_X(⊥_X) = N × ∅ (cs_{⊥_X}) = ∅. ■

E.5 Aik/1 = λ X.Prop(Bottom(Single(X)))

This combinator is commonly applied in logical information systems on the logic of object descriptions and features. This produces a full querying language with boolean connectives matching set operations on sets of answers, i.e., queries are interpreted under the Closed World Assumption.