How to Kiss an Angel

Christoph Benzmüller FR Informatik, Saarland Univ.

chris@ags.uni-sb.de

SEKI Working-Paper SWP–2006–02

SEKI Working-Paperhttp://www.dfki.de/seki ISSN 1860-5931

SEKI is published by the following institutions:

German Research Center for Artificial Intelligence (DFKI GmbH), Germany

• Robert Hooke Str. 5, D–28359 Bremen
• Trippstadter Str. 122, D–67663 Kaiserslautern
• Campus D 3 2, D–66123 Saarbrücken

Jacobs University Bremen, School of Engineering & Science, Campus Ring 1, D–28759 Bremen, Germany

Universität des Saarlandes, FR 6.2 Informatik, Campus, D–66123 Saarbrücken, Germany

SEKI Editor:

Claus-Peter Wirth

E-mail: wirth@logic.at
WWW: http://www.ags.uni-sb.de/~cp

Please send surface mail exclusively to:

DFKI Bremen GmbH Safe and Secure Cognitive Systems Cartesium Enrique Schmidt Str. 5 D–28359 Bremen Germany

This SEKI Working-Paper was internally reviewed by:

Erica Melis FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: melis@activemath.org
WWW: http://www.activemath.org/~melis

How to Kiss an Angel

Christoph Benzmüller FR Informatik, Saarland Univ.

                  chris@ags.uni-sb.de

March 22, 2012

Abstract

We solve the problem of kissing an angel effectively and more efficiently than voodoo man. Some reading of Immanuël Kant, however, is required as a precondition.

Keywords: German Idealism, Dyslexia, Kissing, Angels, Angles, Kant, MSC 03D20, MSC 68Q42, MSC 16S15

1 Introduction 2 Terms and Substitutions

For being concrete, we will work with a simple-typed higher-order framework here.

There is a finite number of sorts or base types, including the Boolean sort bool (denoted with o by other authors). Types are inductively defined to be either a base type or a function type α → β, for two types α and β. The operator “ → ” associates to the right.

There is a finite number of constants, including true, false : bool, ¬ : bool → bool, ⇒, ∨, ∧ : bool → bool → bool, ∀_{α}, ∃_{α} : (α → bool) → bool, and ε_{α,n} : (α → bool) → α, for each type α and for each natural number n. Each constant must have a unique type.

There are three disjoint sets of bound atoms 𝔹, (free) atoms 𝔸, and (free) variables 𝕍. Each of their elements has a unique type, and each of the three sets has infinitely many elements of each type. We define:

\begin{aligned}𝕍𝔸 & := & 𝕍 ⊎ 𝔸 \\ 𝕍𝔸𝔹 & := & 𝕍 ⊎ 𝔸 ⊎ 𝔹 \end{aligned}

The classification as a free variable or as a free or bound atom will be indicated by adjoining a “𝕍”, an “𝔸”, or a “𝔹”, respectively, as a label to the upper right of the meta-variable for the symbol. If a meta-variable stands for a symbol of the union of some of these sets, we will indicate this by listing all possible sets; e.g. “x^{𝕍𝔸}” is a meta-variable for a symbol that may be either a free variable or a free atom.

Meta-variables with disjoint labels always denote different symbols; e.g. “x^{𝕍}” and “x^{𝔸}” will always denote different symbols; whereas “x^{𝕍𝔸}” may denote the same symbol as “x^{𝔸}”. In concrete examples, we will implicitly assume that different meta-variables denote different symbols; whereas in formal discussions, “x^{𝔸}” and “y^{𝔸}” may denote the same symbol.

Definition 2.1 (Terms (T ) and [Finite] Atom Substitutions) Each term of the set of terms T will have a unique sort. A term is closed if it does not contain unbound occurrences of bound atoms. As finite atom substitutions may be parts of our terms, we have to define both notions in a mutual induction.

• Constants, (free) atoms, and bound atoms are terms of their given types.

• If t_{1} : α → β and t_{2} : α are terms, then the application t_{1}t_{2} : β is a term as well. Application associates to the left.

• If t : β is a term and y^{𝔹} : α is a bound atom, then the abstraction λy^{𝔹}. t : α → β is a term as well.

• If z^{𝕍} : α is a variable and θ is a finite atom substitution,

then the pending (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) : α is a term. We will use z^{𝕍} as a shorthand for (\begin{matrix}z^{𝕍} \\ 𝔸 & ↿ & id \end{matrix}).

• An atom substitution θ is a total function from atoms to closed terms respecting types, i.e., for every x^{𝔸} : α, we have θ(x^{𝔸}) : α. For an atom substitution θ we define its non-trivial domain as NT (θ) := { x^{𝔸} ∈ 𝔸 | θ(x^{𝔸}) ≠ x^{𝔸} }. A finite atom substitution θ is an atom substitution where NT (θ) is finite.

Definition 2.2 (Atom Permutation) An atom permutation π is an atom substitution that is a permutation in the sense that π is a bijection of 𝔸 onto 𝔸.

Definition 2.3 ([Finite] Variable Substitutions) A variable substitution σ is a total function from variables to closed terms respecting types, i.e., for every z^{𝕍} : α, we have σ(z^{𝕍}) : α. For a variable substitution θ we define its non-trivial domain as

NT (σ) := \{ z^{𝕍} ∈ 𝕍 σ(z^{𝕍}) ≠ (\begin{matrix}z^{𝕍} \\ 𝔸 & ↿ & id \end{matrix}) \}.

A finite variable substitution θ is a variable substitution where NT (σ) is finite.

Definition 2.4 (Extension to Terms) We extend any finite atom substitution θ and any variable substitution σ to functions θ^{T} and σ^{T} from terms to terms as given in the following box. Note that we write tθ as a shorthand for θ^{T}(t), and also tσ as a shorthand for σ^{T}(t), which are recursively defined according to the following table:

t  tθ  tσ
f (a constant)  f  f
y^{𝔹} (a bound atom)  y^{𝔹}  y^{𝔹}
x^{𝔸} (an atom)  θ(x^{𝔸})  x^{𝔸}
t_{1}t_{2} (an application)  (t_{1}θ)(t_{2}θ)  (t_{1}σ)(t_{2}σ)
λy^{𝔹}. t′ (an abstraction) λy^{𝔹}. (t′θ)  λy^{𝔹}. (t′σ)
(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) (a pending)  (\begin{matrix}z^{𝕍} \\ θ′ ∘ θ^{T} \end{matrix} ) (σ(z^{𝕍}))(θ′ ∘ σ^{T})

Note that θ′ ∘θ^{T} may be an infinite atom substitution for a finite atom substitution θ′ and an infinite atom substitution θ; so we have to require θ to be finite in Definition 2.4. This finiteness requirement also applies to the atom substitution θ′ ∘ σ^{T} , where, however, we do not have to require σ to be a finite variable substitution because of NT (θ′ ∘ σ^{T}) ⊆ NT (θ′). Moreover, note that the term (σ(z^{𝕍}))(θ′ ∘ σ^{T}) in the last field of the table of Definition 2.4 denotes (θ ∘ σ^{T})^{T} (σ(z^{𝕍})) and not the (in general different) (θ^{T} ∘ σ^{T})(σ(z^{𝕍})); to see the difference, take θ := _{𝔸}↿id, then θ^{T} ∘σ^{T} = _{T} ↿id∘σ^{T} = σ^{T}, but (θ ∘ σ^{T})^{T} = (_{𝔸}↿id)^{T} = _{T} ↿id. For an atom substitution instead of σ, however, this difference does not exist:

Lemma 2.5 For two finite atom substitutions θ, θ′, we have: (θ′)^{T} ∘ θ^{T} = (θ′ ∘ θ^{T})^{T}.

Proof of Lemma 2.5 It suffices to show (tθ′)θ = t(θ′ ∘ θ^{T}) by structural induction on the term t.

\underline{t = f (a constant):} (fθ′)θ = fθ = f = f(θ′ ∘ θ^{T}).

\underline{t = y^{𝔹} (a bound atom):} (y^{𝔹}θ′)θ = y^{𝔹}θ = y^{𝔹} = y^{𝔹}(θ′ ∘ θ^{T}).

\underline{t = x^{𝔸} (an atom):} (x^{𝔸}θ′)θ = (θ′(x^{𝔸}))θ = θ^{T} (θ′(x^{𝔸})) = (θ′ ∘ θ^{T})(x^{𝔸}) = x^{𝔸}(θ′ ∘ θ^{T}).

\underline{t = t_{1}t_{2} (an application):} ((t_{1}t_{2})θ′)θ = ((t_{1}θ′)(t_{2}θ′))θ = ((t_{1}θ′)θ)((t_{2}θ′)θ) = (t_{1}(θ′ ∘ θ^{T}))(t_{1}(θ′ ∘ θ^{T})) = (t_{1}t_{2})(θ′ ∘ θ^{T}).

\underline{t = λy^{𝔹}. t′ (an abstraction):} ((λy^{𝔹}. t′)θ′)θ = (λy^{𝔹}. (t′θ′))θ = λy^{𝔹}. ((t′θ′)θ) = λy^{𝔹}. (t′(θ′ ∘ θ^{T})) = (λy^{𝔹}. t′)(θ′ ∘ θ^{T}).

\underline{t = (\begin{matrix}z^{𝕍} \\ θ′′ \end{matrix}) (a pending):} By induction hypothesis we have ((θ′′(x^{𝔸}))θ′)θ = (θ′′(x^{𝔸}))(θ′ ∘ θ^{T})

for all x^{𝔸} ∈ NT (θ′′). And for x^{𝔸} ∈ 𝔸\ NT (θ′′), this holds as well

because of θ′′(x^{𝔸}) = x^{𝔸} and the above proof for atoms. This means that, for all x^{𝔸} ∈ 𝔸, we have (θ′′ ∘ (θ′)^{T} ∘ θ^{T})(x^{𝔸}) = (θ′′ ∘ (θ′ ∘ θ^{T})^{T})(x^{𝔸}). Thus, we have:

( (\begin{matrix}z^{𝕍} \\ θ′′ \end{matrix})θ′ )θ = (\begin{matrix}z^{𝕍} \\ θ′′ ∘ (θ′)^{T} \end{matrix} )θ = (\begin{matrix}z^{𝕍} \\ θ′′ ∘ (θ′)^{T} ∘ θ^{T} \end{matrix} ) = (\begin{matrix}z^{𝕍} \\ θ′′ ∘ (θ′ ∘ θ^{T})^{T} \end{matrix} ) = (\begin{matrix}z^{𝕍} \\ θ′′ \end{matrix})(θ′ ∘ θ^{T}).

Q.e.d. (Lemma 2.5)

Lemma 2.6 For a term t, a finite atom substitution θ, and a variable substitution σ, we have:

(tθ)σ = (tσ)(θ ∘ σ^{T}).

Proof of Lemma 2.6 By structural induction on the term t. \underline{t = f (a constant):} (fθ)σ = fσ = f = f(θ ∘ σ^{T}) = (fσ)(θ ∘ σ^{T}). \underline{t = y^{𝔹} (a bound atom):} (y^{𝔹}θ)σ = y^{𝔹}σ = y^{𝔹} = y^{𝔹}(θ ∘ σ^{T}) = (y^{𝔹}σ)(θ ∘ σ^{T}). \underline{t = x^{𝔸} (an atom):} (x^{𝔸}θ)σ = (θ(x^{𝔸}))σ = (θ ∘ σ^{T})(x^{𝔸}) = x^{𝔸}(θ ∘ σ^{T}) = (x^{𝔸}σ)(θ ∘ σ^{T}). \underline{t = t_{1}t_{2} (an application):} ((t_{1}t_{2})θ)σ = ((t_{1}θ)(t_{2}θ))σ = ((t_{1}θ)σ)((t_{2}θ)σ) =

((t_{1}σ)(θ ∘ σ^{T}))((t_{2}σ)(θ ∘ σ^{T})) = ((t_{1}σ)(t_{2}σ))(θ ∘ σ^{T}) =

((t_{1}t_{2})σ)(θ ∘ σ^{T}). \underline{t = λy^{𝔹}. t′ (an abstraction):} ((λy^{𝔹}. t′)θ)σ = (λy^{𝔹}. (t′θ))σ = λy^{𝔹}. ((t′θ)σ) =

λy^{𝔹}. ((t′σ)(θ ∘ σ^{T})) = (λy^{𝔹}. (t′σ))(θ ∘ σ^{T}) =

((λy^{𝔹}. t′)σ)(θ ∘ σ^{T}).

\underline{t = (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) (a pending):} By induction hypothesis we have

((θ′(x^{𝔸}))θ)σ = ((θ′(x^{𝔸}))σ)(θ ∘ σ^{T}) for all x^{𝔸} ∈ NT (θ′). And

for x^{𝔸} ∈ 𝔸\ NT (θ′), this holds as well because of θ′(x^{𝔸}) = x^{𝔸} and the above proof for atoms. This means that, for all x^{𝔸} ∈ 𝔸, we have (θ′ ∘ θ^{T} ∘ σ^{T})(x^{𝔸}) = (θ′ ∘ σ^{T} ∘ (θ ∘ σ^{T})^{T})(x^{𝔸}); i.e. θ′ ∘ θ^{T} ∘ σ^{T} = θ′ ∘ σ^{T} ∘ (θ ∘ σ^{T})^{T}; i.e. (θ′ ∘ θ^{T} ∘ σ^{T})^{T} = ( θ′ ∘ σ^{T} ∘ (θ ∘ σ^{T})^{T} )^{T} = (θ′ ∘ σ^{T})^{T} ∘ (θ ∘ σ^{T})^{T} by Lemma 2.5. Thus, we have:

( (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})θ )σ = (\begin{matrix}z^{𝕍} \\ θ′ ∘ θ^{T} \end{matrix} )σ = (σ(z^{𝕍}))(θ′ ∘ θ^{T} ∘ σ^{T}) = (θ′ ∘ θ^{T} ∘ σ^{T})^{T} (σ(z^{𝕍})) =

((θ′ ∘ σ^{T})^{T} ∘ (θ ∘ σ^{T})^{T})(σ(z^{𝕍})) = ((σ(z^{𝕍}))(θ′ ∘ σ^{T}))(θ ∘ σ^{T}) = ( (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})σ )(θ ∘ σ^{T}).

Q.e.d. (Lemma 2.6)

Lemma 2.7 For a term t, a finite atom permutation π, and a variable substitution σ, we have:

(tπ)σ = (tσ)π.

Proof of Lemma 2.7 According to Lemma 2.6 we have (tπ)σ = (tσ)(π ∘ σ^{T}) = (tσ)π. Q.e.d. (Lemma 2.7)

Definition 2.8 (𝔸(t), 𝕍(t)) The (free) atoms 𝔸(t) of a term t and the (free) variables 𝕍(t) of a term t are recursively defined according to the following table:

t  𝔸(t)  𝕍(t)
T (a set of terms)  ⋃_{t∈T} 𝔸(t)  ⋃_{t∈T} 𝕍(t)
f (a constant)  ∅  ∅
y^{𝔹} (a bound atom)  ∅  ∅
x^{𝔸} (an atom)  {x^{𝔸}}  ∅
t_{1}t_{2} (an application)  ⋃_{i∈{1,2}} 𝔸(t_{i}) ⋃_{i∈{1,2}} 𝕍(t_{i})
λy^{𝔹}. t′ (an abstraction)  𝔸(t′)  𝕍(t′)
(\begin{matrix}z^{𝕍} \\ θ \end{matrix}) (a pending)  ∅  \{ (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) \}

Moreover, we set 𝕍𝔸(t) := 𝔸(t) ⊎ 𝕍(t).

Corollary 2.9

1. 𝔸( ⋃_{i∈I} T_{i} ) = ⋃_{i∈I} 𝔸(T_{i}).

2. 𝕍( ⋃_{i∈I} T_{i} ) = ⋃_{i∈I} 𝕍(T_{i}).

Lemma 2.10 For a term t and a finite atom substitution θ we have:

1. 𝔸(tθ) = 𝔸(⟨𝔸(t)⟩θ).

2. 𝕍(tθ) = ⟨𝕍(t)⟩θ^{T} ∪ 𝕍(⟨𝔸(t)⟩θ).

Proof of Lemma 2.10 By structural induction on t.

\underline{t = f (a constant):} 𝔸(fθ) = 𝔸(f) = ∅ = 𝔸(∅) = 𝔸(⟨∅⟩θ) = 𝔸(⟨𝔸(f)⟩θ).

𝕍(fθ) = 𝕍(f) = ∅ = ∅ ∪ 𝕍(∅) = ⟨∅⟩θ^{T} ∪ 𝕍(⟨∅⟩θ) =

⟨𝕍(f)⟩θ^{T} ∪ 𝕍(⟨𝔸(f)⟩θ).

\underline{t = y^{𝔹} (a bound atom):} 𝔸(y^{𝔹}θ) = 𝔸(y^{𝔹}) = ∅ = 𝔸(∅) = 𝔸(⟨∅⟩θ) = 𝔸(⟨𝔸(y^{𝔹})⟩θ).

𝕍(y^{𝔹}θ) = 𝕍(y^{𝔹}) = ∅ = ∅ ∪ 𝕍(∅) = ⟨∅⟩θ^{T} ∪ 𝕍(⟨∅⟩θ) =

⟨𝕍(y^{𝔹})⟩θ ∪ 𝕍(⟨𝔸(y^{𝔹})⟩θ^{T}).

\underline{t = x^{𝔸} (an atom):} 𝔸(x^{𝔸}θ) = 𝔸(θ(x^{𝔸})) = 𝔸(⟨\{x^{𝔸}\}⟩θ) = 𝔸(⟨𝔸(x^{𝔸})⟩θ).

𝕍(x^{𝔸}θ) = 𝕍(θ(x^{𝔸})) = ∅ ∪ 𝕍(θ(x^{𝔸})) = ⟨∅⟩θ^{T} ∪ 𝕍(⟨{x^{𝔸}}⟩θ) =

⟨𝕍(x^{𝔸})⟩θ^{T} ∪ 𝕍(⟨𝔸(x^{𝔸})⟩θ).

\underline{t = t_{1}t_{2} (an application):} 𝔸((t_{1}t_{2})θ) = 𝔸((t_{1}θ)(t_{2}θ)) = ⋃_{i∈\{1,2\}} 𝔸(t_{i}θ) =

⋃_{i∈{1,2}} 𝔸(⟨𝔸(t_{i})⟩θ) = 𝔸( ⋃_{i∈{1,2}} ⟨𝔸(t_{i})⟩θ ) =

𝔸( ⟨⋃_{i∈{1,2}} 𝔸(t_{i})⟩θ ) = 𝔸(⟨𝔸(t_{1}t_{2})⟩θ). 𝕍((t_{1}t_{2})θ) = 𝕍((t_{1}θ)(t_{2}θ)) = ⋃_{i∈{1,2}} 𝕍(t_{i}θ) = ⋃_{i∈{1,2}} ⟨𝕍(t_{i})⟩θ^{T} ∪ ⋃_{i∈{1,2}} 𝕍(⟨𝔸(t_{i})⟩θ) = ⋃_{i∈{1,2}} ⟨𝕍(t_{i})⟩θ^{T} ∪ 𝕍( ⋃_{i∈{1,2}} ⟨𝔸(t_{i})⟩θ ) = ⟨⋃_{i∈{1,2}} 𝕍(t_{i})⟩θ^{T} ∪ 𝕍( ⟨⋃_{i∈{1,2}} 𝔸(t_{i})⟩θ ) = ⟨𝕍(t_{1}t_{2})⟩θ^{T} ∪ 𝕍(⟨𝔸(t_{1}t_{2})⟩θ).

\underline{t = λy^{𝔹}. t′ (an abstraction):} 𝔸((λy^{𝔹}. t′)θ) = 𝔸(λy^{𝔹}. (t′θ)) = 𝔸(t′θ) = 𝔸(⟨𝔸(t′)⟩θ) =

𝔸(⟨𝔸(λy^{𝔹}. t′)⟩θ).

𝕍((λy^{𝔹}. t′)θ) = 𝕍(λy^{𝔹}. (t′θ)) = 𝕍(t′θ) = ⟨𝕍(t′)⟩θ^{T} ∪ 𝕍(⟨𝔸(t′)⟩θ) = ⟨𝕍(λy^{𝔹}. t′)⟩θ^{T} ∪ 𝕍(⟨𝔸(λy^{𝔹}. t′)⟩θ).

\underline{t = (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) (a pending):} 𝔸( (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})θ ) = 𝔸(\begin{matrix}z^{𝕍} \\ θ′ ∘ θ^{T} \end{matrix} ) = ∅ = 𝔸(∅) = 𝔸(⟨∅⟩θ) =

𝔸( ⟨𝔸(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})⟩θ ).

𝕍( (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})θ ) = 𝕍(\begin{matrix}z^{𝕍} \\ θ′ ∘ θ^{T} \end{matrix} ) = \{ (\begin{matrix}z^{𝕍} \\ θ′ ∘ θ^{T} \end{matrix} ) \} = \{ (\begin{matrix}z^{𝕍} \\ θ′ ∘ θ^{T} \end{matrix} ) \} ∪ ∅ =

\{ (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})θ \} ∪ 𝕍(∅) = ⟨\{ (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) \}⟩θ^{T} ∪ 𝕍(⟨∅⟩θ) = ⟨𝕍(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})⟩θ^{T} ∪ 𝕍( ⟨𝔸(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})⟩θ ).

Q.e.d. (Lemma 2.10)

Lemma 2.11 For a term t and a variable substitution σ we have:

1. 𝔸(tσ) = 𝔸(t) ∪ 𝔸(⟨𝕍(t)⟩σ^{T}).

2. 𝕍(tσ) = 𝕍(⟨𝕍(t)⟩σ^{T}).

Proof of Lemma 2.11 By structural induction on t. \underline{t = f (a constant):} 𝔸(fσ) = 𝔸(f) = 𝔸(f) ∪ ∅ = 𝔸(f) ∪ 𝔸(∅) = 𝔸(f) ∪ 𝔸(⟨∅⟩σ^{T}) =

𝔸(f) ∪ 𝔸(⟨𝕍(f)⟩σ^{T}).

𝕍(fσ) = 𝕍(f) = ∅ = 𝕍(∅) = 𝕍(⟨∅⟩σ^{T}) = 𝕍(⟨𝕍(f)⟩σ^{T}). \underline{t = y^{𝔹} (a bound atom):} 𝔸(y^{𝔹}σ) = 𝔸(y^{𝔹}) = 𝔸(y^{𝔹})∪∅ = 𝔸(y^{𝔹})∪𝔸(∅) = 𝔸(y^{𝔹})∪𝔸(⟨∅⟩σ^{T}) =

𝔸(y^{𝔹}) ∪ 𝔸(⟨𝕍(y^{𝔹})⟩σ^{T}).

𝕍(y^{𝔹}σ) = 𝕍(y^{𝔹}) = ∅ = 𝕍(∅) = 𝕍(⟨∅⟩σ^{T}) = 𝕍(⟨𝕍(y^{𝔹})⟩σ^{T}). \underline{t = x^{𝔸} (an atom):} 𝔸(x^{𝔸}σ) = 𝔸(x^{𝔸}) = 𝔸(x^{𝔸}) ∪ ∅ = 𝔸(x^{𝔸}) ∪ 𝔸(∅) = 𝔸(x^{𝔸}) ∪ 𝔸(⟨∅⟩σ^{T}) =

𝔸(x^{𝔸}) ∪ 𝔸(⟨𝕍(x^{𝔸})⟩σ^{T}).

𝕍(x^{𝔸}σ) = 𝕍(x^{𝔸}) = ∅ = 𝕍(∅) = 𝕍(⟨∅⟩σ^{T}) = 𝕍(⟨𝕍(x^{𝔸})⟩σ^{T}). \underline{t = t_{1}t_{2} (an application):} 𝔸((t_{1}t_{2})σ) = 𝔸((t_{1}σ)(t_{2}σ)) = ⋃_{i∈\{1,2\}} 𝔸(t_{i}σ) =

⋃_{i∈{1,2}} 𝔸(t_{i}) ∪ ⋃_{i∈{1,2}} 𝔸(⟨𝕍(t_{i})⟩σ^{T}) =

𝔸(t_{1}t_{2}) ∪ 𝔸( ⋃_{i∈{1,2}} ⟨𝕍(t_{i})⟩σ^{T} ) = 𝔸(t_{1}t_{2}) ∪ 𝔸( ⟨⋃_{i∈{1,2}} 𝕍(t_{i})⟩σ^{T} ) = 𝔸(t_{1}t_{2}) ∪ 𝔸(⟨𝕍(t_{1}t_{2})⟩σ^{T}). 𝕍((t_{1}t_{2})σ) = 𝕍((t_{1}σ)(t_{2}σ)) = ⋃_{i∈{1,2}} 𝕍(t_{i}σ) = ⋃_{i∈{1,2}} 𝕍(⟨𝕍(t_{i})⟩σ^{T}) = 𝕍( ⋃_{i∈{1,2}} ⟨𝕍(t_{i})⟩σ^{T} ) = 𝕍( ⟨⋃_{i∈{1,2}} 𝕍(t_{i})⟩σ^{T} ) = 𝕍(⟨𝕍(t_{1}t_{2})⟩σ^{T}). \underline{t = λy^{𝔹}. t′ (an abstraction):} 𝔸((λy^{𝔹}. t′)σ) = 𝔸(λy^{𝔹}. (t′σ)) = 𝔸(t′σ) =

𝔸(t′) ∪ 𝔸(⟨𝕍(t′)⟩σ^{T}) = 𝔸(λy^{𝔹}. t′) ∪ 𝔸(⟨𝕍(λy^{𝔹}. t′)⟩σ^{T}).

𝕍((λy^{𝔹}. t′)σ) = 𝕍(λy^{𝔹}. (t′σ)) = 𝕍(t′σ) = 𝕍(⟨𝕍(t′)⟩σ^{T}) = 𝕍(⟨𝕍(λy^{𝔹}. t′)⟩σ^{T}).

\underline{t = (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) (a pending):} 𝔸( (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})σ ) = 𝔸( \{ (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})σ \} ) =

∅ ∪ 𝔸( ⟨\{ (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) \}⟩σ^{T} ) = 𝔸(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) ∪ 𝔸( ⟨𝕍(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})⟩σ^{T} ).

𝕍( (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})σ ) = 𝕍( \{ (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})σ \} ) = 𝕍( ⟨\{ (\begin{matrix}z^{𝕍} \\ θ′ \end{matrix}) \}⟩σ^{T} ) = 𝕍( ⟨𝕍(\begin{matrix}z^{𝕍} \\ θ′ \end{matrix})⟩σ^{T} ).

Q.e.d. (Lemma 2.11)

Definition 2.12 ([Finite] Positive/Negative Variable-Condition) A [finite] positive/negative variable-condition is a pair (P, N) with

and \begin{aligned}P & ⊆ & 𝕍𝔸 & × & 𝕍 \\ N & ⊆ & 𝕍 & × & 𝔸 \end{aligned}

[and |P | , |N| ∈ N].

Definition 2.13 (Consistency) A pair (P, N) is consistent if

and  P is well-founded P^{+} ∘ N is irreflexive.

Corollary 2.14 If (P, N) is a finite positive/negative variable-condition, then (P, N) is consistent iff each cycle in the directed graph of P ⊎N contains more than one edge from N. The latter can be effectively tested with time complexity of |P | + |N|.

Note that, in the finite case, the test of Corollary 2.14 seems to be both the most efficient and the most human-oriented way to represent the question of consistency of positive/negative variable-conditions.

Definition 2.15 (Admission Relation) Let (P, N) be a positive/negative variable-condition. The admission relation A_{(P,N)} is given as

( x^{𝔸}, (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) ) ∈ A_{(P,N)} if (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) is a pending and x^{𝔸} ∈ 𝔸 ∩ P^{+}⟨\{z^{𝕍}\}⟩.

The occurrence relation O is given as

( x^{𝔸}, (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) ) ∈ O if (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) is a pending and x^{𝔸} ∈ NT (θ).

The notion of an occurrence of a variable or an atom in a term we need in the following is not the simple one of a participation in the mutually inductive construction of terms and finite atom variables. The reason is that a variable in a pending may stand for any term with atoms from its permission set.

Definition 2.16 (𝔸_{(P,N)}(t), 𝕍_{(P,N)}(t)) Let A be a binary relation. The (free) atoms 𝔸_{A}(t) of a term t w.r.t. A and the (free) variables 𝕍_{A}(t) of a term t w.r.t. A are recursively defined according to the following table:

t  𝔸_{A}(t)  𝕍_{A}(t)
T (a set of terms)  ⋃_{t∈T} 𝔸_{A}(t)  ⋃_{t∈T} 𝕍_{A}(t)
f (a constant)  ∅  ∅
x^{𝔸} (an atom)  {x^{𝔸}}  ∅
y^{𝔹} (a bound atom)  ∅  ∅
t_{1}t_{2} (an application)  𝔸_{A}({t_{1}, t_{2}}) 𝕍_{A}({t_{1}, t_{2}})
λy^{𝔹}. t′ (an abstraction)  𝔸_{A}(t′)  𝕍_{A}(t′)
(\begin{matrix}z^{𝕍} \\ θ \end{matrix}) (a pending); setting X := A\begin{matrix}⟨ \\ \{ & (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) & \} \\ ⟩ \end{matrix} 𝔸_{A}(⟨X⟩θ) \{z^{𝕍}\} ∪ 𝕍_{A}(⟨X⟩θ)

Moreover, we set 𝕍𝔸_{A}(t) := 𝔸_{A}(t) ⊎ 𝕍_{A}(t).

Lemma 2.17 𝕍_{A_{(P,N)}}(t) ⊆ 𝕍_{O}(t). 𝔸_{A_{(P,N)}}(t) ⊆ 𝔸_{O}(t) ∪ P^{+}⟨𝕍_{O}(t)⟩.

Corollary 2.18 𝕍𝔸_{A_{(P,N)}}(t) is finitary in P in the sense that for every term t there is a finite P′ ⊆ P with 𝕍𝔸_{A_{(P,N)}}(t) = 𝕍𝔸_{A_{(P′,∅)}}(t) .

Corollary 2.19 Let (P, N) be finite positive/negative variable-condition. Let t be a term. All the sets 𝔸_{A_{(P,N)}}(t), 𝔸_{O}(t), 𝕍_{A_{(P,N)}}(t), 𝕍_{O}(t) are always finite. We have 𝔸_{A_{(P,N)}}(t) ⊆ 𝔸_{O}(t) ⊆ 𝔸, and 𝕍_{A_{(P,N)}}(t) ⊆ 𝕍_{O}(t) ⊆ 𝕍.

2.1 Extensions, σ-Updates, and (P, N)-Substitutions

Within a reasoning process, positive/negative variable-conditions may be subject to only one kind of transformation, which we simply call an “extension”.

Definition 2.20 ([Weak] Extension) (P′, N′) is an [weak] extension of (P, N) if (P′, N′) is a positive/negative variable-condition, P ⊆ P′ [or at least P ⊆ (P′)^{+}], and N ⊆ N′.

As an immediate corollary of Definitions 2.20 and 2.13 we get:

Corollary 2.21 If (P′, N′) is a consistent positive/negative variable-condition and an [weak] extension of (P, N), then (P, N) is a consistent positive/negative variable-condition as well.

A σ-update is a special form of an extension:

Definition 2.22 (σ-Update, Dependence) Let (P, N) be a finite positive/negative variable-condition. Let σ be a finite variable substitution. The (P, N)-dependence of σ is the smallest set D such that P ⊆ D and

{ (z^{𝕍𝔸}, x^{𝕍}) | x^{𝕍} ∈ NT (σ) ∧ z^{𝕍𝔸} ∈ 𝕍𝔸_{A_{(D,N)}}(σ(x^{𝕍})) } ⊆ D.

The σ-update of (P, N) is (D, N).

As a corollary of Corollary 2.19, we get:

Lemma 2.23 The σ-update (D, N) of a finite positive/negative variable-condition (P, N) and a finite variable substitution σ satisfies

D ⊆ P ∪ ( ( ⋃_{x^{𝕍}∈NT (σ)} 𝕍𝔸_{O}(σ(x^{𝕍})) ) × NT (σ) ),

so, especially, (D, N) is a finite positive/negative variable-condition.

Proof of Lemma 2.23 By Corollary 2.18, the closure operator of Definition 2.22 is finitary for a finite variable substitution σ. Moreover, it is monotonic. Thus, we get the set D as the ω-closure of P. By Corollary 2.19, it now suffices to show that all finite applications of the closure operator satisfy the displayed equation of Lemma 2.23. So let us consider a

pending (\begin{matrix}z^{𝕍} \\ θ \end{matrix}). Set X := A_{(D,N)}\begin{matrix}⟨ \\ \{ & (\begin{matrix}z^{𝕍} \\ θ \end{matrix}) & \} \\ ⟩ \end{matrix}. Then X = 𝔸 ∩ D^{+}⟨\{z^{𝕍}\}⟩. Then ⟨X⟩θ =

⟨X ∩ NT (θ)⟩θ ∪ ⟨X \ NT (θ)⟩θ = ⟨X ∩ NT (θ)⟩θ ∪ (X \ NT (θ)) ⊆ ⟨NT (θ)⟩θ ∪ (X \ NT (θ)). Thus, 𝕍_{A_{(D,N)}}(⟨X⟩θ) ⊆ 𝕍_{A_{(D,N)}}(⟨NT (θ)⟩θ) and 𝔸_{A_{(D,N)}}(⟨X⟩θ) ⊆ 𝔸_{A_{(D,N)}}(⟨NT (θ)⟩θ) ∪ (X \ NT (θ)). Q.e.d. (Lemma 2.23)

Definition 2.24 ((P, N)-Substitution) Let (P, N) be a positive/negative variable-condition. σ is a (P, N)-substitution if σ is a variable substitution and the σ-update of (P, N) is consistent.

Syntactically, (x^{𝕍}, a^{𝔸}) ∈ N is to express that a (P, N)-substitution σ must not replace x^{𝕍} with a term in which a^{𝔸} could ever occur; i.e. that a^{𝔸} is fresh for x^{𝕍}: a^{𝔸} # x^{𝕍}. This is indeed guaranteed if any σ-update (P′, N′) of (P, N) is again required to be consistent, and so on. We can see this as follows: For z^{𝕍} ∈ 𝕍(σ(x^{𝕍})), we get

z^{𝕍} P′ x^{𝕍} N′ a^{𝔸}.

If we now try to apply a second substitution σ′ with a^{𝔸} ∈ 𝔸(σ′(z^{𝕍})) (so that a^{𝔸} occurs in (x^{𝕍}σ)σ′, contrary to what we initially expressed as our freshness intention), then σ′ is not a (P′, N′)-substitution because, for the σ′-update (P′′, N′′) of (P′, N′), we have

a^{𝔸} P′′ z^{𝕍} P′′ x^{𝕍} N′′ a^{𝔸};

so (P′′)^{+} ∘ N′′ is not irreflexive. All in all, the positive/negative variable-condition

• (P′, N′) blocks any instantiation of (x^{𝕍}σ) resulting in a term containing a^{𝔸}, just as

• (P, N) blocked x^{𝕍} before the application of σ.