Appendix B Initiators

The Initiators are 0-ary logic functors. They correspond to symbols, constants, and values in concrete domains. They can also introduce patterns on these values (e.g., in String). They usually satisfy many properties, and so can easily be integrated in various logics.

B.1 Unit/0 = {unit}

Minimal logic with only one interpretation, and only one formula. Useful to make optional some properties in logics. {unit} is an equivalent notation of this functor, where unit can be replaced by any symbol.

B.1.1 Parameters

No parameters.

B.1.2 Syntax

There is a unique formula:
AS =_def {unit}

B.1.3 Semantics

domain:: I =_def {unit}.
satisfaction:: M(unit) =_def {unit}.

B.1.4 Operations

subsumption:: unit ⊑ unit.
tautology:: ⊤ =_def unit.
conjunction:: unit ⊓ unit =_def unit
disjunction:: unit ⊔ unit =_def unit

B.1.5 Properties

df
st
sg
cs_⊑
cp_⊑
cp_⊤
reduced

Proof: Let F,G ∈ AS^*, and suppose F ¬ ⊑^* G
⇒ ∀ f ∈ F, g ∈ G: f ¬ ⊑g ∀ g ∈ G: ⊤ ¬ ⊑g
⇒ (F = ∅ G = ∅) G = ∅ (because ∀ f,g ∈ AS: f ⊑ g)
⇒ ∩_{f ∈ F}M(f) = I ∪_{g ∈ G}M(g) = ∅
⇒ ∩_{f ∈ F}M(f) ¬ ⊆∪_{g ∈ G}M(g). ■

B.2 Atom/0

The logic whose formulas and interpretations are the usual atoms. Each atom is interpreted by itself. It is useful to represent abstract atomic properties (as opposed to concrete properties).

B.2.1 Parameters

No parameters.

B.2.2 Syntax

AS is a set of atoms.

B.2.3 Semantics

domain:: I = AS.
satisfaction:: i ⊨ a =_def i = a.

B.2.4 Operations

subsumption:

a ⊑ b =_def a = b,

conjunction:

a ⊓ b =_def

⎧
⎨
⎩

a	if a = b
undef	otherwise

disjunction:

a ⊓ b =_def

⎧
⎨
⎩

{a}	if a = b
{a,b}	otherwise

B.2.5 Properties

df
st

Proof: For all a ∈ AS, M(a) = {a} ≠ ∅. ■
sg

Proof: For all a ∈ AS, M(a) = {a}. ■
cs_⊑

Proof: a ⊑ b ⇒ a = b ⇒ M(a) = M(b) ⇒ M(a) ⊆ M(b). ■
cp_⊑

Proof: a ¬ ⊑b ⇒ a ≠ b ⇒ a ⊨ a, a ¬ ⊨b ⇒ M(a) ¬ ⊆M(b). ■
defst_⊓

Proof: M(a) ∩ M(b) ≠ ∅
⇒ {a} ∩ {b} ≠ ∅ ⇒ a = b
⇒ def_⊓(a,b). ■
cs_⊓ cp_⊓
cs_⊔ cp_⊔
reduced.right
reduced.bot

Proof: M(a) ⊆ ∪_{b ∈ B}M(b)
⇒ {a} ⊆ B ⇒ a ∈ B
⇒ ∃ b ∈ B: a = b ⇒ ∃ b ∈ B: a ⊑ b
⇒ {a} ⊑^* B. ■

B.3 Int/0

Formulas and models are simple integers. Each integer is interpreted by itself. Interpretations are ordered according to the usual ordering on integers.

B.3.1 Parameters

No parameters.

B.3.2 Syntax

AS =_def Z

B.3.3 Semantics

domain:: I =_def Z
satisfaction:: i ⊨ f =_def i = f

B.3.4 Operations

subsumption:: f ⊑ g =_def f = g
lower ordering:: f ≤ g =_def f ≤ g
upper ordering:: f ⋜ g =_def f ≤ g

B.3.5 Properties

df
st
sg
cs_⊑ cp_⊑
cs_≤ cp_≤

Proof: ≤ is a total ordering, so ≤ is both reflexive and transitive. ■
cs_⋜ cp_⋜

Proof: ≤ is a total ordering, so ⋜ is both reflexive and transitive. ■
reduced.right
reduced.bot

Proof: Let a ∈ AS, B ⊆ AS, s.t. {a} ¬ ⊑^* B.
Then ∀ b ∈ B: a ¬ ⊑b ⇒ ∀ b ∈ B: a ≠ b
⇒ ∀ b ∈ B: a ¬ ⊨b ⇒ a ∉ ∪_{b ∈ B}M(b)
⇒ M(a) ¬ ⊆∪_{b ∈ B}M(b). ■

B.4 Card/0

Formulas expressing cardinals, i.e. “at least” properties. So formulas and interpretations are natural numbers, and both the satisfaction and subsumption relations are the decreasing ordering on natural numbers.

B.4.1 Parameters

No parameters.

B.4.2 Syntax

AS =_def N

B.4.3 Semantics

domain:: I =_def N
satisfaction:: i ⊨ f =_def i ≥ f

B.4.4 Operations

subsumption:: f ⊑ g =_def f ≥ g
top:: ⊤ =_def 0
conjunction:: f ⊓ g =_def max(f,g)
disjunction:: f ⊓ g =_def {min(f,g)}

B.4.5 Properties

df
st

Proof: ∀ f ∈ N: f ≥ f
⇒ ∀ f ∈ N: ∃ i ∈ N: i ≥ f
⇒ ∀ f ∈ AS: ∃ i ∈ I: i ⊨ f
⇒ ∀ f ∈ AS: M(f) ≠ ∅. ■
cs_⊑

Proof: f ⊑ g ⇒ f ≥ g
⇒ ∀ i ∈ N: i ≥ f ⇒ i ≥ g
⇒ ∀ i ∈ I: i ⊨ f ⇒ i ⊨ g
⇒ M(f) ⊆ M(g). ■
cp_⊑

Proof: M(f) ⊆ M(g) ⇒ ∀ i ∈ I: i ⊨ f ⇒ i ⊨ g
⇒ ∀ i ∈ N: i ≥ f ⇒ i ≥ g
⇒ f ≥ g ⇒ f ⊑ g. ■
cp_⊤

Proof: M(⊤) = M(0) = {i ∈ N ∣ i ≥ 0} = N = I. ■
cs_⊓ cp_⊓

Proof: M(f ⊓ g) = M(max(f,g))
= {i ∈ N ∣ i ≥ max(f,g)}
= {i ∈ N ∣ i ≥ f i ≥ g}
= {i ∈ N ∣ i ≥ f} ∩ {i ∈ N ∣ i ≥ g}
= M(f) ∩ M(g). ■
cs_⊓ cp_⊓

Proof: M(f ⊔ g) = ∪_{h ∈ f ⊔ g}M(h) = M(max(f,g))
= {i ∈ N ∣ i ≥ min(f,g)}
= {i ∈ N ∣ i ≥ f i ≥ g}
= {i ∈ N ∣ i ≥ f} ∪ {i ∈ N ∣ i ≥ g}
= M(f) ∪ M(g). ■
reduced

Proof: Let A,B ⊆ AS, s.t. A ¬ ⊑^* B, closed_⊓(A), closed_⊔(B). Then we have
1. ∀ a₁ ≠ a₂ ∈ A: ¬def(a₁ ⊓ a₂): hence, A = {a} is a singleton because ⊓ is totally defined.
2. ∀ b₁ ≠ b₂ ∈ B: b₁ ⊔ b₂ ⊆ B:
  ⇒ ∀ b₁ ≠ b₂ ∈ B: min(b₁,b₂) ∈ B
  ⇒ min(B) ∈ B.
  Now, for all b ∈ B, b ≥ min(B) ⇒ b ⊑ min(B) ⇒ M(b) ⊆ M(min(B)) (because cs_⊑). Hence ∪_{b ∈ B}M(b) = M(min(B)).
3. a ¬ ⊑min(B) ⇒ M(a) ¬ ⊆M(min(B)) (cp_⊑)
  ⇒ ∩_{a ∈ A}M(a) ¬ ⊆∪_{b ∈ B}M(b). ■

B.5 String/0

Formulas are strings and substrings over an arbitrary alphabet plus 2 special characters for representing the beginning and the end of a string. Interpretations are closed strings, i.e., strings having a beginning and an end. Both satisfaction and subsumption relations are based on exact string matching.

B.5.1 Parameters

Σ:: an alphabet.

B.5.2 Syntax

AS =_def <?Σ^*>?: formulas are strings and substrings

B.5.3 Semantics

domain:: I =_def <Σ^*>: interpretations are also strings, but closed with a beginning and an end
satisfaction:: i ⊨ f =_def ∃ u,v ∈ AS: i = u.f.v: f is a substring of i

B.5.4 Operations

subsumption:: f ⊑ g =_def ∃ u,v ∈ AS: f = u.g.v
tautology:: ⊤ =_def є (the empty string)

B.5.5 Properties

df
st

Proof: For every f ∈ AS, there exists a w ∈ Σ^* s.t. f ∈ {<w>, <w, w>, w}. Then <w> ∈ I, and <w> ⊨ f in all cases. ■
cs_⊑

Proof: f ⊑ g ⇒ ∃ u,v ∈ AS: f = u.g.v
⇒ ∀ i ∈ I: i ⊨ f ⇒ ∃ u',v' ∈ AS: i = u'.f.v' = u'.u.g.v.v'
⇒ ∀ i ∈ I: i ⊨ f ⇒ i ⊨ g
⇒ M(f) ⊆ M(g). ■
cp_⊑

Proof: f ¬ ⊑g ⇒ ¬ ∃u,v ∈ AS: f = u.g.v. Then
- either f ∈ <Σ^*>: f ∈ I
  ⇒ f ⊨ f f ¬ ⊨g
  ⇒ M(f) ¬ ⊆M(g),
- or f ∈ Σ^*: <f> ∈ I, and <f> ⊨ f.
  Now suppose <f> ⊨ g
  ⇒ ∃ u',v' ∈ AS: <f> = u'.g.v'
  ⇒ ∃ u'',v'' ∈ AS: f = u''.g.v''
  ⇒ f ⊑ g —→ contadiction.
  Hence <f> ¬ ⊨g, and M(f) ¬ ⊆M(g).
- or f ∈ <Σ^*: similar proof,
- or f ∈ Σ^*>: similar proof. ■
cp_⊤

Proof: i ∈ I ⇒ i = i.є.є ⇒ i ⊨ є
⇒ M(є) = I. ■
cs_⊓ cp_⊓
reduced.right
reduced.bot

Proof: Let a ∈ AS, B ⊆ AS, s.t. {a} ¬ ⊑^* B.
Then ∀ b ∈ B: a ¬ ⊑b. Now we have seen in the proof of cp_⊑ that
f ¬ ⊑g ⇒ ∃ i_f ∈ I: i ⊨ f i ¬ ⊨g,
where the model i_f depends solely on f (it is the “closure” of f).
So ∃ i_a ∈ I: ∀ b ∈ B: i_a ⊨ a i_a ¬ ⊨b
⇒ ∃ i_a ∈ M(a): ∀ b ∈ B: i_a ∉ M(b)
⇒ M(a) ¬ ⊆∪_{b ∈ B}M(b). ■