1–LABEL:LastPageMay 23, 2017May 22, 2018 enumeratei*enumeratei

# The language of Stratified Sets is confluent and strongly normalising

Murdoch J. Gabbay  Heriot-Watt University, Scotland, UK www.gabbay.org.uk

###### Abstract.

We study the properties of the language of Stratified Sets (first-order logic
with $\in$ and a stratification condition) as used in TST, TZT, and (with
stratifiability instead of stratification) in Quine’s NF. We find that the
syntax forms a nominal algebra for substitution and that stratification and
stratifiability imply confluence and strong normalisation under rewrites
corresponding naturally to $\beta$-conversion.

###### Key words and phrases:

Stratified syntax, typed set theory, Quine’s New Foundations, nominal
rewriting, nominal algebra

###### 1991 Mathematics Subject Classification:

D.3.1: Syntax; F.3.2: Operational Semantics; F.4.1: Set theory

Thanks to the editor and to the anonymous referees

##  1\. Introduction

###  1.1. About Stratified Sets

Consider Russell’s paradox, that if $s=\\{a\mid a\not\in a\\}$ then $s\in s$
if and only if $s\not\in s$. One way to avoid the term $s$ is to restrict to
the language of _Stratified Sets_. This is first-order logic with a binary
relation $t{\boldsymbol{\in}}s$ whose intuition is ‘$t$ is an element of $s$’
and:

  * •

Variable symbols $a$ (called _atoms_ in this paper) are assigned levels, which
are typically integers or natural numbers.

  * •

We impose a _stratification_ typing condition that we may only form
$t{\boldsymbol{\in}}s$ if the level of $s$ is one plus the level of $t$.
$\mathit{level}(s)=\mathit{level}(t){\text{+}}1$.

See Definition 66 for full details. Then $s=\\{a\mid a\not\in a\\}$ cannot be
stratified, since whatever level we assign to $a$ in $a\in a$ we cannot make
$\mathit{level}(a)=\mathit{level}(a){\text{+}}1$.

Stratified Sets are one of a family of syntaxes designed to exclude Russell’s
paradox:

The language of ZF set theory restricts sets comprehension to bounded
comprehension $\\{a\in X\mid\phi\\}$.

Type Theories (such as Higher-Order Logic) impose more or less elaborate type
systems. The canonical example of this is _simple types_
$\tau::=\iota\mid\tau\to\tau$.

Stratified Sets stratifies terms as described. One feature of Stratified Sets
is that we can write a term representing the universal set:

$\mathbf{univ}=\\{a\mid\top\\}$

is easily stratified by giving $a$ any level we like. Likewise we can write
definitions such as ‘the number 2’ to be ‘the set of all two-element sets’:

$\mathbf{2}=\\{a\mid\exists b,c.(a=\\{b,c\\}\wedge b\neq c)\\}$

(Here we freely use syntactic sugar for readability; this can all be made
fully formal.)

This feels liberating: we have the pleasure of full unbounded sets
comprehension111It still needs to be stratified, of course, but by Russell’s
paradox we must expect our party to be spoiled. Our choices are only: how, and
where? and we have the pleasure of more sweeping types than are possible in
the usual type theories such as Higher-Order Logic and its elaborations.222Two
attitudes are possible with types: embrace and enrich them, which leads us in
the direction of (for instance) dependent types, or minimise type structure.
Stratification minimises types all the way down to just being
‘$i\in\mathbb{Z}$’.

###  1.2. What this paper does

The published literature using Stratified Sets does not view the basic syntax
from the point of view of rewriting. On this topic, this paper makes three
observations:

  1. (1)

The stratification condition implies that the syntax is confluent and strongly
normalising under the natural rewrite

$t\in\\{a\mid\phi\\}\quad\to\quad\phi[a{{:}\text{=}}t].$

We can write:

> _Stratification_ $\Rightarrow$  _confluence and strong normalisation_.

Similarly for stratifiability. See Theorems 89 and 91.

  2. (2)

The syntax of normal forms becomes an algebra for substitution in a sense that
will be made formal using nominal algebra.

See Theorem 55; in fact the proof of Theorem 89 uses this.

  3. (3)

Our proof is constructed using nominal techniques. The proofs in this paper
should be fairly directly implementable in a nominal theorem-prover, such as
Nominal Isabelle [Urb08].

In some senses, this paper is deliberately conventional, even simple: we write
down a syntax and a rewrite relation and prove some nice properties. But the
simplicity is deceptive:

TST, TZT, and NF as usually presented do not include sets comprehension in
their syntax, if that syntax is even made fully formal. So just noting that
there are rewrite relations here that might be useful to look at, seems to be
a new observation.

The proofs are not trivial. It is easy to give a handwaving argument (such as
that given in the first half of Remark 6 below) but it is surprisingly
difficult to give a rigorous proof with all details. More on this in Section
6.

We use nominal techniques (see the material in Section 2) to manage the
$\alpha$-binding in the syntax for universal quantification and sets
comprehension. If the reader is unfamiliar with nominal techniques then they
can just ignore this aspect: wherever we see reference to a nominal theorem,
we can replace it with ‘by $\alpha$-conversion’ or with ‘it is a fact of
syntax that’. The result should then be close to the kind of argument that
might normally pass without comment or challenge.

###  1.3. Some remarks

######  Remark 1.

‘The language of Stratified Sets’ is a description specific to this paper. In
the literature, this syntax is unnamed and presented along with the theory we
express using it:

  1. (1)

TST (which stands for Typed Set Theory) is typically taken to be first-order
logic with $\in$ and variables stratified as $\mathbb{N}=\\{0,1,2,\dots\\}$,
along with reasonable axioms for first-order logic and extensional sets
equality.

  2. (2)

TZT is typically taken to be as the syntax and axioms of TST but with
variables stratified as
$\mathbb{Z}=\\{0,1,{\text{-}}1,2,{\text{-}}2,\dots\\}$.

  3. (3)

Quine’s New Foundations (NF) uses the language of first-order logic with
$\in$, and reasonable axioms, and a stratifiability condition that variables
_could_ be stratified.

So in TST we would have to write (say) $a^{1}\in b^{2}$ (choosing a level 1
variable symbol $a$ and a level 2 variable symbol $b$), whereas in NF we could
write just $a\in b$ and say “we _could_ assign $a$ level 1 and $b$ level 2”.

######  Remark 2.

There is a slight ambiguity when we talk about stratification whether we
insist that the syntax come delivered with an assignment of levels to all
terms, or whether we insist on the weaker condition that an assignment _could_
be made, but this assignment need not be a structural part of the formula or
term. This distinguishes the languages of TST and TZT from that of NF: TST and
TZT insist on stratification, and NF insists on stratifiability.

Our results will be agnostic in this choice (see for instance Theorems 89 and
91). So when we write _Stratified Sets_ we could just as well write
_Stratifiable Sets_ and everything would still work with only minor
bookkeeping changes.

######  Remark 3.

The reader with a background in TST, TZT, and NF should note that this is not
a paper about logical theories: it is a paper about their _syntax_. This is
why we talk about ‘Stratified Sets’ in this paper, and not e.g. ‘Typed Set
Theories’. Our protagonist is a language, not a logic.

######  Remark 4 (Some words on terminology).

Some authors expand TST as ‘Theory of Simple Types’. I think this terminology
invites confusion with Simple Type Theory, so I prefer the alternative ‘Typed
Set Theory’. I would also like to write that TZT stands for ‘Typed Zet
Theory’, but really TZT just stands for itself.

######  Remark 5 (References).

For the reader interested in the logical motivations for these syntaxes we
provide references:

A historical account of Russell’s paradox is in [Gri04].

For ZF set theory, see e.g. [Jec06].

Excellent discussions of TST, TZT, and NF are in [For95] and [Hol98], and a
clear summary with a brief but well-chosen bibliography is in [For97].

######  Remark 6 (Connection to the $\lambda$-calculus).

One way to see that something _like_ this paper _should_ work, fingers
crossed, is by an analogy:

The rewrite $t\in\\{a\mid\phi\\}\to\phi[a{{:}\text{=}}t]$ can be rewritten as
$(\lambda a.\phi)t\to\phi[a{{:}\text{=}}t]$.

Extensionality is $s=\\{b\mid b\in s\\}$, and we can rewrite this as
$s=\lambda b.(sb)$. These are of course familiar as $\beta$-reduction and
$\eta$-expansion. The proofs need to be checked but the analogy above invites
an analysis of the kind that we will now carry out.

And indeed this has been done, though not for stratified sets. In [KA10] (many
thanks to an anonymous referee for bringing this to my attention) a
development analogous to what is done in this paper for stratified syntax
using nominal techniques, is carried out for the simply-typed lambda-calculus
using de Bruijn indexes. Definitions and results bear a very nice comparison:
for instance, Lemma 6 of [KA10] corresponds to Proposition 74.333There are
also differences: In [KA10] the authors implement their proof in Agda, whereas
implementation of the proofs in this paper for future work. On the other hand,
proofs in this paper are given more-or-less in full, whereas in [KA10] the
authors elide technical details. This paper proves confluence and strong
normalisation, which is strictly more than [KA10] which considers only the
existence of a reduction path to normal forms.

A technical device in [KA10], which goes back to a quite technical development
in [WCPW03], is to work directly with a datatype of normal forms and
substitution on them; this is just like the _internal syntax_ and its _sigma-
action_ that we will see in this paper.

For me the motivation for setting things up in this way is partly practical
and partly abstract: internal syntax with its sigma-action turns out to be a
nominal sigma-algebra (Theorem 55) and this ties in with a literature on
advanced nominal models of logic and computation [Gab16, GG17, GM08]. This
paper was originally conceived as a prelude to building advanced nominal
models of stratified and stratifiable syntaxes and type theories, though it
has acquired independent interest.

It is therefore interesting to see analogous design choices appearing
independently, motivated by apparently purely implementational concerns: what
is good for the abstract mathematics also seems to be good for the proof-
engineering.

##  2\. Background on nominal techniques

Intuitively, a nominal set is “a set $\mathsf{X}$ whose elements
$x\in\mathsf{X}$ may ‘contain’ finitely many names $a,b,c\in\mathbb{A}$”. We
may call names _atoms_. The notion of ‘contain’ used here is not the obvious
notion of ‘is a set element of’: formally, we say that $x$ has _finite
support_ (Definition 13).

Nominal sets are formally defined in Subsection 2.1. Examples are in
Subsection 2.2. The reader might prefer to read this section only briefly at
first, and then use it as a reference for the later sections where these
underlying ideas get applied. More detailed expositions are also in [GP01,
Gab11, DG12a, Pit13].

In the context of the broader literature, the message of this section is as
follows:

The reader with a category-theory background can read this section as
exploring the category of nominal sets, or equivalently the Schanuel topos
(more on this in [MM92, Section III.9], [Joh03, A.21, page 79], or [Gab11,
Theorem 9.14]).

The reader with a sets background can read this section as stating that we use
Fraenkel-Mostowski set theory (FM sets).

A discussion of this sets foundation, tailored to nominal techniques, can be
found in [Gab11, Section 10]. FM sets add _urelemente_ or _atoms_ to the sets
universe.

The reader uninterested in foundations can note that previous work [GP01,
Gab11, DG12a] has shown that just assuming names as primitive entities in
Definition 7 yields a remarkable clutch of definitions and results, including
Theorem 14, Corollary 15, and Theorem 27.

###  2.1. Basic definitions

####  2.1.1. Atoms and permutations

######  Definition 7.

For each $i{\in}{\mathbb{Z}}$ fix a disjoint countably infinite set
$\mathbb{A}^{{i}}$ of atoms.444These will serve as variable symbols in
Definition 31.

Write $\mathbb{A}=\bigcup_{i{\in}{\mathbb{Z}}}\mathbb{A}^{{i}}$.

If $a{\in}\mathbb{A}$ (so $a$ is an atom) write $\mathit{level}(a)$ for the
unique number such that $a{\in}\mathbb{A}^{{\mathit{level}(a)}}$.

We use a permutative convention that $a,b,c,\ldots$ range over _distinct_
atoms.

If we do not wish to use the permutative convention then we will refer to the
atom using $n$ (see for instance ${\mathrm{\bf(\sigma{\text{\tt elt}}\text{\tt
atm})}}$ of Figure 2).

####  2.1.2. Permutation actions on sets

######  Definition 8.

Suppose $\pi:\mathbb{A}\cong\mathbb{A}$ is a bijection on atoms.

  1. (1)

If $\mathit{nontriv}(\pi)=\\{a\mid\pi(a)\neq a\\}$ is finite then we call
$\pi$ finite.

  2. (2)

If $\pi(a)\in\mathbb{A}^{{i}}\Leftrightarrow a\in\mathbb{A}^{{i}}$ then call
$\pi$ sort-respecting.

  3. (3)

A permutation $\pi$ is a finite sort-respecting bijection on atoms.

Henceforth $\pi$ will range over permutations.

We will use the following notations in the rest of this paper:

Write $\mathrm{id}$ for the identity permutation such that $\mathrm{id}(a)=a$
for all $a$.

Write $\pi^{\prime}\circ\pi$ for composition, so that
$(\pi^{\prime}\circ\pi)(a)=\pi^{\prime}(\pi(a))$.

If $i{\in}{\mathbb{Z}}$ and $a,b{\in}\mathbb{A}^{{i}}$ then write $(a\;b)$ for
the swapping (terminology from [GP01]) mapping $a$ to $b$, $b$ to $a$, and all
other $c$ to themselves, and take $(a\;a)=\mathrm{id}$.

Write $\pi^{{\text{-}1}}$ for the inverse of $\pi$, so that
$\pi^{{\text{-}1}}\circ\pi=\mathrm{id}=\pi\circ\pi^{{\text{-}1}}$.

####  2.1.3. Sets with a permutation action

If $A\subseteq\mathbb{A}$ write

$\mathit{fix}(A)=\\{\pi\mid\forall a{\in}A.\pi(a)=a\\}.$

######  Definition 9.

A set with a permutation action $\mathsf{X}$ is a pair
$(|\mathsf{X}|,{\cdot})$ of an underlying set $|\mathsf{X}|$ and a permutation
action written $\pi{\cdot}x$ which is a group action on $|\mathsf{X}|$, so
that $\mathrm{id}{\cdot}x=x$ and
$\pi{\cdot}(\pi^{\prime}{\cdot}x)=(\pi\circ\pi^{\prime}){\cdot}x$ for all
$x\in\mathsf{X}$ and permutations $\pi$ and $\pi^{\prime}$.

######  Definition 10.

Say that $A\subseteq\mathbb{A}$ supports $x\in\mathsf{X}$ when
$\forall\pi.\pi\in\mathit{fix}(A)\Rightarrow\pi{\cdot}x=x$.

If a finite $A\subseteq\mathbb{A}$ supporting $x$ exists, call $x$ finitely
supported (by $A$) and say that $x$ has finite support.

If $\mathsf{X}$ is a set with a permutation action then we may write

$x\in\mathsf{X}$ as shorthand for $x\in|\mathsf{X}|$, and

$X\subseteq\mathsf{X}$ as shorthand for $X\subseteq|\mathsf{X}|$.

####  2.1.4. Nominal sets

######  Definition 11.

Call a set with a permutation action $\mathsf{X}$ a nominal set when every
$x\in\mathsf{X}$ has finite support. $\mathsf{X}$, $\mathsf{Y}$, $\mathsf{Z}$
will range over nominal sets.

######  Definition 12.

Call a function $f\in\mathsf{X}{\Rightarrow}\mathsf{Y}$ equivariant when
$\pi{\cdot}(f(x))=f(\pi{\cdot}x)$ for all permutations $\pi$ and
$x\in\mathsf{X}$. In this case write $f:\mathsf{X}{\Rightarrow}\mathsf{Y}$.

The category of nominal sets and equivariant functions between them is usually
called the category of _nominal sets_.

######  Definition 13.

Suppose $\mathsf{X}$ is a nominal set and $x\in\mathsf{X}$. Define the support
of $x$ by

$\mathit{supp}(x)=\bigcap\\{A{\subseteq}\mathbb{A}\mid A\text{ is finite and
supports }x\\}.$

Write $a\text{\tt\\#}x$ as shorthand for $a\not\in\mathit{supp}(x)$ and read
this as $a$ is fresh for $x$.

If $T{\subseteq}\mathbb{A}$ write $T\text{\tt\\#}x$ as shorthand for $\forall
a{\in}T.a\text{\tt\\#}x$.

Given atoms $a_{1},\dots,a_{n}$ and elements $x_{1},\dots,x_{m}$ write
$a_{1},\dots,a_{n}\text{\tt\\#}x_{1},\dots,x_{m}$ as shorthand for $\forall
1{\leq}j{\leq}m.\\{a_{1},\dots,a_{n}\\}\text{\tt\\#}x_{j}$. That is:
$a_{i}\text{\tt\\#}x_{j}$ for every $i$ and $j$.

######  Theorem 14.

Suppose $\mathsf{X}$ is a nominal set and $x\in\mathsf{X}$. Then
$\mathit{supp}(x)$ is the unique least finite set of atoms that supports $x$.

######  Proof 2.1.

See [Gab11, Theorem 2.21(1)].

######  Corollary 15.

If $\pi(a)=a$ for all $a\in\mathit{supp}(x)$ then $\pi{\cdot}x=x$.
Equivalently:

If $\pi{\in}\mathit{fix}(\mathit{supp}(x))$ then $\pi{\cdot}x=x$.

If $\forall a{\in}\mathbb{A}.(\pi(a){\neq}a\Rightarrow a\text{\tt\\#}x)$ then
$\pi{\cdot}x=x$ (see Notation 2.1.4).

If $\pi(a)=\pi^{\prime}(a)$ for every $a{\in}\mathit{supp}(x)$ then
$\pi{\cdot}x=\pi^{\prime}{\cdot}x$.

$a\text{\tt\\#}x$ if and only if $\exists
b.(b\text{\tt\\#}x\wedge(b\;a){\cdot}x=x)$.

######  Proof 2.2.

By routine calculations from the definitions and from Theorem 14 (see also
[Gab11, Theorem 2.21(2)]).

###  2.2. Examples

Suppose $\mathsf{X}$ and $\mathsf{Y}$ are nominal sets. We consider some
examples, some of which will be useful later.

####  2.2.1. Atoms

$\mathbb{A}$ is a nominal set with the _natural permutation action_
$\pi{\cdot}a=\pi(a)$.

####  2.2.2. Cartesian product

$\mathsf{X}\times\mathsf{Y}$ is a nominal set with underlying set
$\\{(x,y)\mid x\in\mathsf{X},y\in\mathsf{Y}\\}$ and the _pointwise_ action
$\pi{\cdot}(x,y)=(\pi{\cdot}x,\pi{\cdot}y)$.

It is routine to check that
$\mathit{supp}((x,y))=\mathit{supp}(x){\cup}\mathit{supp}(y)$.

####  2.2.3. Full function space

$\mathsf{X}{\to}\mathsf{Y}$ is a set with a permutation action with underlying
set all functions from $|\mathsf{X}|$ to $|\mathsf{Y}|$, and the conjugation
permutation action

$(\pi{\cdot}f)(x)=\pi{\cdot}(f(\pi^{{\text{-}1}}{\cdot}x)).$

####  2.2.4. Finite-supported function space

$\mathsf{X}{\Rightarrow}\mathsf{Y}$ is a nominal set with underlying set the
functions from $|\mathsf{X}|$ to $|\mathsf{Y}|$ with finite support under the
conjugation action, and the conjugation permutation action.

####  2.2.5. Full powerset

######  Definition 16.

Suppose $\mathsf{Z}$ is a set with a permutation action. Give subsets
$Z\subseteq\mathsf{Z}$ the pointwise permutation action

$\pi{\cdot}Z=\\{\pi{\cdot}z\mid z\in Z\\}.$

Then $\mathit{pset}(\mathsf{Z})$ (the full powerset of $\mathsf{Z}$) is a set
with a permutation action with

underlying set $\\{Z\mid Z\subseteq\mathsf{Z}\\}$ (the set of all subsets of
$|\mathsf{Z}|$), and

the pointwise action $\pi{\cdot}Z=\\{\pi{\cdot}z\mid z\in Z\\}$.

A particularly useful instance of the pointwise action is for sets of atoms.
As discussed in Subsection 2.2.1 above, if $a\in\mathbb{A}$ then
$\pi{\cdot}a=\pi(a)$. Thus if $A\subseteq\mathbb{A}$ then

$\pi{\cdot}A\quad\text{means}\quad\\{\pi(a)\mid a\in A\\}.$

######  Lemma 17.

Even if $\mathsf{Z}$ is a nominal set, $\mathit{pset}(\mathsf{Z})$ need not be
a nominal set.

######  Proof 2.3.

Take $\mathsf{Z}=\mathbb{A}$ which we enumerate as
$\\{a_{0},a_{1},a_{2},\dots\\}$ and we take $Z\in\mathit{pset}(\mathsf{Z})$ to
be equal to $\mathit{comb}$ defined by

$\mathit{comb}=\\{a_{0},a_{2},a_{4},\dots\\}.$

This does not have finite support (see also [Gab11, Remark 2.18]).

####  2.2.6. Finite powerset

For this subsection, fix a nominal set $\mathsf{X}$.

######  Definition 18.

Write $\mathit{FinPow}(\mathsf{X})$ for the nominal set with

underlying set the set of all finite subsets of $\mathsf{X}$,

with the pointwise action from Definition 16.

We might write $X\mathbin{\subseteq_{\text{\it fin}}}\mathsf{X}$ for
$X{\in}\mathit{FinPow}(\mathsf{X})$.

######  Lemma 19.

If $X\mathbin{\subseteq_{\text{\it fin}}}\mathsf{X}$ then:

$\bigcup\\{\mathit{supp}(x)\mid x{\in}X\\}$ is finite.

$\bigcup\\{\mathit{supp}(x)\mid x{\in}X\\}=\mathit{supp}(X)$.

$x\in X$ implies $\mathit{supp}(x)\subseteq\mathit{supp}(X)$.

Rewriting this using Notation 2.1.4: if $X$ is finite and $x{\in}X$ then
$a\text{\tt\\#}X$ implies $a\text{\tt\\#}x$.555This is not necessarily true if
$X$ is infinite. For instance if we take $\mathsf{X}=\mathbb{A}=X$ then the
reader can verify that $a\text{\tt\\#}X$ for every $a$, but $a\text{\tt\\#}a$
does not hold for any $a\in\mathbb{A}$. This is a feature of nominal
techniques, not a bug; but for the case of finite sets, things are simpler.

######  Proof 2.4.

The first part is immediate since by assumption there is some finite
$A{\subseteq}\mathbb{A}$ that bounds $\mathit{supp}(x)$ for all $x\in X$. The
second part follows by an easy calculation using part 3 of Corollary 15; full
details are in [Gab11, Theorem 2.29], of which Lemma 19 is a special case.
Part 3 follows from the first and second parts.

####  2.2.7. Atoms-abstraction

Atoms-abstraction was the first real application of nominal techniques; it was
used to build inductive datatypes of syntax-with-binding. Nominal atoms-
abstraction captures the essence of $\alpha$-binding. In this paper we use it
to model the binding in universal quantification and sets comprehension (see
Definition 31). The maths here goes back to [Gab01, GP01]; we give references
to proofs in a more recent presentation [Gab11].

Assume a nominal set $\mathsf{X}$ and an $i{\in}{\mathbb{Z}}$.

######  Definition 20.

Let the atoms-abstraction set $[\mathbb{A}^{{i}}]\mathsf{X}$ have

Underlying set $\\{[a]x\mid a{\in}\mathbb{A}^{{i}},\ x\in\mathsf{X}\\}$ where
$[a]x=\\{(\pi(a),\pi{\cdot}x)\mid\pi\in\mathit{fix}(\mathit{supp}(x){\setminus}\\{a\\})\\}$.

Permutation action $\pi{\cdot}[a]x=[\pi{\cdot}a]\pi{\cdot}x$.

######  Lemma 21.

If $x{\in}\mathsf{X}$ and $a{\in}\mathbb{A}^{{i}}$ then
$\mathit{supp}([a]x)=\mathit{supp}(x){\setminus}\\{a\\}$. In particular
$a\text{\tt\\#}[a]x$ (Notation 2.1.4).

######  Proof 2.5.

See [Gab11, Theorem 3.11].

######  Lemma 22.

Suppose $x{\in}\mathsf{X}$ and $a,b{\in}\mathbb{A}^{{i}}$. Then if
$b\text{\tt\\#}x$ then $[a]x=[b](b\ a){\cdot}x$.

######  Proof 2.6.

See [Gab11, Lemma 3.12].

######  Definition 23.

Suppose $z{\in}[\mathbb{A}^{{i}}]\mathsf{X}$ and $b{\in}\mathbb{A}^{{i}}$.
Write $z\text{@}b$ for the unique $x\in\mathsf{X}$ such that $z=[b]x$, if this
exists.

######  Lemma 24.

Suppose $b{\in}\mathbb{A}^{{i}}$ and $z\in[\mathbb{A}^{{i}}]\mathsf{X}$. Then
$b\text{\tt\\#}z$ implies $z\text{@}b\in\mathsf{X}$ is well-defined.

######  Proof 2.7.

See [Gab11, Theorem 3.19].

######  Lemma 25.

Suppose $a{\in}\mathbb{A}^{{i}}$ and $x{\in}\mathsf{X}$ and
$z\in[\mathbb{A}^{{i}}]\mathsf{X}$. Then:

$([a]x)\text{@}a=x$ and if $b\text{\tt\\#}x$ then $([a]x)\text{@}b=(b\
a){\cdot}x$.

If $a\text{\tt\\#}z$ then $[a](z\text{@}a)=z$.

######  Proof 2.8.

See [Gab11, Theorem 3.19].

###  2.3. The principle of equivariance

######  Remark 26.

We now come to the _principle of equivariance_ (Theorem 27; see also [Gab11,
Subsection 4.2] and [GP01, Lemma 4.7]). It enables a particularly efficient
management of renaming and $\alpha$-conversion in syntax and semantics and
captures why it is so useful to use _names_ to model them instead of, for
instance, numbers.

In a nutshell we can say

> _Atoms are distinguishable, but interchangable._

and we make this formal as follows:

######  Theorem 27.

Suppose $\overline{x}$ is a list $x_{1},\ldots,x_{n}$. Suppose $\pi$ is a (not
necessarily finite) permutation and write $\pi{\cdot}\overline{x}$ for
$\pi{\cdot}x_{1},\ldots,\pi{\cdot}x_{n}$. Suppose $\Phi(\overline{x})$ is a
first-order logic predicate in the language of ZFA666First-order logic with
equality $=$, sets membership $\in$, and a constant or collection of constants
for sets of atoms. with free variables $\overline{x}$. Suppose
$\Upsilon(\overline{x})$ is a function specified using a first-order predicate
in the language of ZFA with free variables $\overline{x}$.

Then we have the following principles:

Equivariance of predicates.
$\Phi(\overline{x})\Leftrightarrow\Phi(\pi{\cdot}\overline{x})$.777It is
important to realise here that $\overline{x}$ must contain _all_ the variables
mentioned in the predicate. It is not the case that $a=a$ if and only if $a=b$
— but it is the case that $a=b$ if and only if $b=a$ (both are false).

Equivariance of functions.
$\pi{\cdot}\Upsilon(\overline{x})=\Upsilon(\pi{\cdot}\overline{x})$.

Conservation of support. If $\overline{x}$ denotes elements with finite
support
then
$\mathit{supp}(\Upsilon(\overline{x}))\subseteq\mathit{supp}(x_{1}){\cup}\cdots{\cup}\mathit{supp}(x_{n})$.

######  Proof 2.9.

See Theorem 4.4, Corollary 4.6, and Theorem 4.7 from [Gab11].

######  Remark 28.

Theorem 27 states that atoms can be permuted in our theorems and lemmas
provided we do so consistently in all parameters. So for instance if we have
proved $\phi(a,b,c)$, then

taking $\pi=(a\,c)$ we also know $\phi(c,b,a)$ and

taking $\pi=(a\,a^{\prime})(b\,b^{\prime})(c\,c^{\prime})$ we also know
$\phi(a^{\prime},b^{\prime},c^{\prime})$, but

we do not necessarily know that we can deduce $\phi(a,b,a)$ (depending on
$\phi$ this may still hold, of course, but not by equivariance since no
permutation takes $(a,b,c)$ to $(a,b,a)$). Equivariance makes explicit a sense
in which atoms have a dual nature: individually, atoms behave like pointers to
themselves,888In the implementation of FM set theory in my PhD thesis [GP01]
this was literally true: I found it convenient to use _Quine atoms_ , meaning
that $a=\\{a\\}$. but collectively they have the flavour of variables ranging
over the set of all atoms via the action of permutations.999This too can be
made precise. See Subsection 2.6 and Lemma 4.17 of [DG12b]. See also the
permutative convention from Definition 7.

We will use Theorem 27 frequently in this paper, either to move permutations
around (parts 1 and 2) or to get ‘free’ bounds on the support of elements
(part 3). ‘Free’ here means ‘from the form of the definition, without having
to verify it by calculations’. Theorem 27 is ‘free’ in the spirit of Wadler’s
marvellously titled _Theorems for free!_ [Wad89].101010Finally, we can be
somewhat more precise about the effort these free equivariance deductions can
save: With equivariance, the cost of deducing
$\phi(\pi{\cdot}x,\pi{\cdot}y,\pi{\cdot}z)$, given a deduction of
$\phi(x,y,z)$, is 1. Without equivariance, the cost of deducing
$\phi(\pi{\cdot}x,\pi{\cdot}y,\pi{\cdot}z)$, given a deduction of
$\phi(x,y,z)$, is roughly $n$ where $n$ is the cost of deducing $\phi(x,y,z)$.
This is convenient in a rigorous but unmechanised proof such as the one in
this paper; in an implementation it can quadratically reduce effort by saving
roughly effort $n$ for each $\phi$. This is the difference between
$\alpha$-equivalence and renaming lemmas being a minor consideration, and them
inflating to dominate the development. My feeling is that once renaming lemmas
consume more than 80% of the developmental effort, development stalls.

Discussions expanding on this remark are in [Gab17] (full paper) and [Gab18]
(abstract).

######  Proposition 29.

$\mathit{supp}(\pi{\cdot}x)=\pi{\cdot}\mathit{supp}(x)$ (which means
$\\{\pi(a)\mid a\in\mathit{supp}(x)\\}$).

$a\text{\tt\\#}\pi{\cdot}x$ (Notation 2.1.4) if and only if
$\pi^{{\text{-}1}}(a)\text{\tt\\#}x$, and $a\text{\tt\\#}x$ if and only if
$\pi(a)\text{\tt\\#}\pi{\cdot}x$.

######  Proof 2.10.

Immediate consequence of part 2 of Theorem 27 (for the ‘not-free’ proof by
concrete calculations see [Gab11, Theorem 2.19]).

##  3\. Internal syntax

###  3.1. Basic definition

######  Remark 30.

We are now ready to to define our syntax (Figure 1) and study its basic
properties (with more advanced properties considered in Section 4).

Figure 1 defines a _nominal_ datatype, in which atoms-abstraction is used to
manage binding, as introduced in [GP01]. This gives us Lemma 33.

Parts 33 and 33 of Lemma 33 say “We can alpha-convert”.

In part 33 of Lemma 33, $\mathit{supp}$ corresponds exactly to the notion that
would normally be written “Free variables of”, and $a\text{\tt\\#}X$
corresponds to “$a$ is not free in $X$”. So why not just write that? Nominal
techniques are a general basket of ideas with implications that go well beyond
modelling syntax, but the specific benefit of using nominal techniques to
model syntax is that we get alpha-conversion for free from the ambient nominal
theory (see [GP01] and Section 2). We do not have to define
$\alpha$-conversion and free variables of by induction, and then prove their
properties (which is actually a more subtle undertaking than is often
realised; cf. Remark 50).

The reader does not expect to see notions of ordered pairs, trees, numbers,
functions, and function application developed from first principles every time
we want to write abstract syntax and write a function on a syntax tree. It is
assumed that these things have been worked out. Nominal techniques do that for
binding (and more).

Write $\mathbb{Z}$ for the integers, so
$\mathbb{Z}=\\{0,1,{\text{-}}1,2,{\text{-}}2,\dots\\}$ and $\mathbb{N}$ for
the natural numbers, which we start at $0$, so $\mathbb{N}=\\{0,1,2,\dots\\}$.

######  Definition 31.

Define datatypes

$\mathsf{Pred}$ of internal predicates and

$\mathsf{Set}^{i}$ for $i{\in}{\mathbb{Z}}$ of internal (level $i$) sets
inductively by the rules in Figure 1, where $\kappa$ ranges over finite
ordinals.

Define

$\begin{array}[]{r@{\ }l@{\quad\text{and}\quad}r@{\
}l}\mathsf{Pred}=&\bigcup_{\kappa}\mathsf{Pred}(\kappa)&\mathsf{Set}^{i}=&\bigcup_{\kappa}\mathsf{Set}^{i}(\kappa).\end{array}$

Write $\mathit{age}(X)$ for the least $\kappa$ such that
$X{\in}\mathsf{Pred}(\kappa)$.

Write $\mathit{age}(x)$ for the least $\kappa$ such that
$x{\in}\mathsf{Set}^{i}(\kappa)$.

$\begin{array}[]{c@{\qquad}c@{\qquad}c}{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 22.46417pt\hbox{$\displaystyle\penalty
1a\in\mathbb{A}^{{i}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=69.08792pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\text{\tt
atm}(a)\in\mathsf{Set}^{i}(\kappa)$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 15.9778pt\hbox{$\displaystyle\penalty
1\mathcal{X}\mathbin{\subseteq_{\text{\it fin}}}\mathsf{Pred}(\kappa)$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=87.87285pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\text{\tt
and}}}(\mathcal{X})\in\mathsf{Pred}(\kappa{\text{+}}1)$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
19.16669pt\hbox{$\displaystyle\penalty 1X{\in}\mathsf{Pred}(\kappa)$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=88.33113pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\text{\tt
neg}}(X)\in\mathsf{Pred}(\kappa{\text{+}}1)$}}}}\\\\[17.22217pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.2854pt\hbox{$\displaystyle\penalty 1X{\in}\mathsf{Pred}(\kappa)\ \
a{\in}\mathbb{A}^{{i}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=91.95042pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\text{\tt
all}}([a]X){\in}\mathsf{Pred}(\kappa{+}1)$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.2707pt\hbox{$\displaystyle\penalty 1a{\in}\mathbb{A}^{{i{+}1}}\ \
x{\in}\mathsf{Set}^{i}(\kappa)$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=90.81837pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\text{\tt
elt}}(x,a)\in\mathsf{Pred}(\kappa{+}1)$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1X{\in}\mathsf{Pred}(\kappa)\ \ a{\in}\mathbb{A}^{{i{\text{-}}1}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=86.04628pt\hbox{}}}\hbox{\kern
0.86108pt\hbox{$\displaystyle\text{\tt
st}([a]X){\in}\mathsf{Set}^{i}(\kappa{\text{+}}1)$}}}}\end{array}$ Figure 1.
Syntax of internal predicates and terms

  * •

If $a{\in}\mathbb{A}$ we may call $\text{\tt atm}(a)$ an internal atom.

  * •

If $X{\in}\mathsf{Pred}$ we may call $\text{\tt st}([a]X)$ an internal
comprehension.

  * •

We may call $\text{\tt atm}(a)$ or $\text{\tt st}([a]X)$ an internal
set.111111So every internal comprehension or internal atom is an internal set.
Another choice of terminology would be to call $\text{\tt atm}(a)$ an internal
atom, $\text{\tt st}([a]X)$ an internal set, and $\text{\tt atm}(a)$ or
$\text{\tt st}([a]X)$ _internal elements_. However, note that $\text{\tt
st}([a]X)$ is not a set and neither is $\text{\tt atm}(a)$; they are both
syntax and we can call them what we like.

######  Remark 32.

We read through and comment on Definition 31:

$\kappa$ measures the _age_ or _stage_ of an element; at what point in the
induction it is introduced into the datatype. This is an inductive measure.

If we elide $\kappa$ and levels and simplify, we can rewrite Definition 31
semi-formally as follows:

$\begin{array}[]{l@{\ }l}x\in\mathsf{Set}&::=\text{\tt atm}(a)\mid\text{\tt
st}([a]X)\\\ X\in\mathsf{Pred}&::={{\text{\tt
and}}}(\mathcal{X})\mid{\text{\tt neg}}(X)\mid{\text{\tt
all}}([a]X)\mid{\text{\tt elt}}(x,a)\end{array}$

neg represents negation. and represents logical conjunction.

and takes a finite set rather than a pair of terms. This is a nonessential
eccentricity that cuts down on cases later on. Truth is represented as
${{\text{\tt and}}}(\varnothing)$. See Example 3.2.

all represents universal quantification; read ${\text{\tt all}}([a]X)$ as ‘for
all $a$, $X$’ or in symbols: ‘$\forall a.\phi$’. In ${\text{\tt all}}([a]X)$,
$[a]X$ is the nominal atoms-abstraction from Definition 20. It implements the
binding of the universal quantifier by the standard nominal method.

${\boldsymbol{\in}}$ represents a sets membership; read ${\text{\tt
elt}}(x,a)$ as ‘$x$ is an element of $a$’. Note here that $a$ is an atom; it
does not literally have any elements. ${\text{\tt elt}}(x,a)$ represents the
predicate ‘we believe that $x$ is an element of the variable $a$’, or in
symbols: ‘$x\in a$’.

$\text{\tt st}([a]X)$ represents sets comprehension; read $\text{\tt
st}([a]X)$ as ‘the set of $a$ such that $X$’ or in symbols: ‘$\\{a\mid X\\}$’.
Again, as standard in nominal techniques, nominal atoms-abstraction is used to
represent the binding.

If $a{\in}\mathbb{A}^{{i}}$ then $\text{\tt
st}([a]X){\in}\mathsf{Set}^{i{+}1}$.

$\text{\tt atm}(a)$ is a copy of $a{\in}\mathbb{A}$ wrapped in some formal
syntax atm.

######  Lemma 33.

Suppose $X{\in}\mathsf{Pred}$ and $i{\in}{\mathbb{Z}}$ and
$a,a^{\prime}{\in}\mathbb{A}^{{i}}$ and $a^{\prime}\text{\tt\\#}X$. Then:

$\text{\tt st}([a]X)=\text{\tt st}([a^{\prime}](a^{\prime}\ a){\cdot}X)$ and
${\text{\tt all}}([a]X)={\text{\tt all}}([a^{\prime}](a^{\prime}\
a){\cdot}X)$.

$a\text{\tt\\#}\text{\tt st}([a]X)$ and $a\text{\tt\\#}{\text{\tt
all}}([a]X)$, and $\mathit{supp}(\text{\tt st}([a]X)),\mathit{supp}({\text{\tt
all}}([a]X))\subseteq\mathit{supp}(X){\setminus}\\{a\\}$.

For every finite $S\mathbin{\subseteq_{\text{\it fin}}}\mathbb{A}^{{i}}$ there
exist $b\in\mathbb{A}^{{i}}{\setminus}S$ and $Y{\in}\mathsf{Pred}$ such that
$\text{\tt st}([a]X)=\text{\tt st}([b]Y)$ and ${\text{\tt
all}}([a]X)={\text{\tt all}}([b]Y)$.

######  Proof 3.1.

Immediate from Lemma 22, and Lemma 21 with Theorem 27.

######  Lemma 34.

Suppose $i{\in}{\mathbb{Z}}$ and $a,b\in\mathbb{A}^{{i}}$ and
$X\in\mathsf{Pred}$ and $x\in\mathsf{Set}$. Then
$\mathit{age}(X)=\mathit{age}((a\ b){\cdot}X)$ and
$\mathit{age}(x)=\mathit{age}((a\ b){\cdot}x)$.

######  Proof 3.2.

Direct from Theorem 27(27).

###  3.2. Some notation

Suppose $X,Y{\in}\mathsf{Pred}$ and $\mathcal{X}\mathbin{\subseteq_{\text{\it
fin}}}\mathsf{Pred}$. Define syntactic sugar ${{\text{\tt or}}}(\mathcal{X})$,
${\text{\tt imp}}(X,Y)$ and ${\text{\tt iff}}(X,Y)$ by

$\begin{array}[]{r@{\ }l}{{\text{\tt or}}}(\mathcal{X})=&{\text{\tt
neg}}(({{\text{\tt and}}}(\\{{\text{\tt neg}}(X)\mid X\in\mathcal{X}\\})))\\\
{\text{\tt imp}}(X,Y)=&{{\text{\tt or}}}(\\{{\text{\tt neg}}(X),Y\\})\\\
{\text{\tt iff}}(X,Y)=&{{\text{\tt and}}}(\\{{\text{\tt imp}}(X,Y),{\text{\tt
imp}}(Y,X)\\}).\end{array}$

Define ${\text{\tt F}}\in\mathsf{Pred}$ and ${\text{\tt T}}\in\mathsf{Pred}$
by

${\text{\tt F}}={{\text{\tt or}}}(\varnothing)\quad\text{and}\quad{\text{\tt
T}}={{\text{\tt and}}}(\varnothing).$

Intuitively, F represents the empty disjunction, and T represents the empty
conjunction.

Suppose that:

$i{\in}{\mathbb{Z}}$ and

$x=\text{\tt st}(x^{\prime}){\in}\mathsf{Set}^{i}$ is an internal
comprehension where $x^{\prime}\in[\mathbb{A}^{{i{\text{-}}1}}]\mathsf{Pred}$
and $a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$ and

$a^{\prime}\text{\tt\\#}x$ (equivalently121212By concrete calculations or by
Theorem 27. $a^{\prime}\text{\tt\\#}x^{\prime}$). Then write

$x\text{@}a^{\prime}\quad\text{for}\quad <EMAIL_ADDRESS>
Lemma 35 checks that Notation 3.2 makes sense:

######  Lemma 35.

Suppose $i{\in}{\mathbb{Z}}$ and $a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$.
Suppose $x{\in}\mathsf{Set}^{i}$ is an internal comprehension and
$a^{\prime}\text{\tt\\#}x$ and $X^{\prime}\in\mathsf{Pred}$. Then:

$x\text{@}a^{\prime}$ is well-defined and
$x\text{@}a^{\prime}\in\mathsf{Pred}$.

$x=\text{\tt st}([a^{\prime}](x\text{@}a^{\prime}))$.

If $\mathit{age}(x)=\kappa{\text{+}}1$ then
$\mathit{age}(x\text{@}a^{\prime})=\kappa$ (meaning that in an inductive
argument using age, taking $x\text{@}a^{\prime}$ strictly decreases the
inductive measure).

$(\text{\tt st}([a^{\prime}]X^{\prime}))\text{@}a^{\prime}=X^{\prime}$.

######  Proof 3.3.

  1. (1)

By construction and Lemma 24.

  2. (2)

By construction and Lemma 25(2).

  3. (3)

By construction and Lemma 34.

  4. (4)

By construction and Lemma 25(1).

Recall ${\text{\tt F}}{=}{{\text{\tt or}}}(\varnothing)$ from Example 3.2.

######  Definition 36.

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i{\text{-}}1}}$. Define
${\text{\tt empt}}^{i}$ and ${\text{\tt set}}^{i}$ by

$\begin{array}[]{r@{\ }l}{\text{\tt empt}}^{i}=&\text{\tt st}([a]{\text{\tt
F}})=\text{\tt st}([a]{{\text{\tt or}}}(\varnothing))\\\ {\text{\tt
set}}^{i}=&\text{\tt st}([a]{\text{\tt T}})=\text{\tt st}([a]{{\text{\tt
and}}}(\varnothing)).\end{array}$

We conclude with an easy lemma:

######  Lemma 37.

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i{\text{-}}1}}$. Then:

${\text{\tt empt}}^{i}\text{@}a={\text{\tt F}}$ and $\text{\tt
st}([a]{\text{\tt F}})={\text{\tt empt}}^{i}$, and similarly ${\text{\tt
set}}^{i}\text{@}a={\text{\tt T}}$ and $\text{\tt st}([a]{\text{\tt
T}})={\text{\tt set}}^{i}$.

$a\text{\tt\\#}{\text{\tt F}}$ and $a\text{\tt\\#}{\text{\tt T}}$.

Definition 36 does not depend on the choice of
$a{\in}\mathbb{A}^{{i{\text{-}}1}}$.

######  Proof 3.4.

From Definition 36 and Lemma 25(1).

From part 1 of this result, since $a\text{\tt\\#}{\text{\tt F}}$ and
$a\text{\tt\\#}{\text{\tt T}}$ by Theorem 27.

From part 2 of this result, using Corollary 15.

##  4\. The sigma-action

###  4.1. Basic definition and well-definedness

Intuitively, Definition 38 defines a substitution action. It is slightly
elaborate, especially because of ${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$ of
Figure 2, so it gets a fancy name (‘$\sigma$-action’) and we need to make
formal and verify that it behaves as a substitution action should; see Remark
43.

######  Definition 38.

Define a $\sigma$-action (sigma-action) to be a family of functions

$\sigma_{i}:\mathsf{Pred}\times\mathbb{A}^{{i}}\times\mathsf{Set}^{i}\to\mathsf{Pred}\quad\text{and}\quad\sigma_{ij}:\mathsf{Set}^{j}\times\mathbb{A}^{{i}}\times\mathsf{Set}^{i}\to\mathsf{Set}^{j}$

where $i,j{\in}{\mathbb{Z}}$, inductively by the rules in Figure 2. For
readability we write

$\sigma_{i}(Z,a,x)\ \text{as}\
Z[a{\mapsto}x]\quad\text{and}\quad\sigma_{i}(z,a,x)\ \text{as}\
z[a{\mapsto}x].$

Furthermore in Figure 2:

In rule ${\mathrm{\bf(\sigma{\text{\tt and}})}}$,
$\mathcal{X}{\mathbin{\subseteq_{\text{\it fin}}}}\mathsf{Pred}$.

In rule ${\mathrm{\bf(\sigma{\text{\tt neg}})}}$, $X{\in}\mathsf{Pred}$.

In rule ${\mathrm{\bf(\sigma{\text{\tt all}})}}$, $X{\in}\mathsf{Pred}$ and
$b{\in}\mathbb{A}^{{j}}$ for some $j{\in}{\mathbb{Z}}$.

In rule ${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$,
$a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$.

In rule ${\mathrm{\bf(\sigma{\text{\tt elt}}\text{\tt atm})}}$, $n$ ranges
over _all_ atoms in $\mathbb{A}^{{i}}$ (not just those distinct from $a$).

In rule ${\mathrm{\bf(\sigma{\text{\tt elt}}b)}}$, $b{\in}\mathbb{A}^{{j}}$
for some $j{\in}{\mathbb{Z}}$.

In rule ${\mathrm{\bf(\sigma{\text{\tt st}})}}$, $X{\in}\mathsf{Pred}$ and
$c{\in}\mathbb{A}^{{k}}$ for some $k{\in}{\mathbb{Z}}$.

$\begin{array}[]{l@{\qquad}l@{\ }r@{\
}l@{\quad}l}{\mathrm{\bf(\sigma{\text{\tt and}})}}&&({{\text{\tt
and}}}(\mathcal{X}))[a{\mapsto}x]=&{{\text{\tt and}}}(\\{X[a{\mapsto}x]\mid
X{\in}\mathcal{X}\\})\\\ {\mathrm{\bf(\sigma{\text{\tt neg}})}}&&({\text{\tt
neg}}(X))[a{\mapsto}x]=&{\text{\tt neg}}((X[a{\mapsto}x]))\\\
{\mathrm{\bf(\sigma{\text{\tt all}})}}&b\text{\tt\\#}x\Rightarrow&({\text{\tt
all}}([b]X))[a{\mapsto}x]=&{\text{\tt all}}([b](X[a{\mapsto}x]))\\\
{\mathrm{\bf(\sigma{\text{\tt elt}}\text{\tt atm})}}&&({\text{\tt
elt}}(y,a))[a{\mapsto}\text{\tt atm}(n)]=&{\text{\tt
elt}}(y[a{\mapsto}\text{\tt atm}(n)],n)\\\ {\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}&&({\text{\tt elt}}(y,a))[a{\mapsto}\text{\tt
st}([a^{\prime}]X^{\prime})]=&X[a^{\prime}{\mapsto}y[a{\mapsto}\text{\tt
st}([a^{\prime}]X^{\prime})]]\\\ {\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}&&({\text{\tt elt}}(y,b))[a{\mapsto}x]=&{\text{\tt
elt}}(y[a{\mapsto}x],b)\\\ {\mathrm{\bf(\sigma a)}}&&\text{\tt
atm}(a)[a{\mapsto}x]=&x\\\ {\mathrm{\bf(\sigma b)}}&&\text{\tt
atm}(b)[a{\mapsto}x]=&\text{\tt atm}(b)\\\ {\mathrm{\bf(\sigma{\text{\tt
st}})}}&c\text{\tt\\#}x\Rightarrow&\text{\tt st}([c]X)[a{\mapsto}x]=&\text{\tt
st}([c](X[a{\mapsto}x]))\end{array}$ Figure 2. The sigma-action (Definition
38)

######  Remark 39.

Figure 2 slips in no fewer than three abuses of the mathematics:

  1. (1)

We do not know that $X\in\mathsf{Pred}$ implies
$X[a{\mapsto}x]\in\mathsf{Pred}$, so we should not write ${{\text{\tt
and}}}(\\{X[a{\mapsto}x]\mid\dots\\})$ on the right-hand side of
${\mathrm{\bf(\sigma{\text{\tt and}})}}$, or indeed $X[a{\mapsto}x]$ on the
right-hand side of ${\mathrm{\bf(\sigma{\text{\tt neg}})}}$, and so on.

In fact, all right-hand sides of Figure 2 are suspect except those of
${\mathrm{\bf(\sigma a)}}$ and ${\mathrm{\bf(\sigma b)}}$.

  2. (2)

We do not know whether the choice of fresh
$a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$ in ${\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}$ matters, so we do not know that ${\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}$ is well-defined.

  3. (3)

The definition looks inductive at first glance, however in the case of
${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$ there is no guarantee that $X$ (on
the right-hand side) is smaller than ${\text{\tt elt}}(y,a)$ (on the left-hand
side). The level of $a^{\prime}$ is strictly lower than the level of $a$,
however levels are taken from ${\mathbb{Z}}$ which is totally ordered but not
well-ordered by $\leq$.

In fact:

  * •

$X\in\mathsf{Pred}$ does indeed imply $X[a{\mapsto}x]\in\mathsf{Pred}$.

  * •

The choice of fresh $a^{\prime}$ in ${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$
is immaterial.

  * •

The levels of atoms involved are bounded below (see Definition 41) so we only
ever work on a well-founded fragment of ${\mathbb{Z}}$.

For proofs see Proposition 42 and Lemma 44.

Would it be more rigorous to interleave the proofs of these lemmas with the
definition, so that at each stage we are confident that what we are writing
actually makes sense? Certainly we could; the reader inclined to worry about
this need only read Definition 38 alongside Proposition 42 and Lemma 44 as a
simultaneous inductive argument.

######  Remark 40 (Why ‘minimum level’).

Levels are in ${\mathbb{Z}}$ and are totally ordered by $\leq$ but not well-
founded (since integers can ‘go downwards forever’).

However, any (finite) internal predicate or internal set can mention only
finitely many levels, so we can calculate the _minimum level_ of a predicate
or set, which is lower bound on the levels of atoms appearing in that
predicate or set. We will use this lower bound to reason inductively on levels
in Propositions 42 and 49.

######  Definition 41.

Define $\mathit{minlevel}(Z)$ and $\mathit{minlevel}(z)$ the minimum level of
$Z$ or $z$, inductively on $Z{\in}\mathsf{Pred}$ and $z{\in}\mathsf{Set}^{i}$
for $i{\in}{\mathbb{Z}}$ as follows:

$\begin{array}[]{l@{\ =\ }l}\mathit{minlevel}(\text{\tt
atm}(a))&\mathit{level}(a)\\\ \mathit{minlevel}({{\text{\tt
and}}}(\mathcal{X}))&\mathit{min}(\\{0\\}\cup\\{\mathit{minlevel}(X)\mid
X{\in}\mathcal{X}\\})\\\ \mathit{minlevel}({\text{\tt
neg}}(X))&\mathit{minlevel}(X)\\\ \mathit{minlevel}({\text{\tt
all}}([a]X))&\mathit{min}(\\{\mathit{level}(a),\mathit{minlevel}(X)\\})\\\
\mathit{minlevel}({\text{\tt
elt}}(x,a))&\mathit{min}(\\{\mathit{minlevel}(x),\mathit{level}(a)\\})\\\
\mathit{minlevel}(\text{\tt
st}([a]X))&\mathit{min}(\\{\mathit{level}(a),\mathit{minlevel}(X)\\})\end{array}$

Above, $\mathit{min}(\mathcal{I})$ is the least element of
$\mathcal{I}\mathbin{\subseteq_{\text{\it fin}}}{\mathbb{Z}}$. We add $0$ in
the clause for and as a ‘default value’ to exclude calculating a minimum for
the empty set; any other fixed integer element would do as well or, if we do
not want to make this choice, we can index $\mathit{minlevel}$ over a fixed
but arbitrary choice. The proofs to follow will not care.

It will be convenient to apply $\mathit{minlevel}$ to a mixed list of internal
predicates, atoms, and internal sets:

  * •

Define $\mathit{minlevel}(a)=\mathit{level}(a)$.

  * •

If $l=(l_{1},l_{2},\dots,l_{n})$ is a list of elements from
$\mathsf{Pred}\cup\bigcup_{i{\in}{\mathbb{Z}}}\mathsf{Set}^{i}\cup\mathbb{A}$
then we write $\mathit{minlevel}(l)$ for the least element of
$\\{\mathit{minlevel}(l_{1}),\dots,\mathit{minlevel}(l_{n})\\}$.

######  Proposition 42.

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i}}$ and
$x{\in}\mathsf{Set}^{i}$.

  1. (1)

If $Z{\in}\mathsf{Pred}$ then

  2. (2)

$Z[a{\mapsto}x]$ is well-defined,

  3. (3)

$\mathit{minlevel}(Z[a{\mapsto}x]){\geq}\mathit{minlevel}(Z,a,x)$, and

  4. (4)

$Z[a{\mapsto}x]{\in}\mathsf{Pred}$.

  5. (5)

If $k{\in}{\mathbb{Z}}$ and $z{\in}\mathsf{Set}^{k}$ then

  6. (6)

$z[a{\mapsto}x]$ is well-defined,

  7. (7)

$\mathit{minlevel}(z[a{\mapsto}x]){\geq}\mathit{minlevel}(z,a,x)$, and

  8. (8)

$z[a{\mapsto}x]{\in}\mathsf{Set}^{k}$.

######  Proof 4.1.

Fix some $k{\in}{\mathbb{Z}}$. We prove the Proposition for all $Z,a,x$ and
$z,a,x$ with $\mathit{minlevel}(Z,a,x){\geq}k$ and
$\mathit{minlevel}(z,a,x){\geq}k$, by induction on

$(\mathit{level}(a),\mathit{age}(Z))\quad\text{and}\quad(\mathit{level}(a),\mathit{age}(z))$

lexicographically ordered. Since $k$ was arbitrary, this suffices to prove it
for all $Z,a,x$ and $z,a,x$.

We consider the possibilities for $Z{\in}\mathsf{Pred}$:

_The case of ${{\text{\tt and}}}(\mathcal{X})$ for
$\mathcal{X}\mathbin{\subseteq_{\text{\it fin}}}\mathsf{Pred}$._

By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt and}})}}$
$Z[a{\mapsto}x]{=}{{\text{\tt
and}}}(\\{X^{\prime}[a{\mapsto}x]{\mid}X^{\prime}{\in}\mathcal{X}\\}).$ We use
the inductive hypothesis on each $X^{\prime}[a{\mapsto}x]$ and some easy
arithmetic calculations.

_The case of ${\text{\tt neg}}(X^{\prime})$ for
$X^{\prime}{\in}\mathsf{Pred}$._

By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt neg}})}}$
$Z[a{\mapsto}x]={\text{\tt neg}}((X^{\prime}[a{\mapsto}x])).$ We use the
inductive hypothesis on $X^{\prime}[a{\mapsto}x]$.

_The case of ${\text{\tt all}}([b]X^{\prime})$ for
$X^{\prime}{\in}\mathsf{Pred}$ and $b{\in}\mathbb{A}^{{j}}$ for some
$j{\in}{\mathbb{Z}}$._

Using Lemma 33(33) we may assume without loss of generality that
$b\text{\tt\\#}x$. By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt all}})}}$
$({\text{\tt all}}([b]X^{\prime}))[a{\mapsto}x]={\text{\tt
all}}([b^{\prime}](X[a{\mapsto}x])).$ We use the inductive hypothesis on
$X^{\prime}[a{\mapsto}x]$.

_The case of ${\text{\tt elt}}(z,a)$ for $z{\in}\mathsf{Set}^{i{\text{-}}1}$._
There are two sub-cases:

  * •

_Suppose $x{=}\text{\tt atm}(n)$ for some $n{\in}\mathbb{A}^{{i}}$._
By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt elt}}\text{\tt atm})}}$
$({\text{\tt elt}}(z,a))[a{\mapsto}x]={\text{\tt elt}}(z[a{\mapsto}\text{\tt
atm}(n)],n).$ We use the inductive hypothesis on $z[a{\mapsto}\text{\tt
atm}(n)]$.

  * •

_Suppose $x{=}\text{\tt st}([a^{\prime}]X^{\prime})$ where
$X^{\prime}=x\text{@}a^{\prime}$ for some fresh
$a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$ (so
$a^{\prime}\text{\tt\\#}x,z$)._
By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$ $({\text{\tt
elt}}(z,a))[a{\mapsto}x]=X^{\prime}[a^{\prime}{\mapsto}z[a{\mapsto}x]].$ We
have the inductive hypothesis on $z[a{\mapsto}x]$. We also have the inductive
hypothesis (since $k{\leq}\mathit{level}(a^{\prime}){=}i{\text{-}}1\lneq
i{=}\mathit{level}(a)$)131313$k$ was chosen no greater than the minimum level
of $Z$, $a$, and $x$. Now $x=\text{\tt st}([a^{\prime}]X^{\prime})$, and it
follows from Definition 41 that $k\leq\mathit{level}(a^{\prime})$. on
$X^{\prime}[a^{\prime}{\mapsto}z[a{\mapsto}x]]$, and this suffices.

_The case of ${\text{\tt elt}}(z,c)$ where $c{\in}\mathbb{A}^{{k}}$ and
$z{\in}\mathsf{Set}^{k{\text{-}}1}$ and $k{\in}{\mathbb{Z}}$._

By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt elt}}b)}}$ and the inductive
hypothesis. We consider the possibilities for $z{\in}\mathsf{Set}^{k}$:

  * •

_The case that $z$ is an internal atom._

We use ${\mathrm{\bf(\sigma a)}}$ or ${\mathrm{\bf(\sigma b)}}$ of Figure 2.

  * •

_The case that $z$ is an internal comprehension._

Choose fresh $c{\in}\mathbb{A}^{{k{\text{-}}1}}$ (so $c\text{\tt\\#}x,z$), so
that by Lemma 35(2) $z=\text{\tt st}([c]z\text{@}c)$. We use the first part of
this result and Figure 2 ${\mathrm{\bf(\sigma{\text{\tt st}})}}$.

###  4.2. Nominal algebraic properties of the sigma-action

######  Remark 43.

Several useful properties of the $\sigma$-action from Definition 38 are
naturally expressed as nominal algebra judgements — equalities subject to
freshness conditions [GM09]. Some are listed for the reader’s convenience in
Figure 3, which goes back to nominal axiomatic studies of substitution from
[GM06, GM08].

In this paper we are dealing with a concrete model, so the judgements in
Figure 3 are not assumed and are not axioms. Instead they must be proved; they
are propositions and lemmas:

${\mathrm{\bf(\sigma\alpha)}}$ is Lemma 44.

${\mathrm{\bf(\sigma\text{\tt\\#})}}$ is Lemma 46.

${\mathrm{\bf(\sigma\sigma)}}$ is Proposition 49.

${\mathrm{\bf(\sigma swp)}}$ and ${\mathrm{\bf(\sigma asc)}}$ are Corollaries
51 and 52.

${\mathrm{\bf(\sigma id)}}$ is Lemma 53.

${\mathrm{\bf(\sigma ren)}}$ is Lemma 54.

${\mathrm{\bf(\sigma\text{@})}}$ is Lemma 48. These are familiar properties of
substitution on syntax: for instance

${\mathrm{\bf(\sigma\alpha)}}$ looks like an $\alpha$-equivalence property —
and indeed it is — and

${\mathrm{\bf(\sigma\text{\tt\\#})}}$ (Lemma 46) is sometimes called _garbage
collection_ and corresponds to the property “if $a$ is not free in $t$ then
$t[a{\mapsto}s]=t$”, and

${\mathrm{\bf(\sigma\sigma)}}$ (Proposition 49) is often called the
_substitution lemma_. See the discussion in Remark 50. But, the proofs of
these properties that we see in this paper are not replays of the familiar
syntactic properties.

This is because the $\sigma$-action on $\mathsf{Pred}$ is not a simple ‘tree-
grafting’ operation — not even a capture-avoiding one — because of
${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$ in Figure 2. The proofs work, but we
cannot take this for granted, and they require checking.

$\begin{array}[]{l@{\qquad}r@{\ }r@{\
}l}{\mathrm{\bf(\sigma\alpha)}}&b^{\prime}\text{\tt\\#}Z\Rightarrow&Z[b{\mapsto}y]=&((b^{\prime}\
b){\cdot}Z)[b^{\prime}{\mapsto}y]\\\
{\mathrm{\bf(\sigma\text{\tt\\#})}}&b\text{\tt\\#}Z\Rightarrow&Z[b{\mapsto}y]=&Z\\\
{\mathrm{\bf(\sigma\sigma)}}&a\text{\tt\\#}y\Rightarrow&Z[a{\mapsto}x][b{\mapsto}y]=&Z[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]]\\\
{\mathrm{\bf(\sigma swp)}}&a\text{\tt\\#}y,\
b\text{\tt\\#}x\Rightarrow&Z[a{\mapsto}x][b{\mapsto}y]=&Z[b{\mapsto}y][a{\mapsto}x]\\\
{\mathrm{\bf(\sigma asc)}}&a\text{\tt\\#}y,\
b\text{\tt\\#}Z\Rightarrow&Z[a{\mapsto}x[b{\mapsto}y]]=&Z[a{\mapsto}x][b{\mapsto}y]\\\
{\mathrm{\bf(\sigma id)}}&&Z[a{\mapsto}\text{\tt atm}(a)]=&Z\\\
{\mathrm{\bf(\sigma
ren)}}&a^{\prime}\text{\tt\\#}Z\Rightarrow&Z[a{\mapsto}\text{\tt
atm}(a^{\prime})]=&(a^{\prime}\ a){\cdot}Z\\\
{\mathrm{\bf(\sigma\text{@})}}&c\text{\tt\\#}x\Rightarrow&(z\text{@}c)[a{\mapsto}x]=&z[a{\mapsto}x]\text{@}c\end{array}$
Figure 3. Further nominal algebra properties of the $\sigma$-action

####  4.2.1. Alpha-equivalence of the sigma-action

######  Lemma 44 (${\mathrm{\bf(\sigma\alpha)}}$).

Suppose $i{\in}{\mathbb{Z}}$ and $a,a^{\prime}{\in}\mathbb{A}^{{i}}$ and
$x{\in}\mathsf{Set}^{i}$. Suppose $Z{\in}\mathsf{Pred}$ and
$a^{\prime}\text{\tt\\#}Z$ and $z{\in}\mathsf{Set}^{k}$ and
$a^{\prime}\text{\tt\\#}z$. Then:

$Z[a{\mapsto}x]=((a^{\prime}\ a){\cdot}Z)[a^{\prime}{\mapsto}x]$ and
$z[a{\mapsto}x]=((a^{\prime}\ a){\cdot}z)[a^{\prime}{\mapsto}x]$.

$\mathit{supp}(Z[a{\mapsto}x])\subseteq(\mathit{supp}(Z){\setminus}\\{a\\})\cup\mathit{supp}(x)$
and
$\mathit{supp}(z[a{\mapsto}x])\subseteq(\mathit{supp}(z){\setminus}\\{a\\})\cup\mathit{supp}(x)$.

If $a\text{\tt\\#}x$ then $a\text{\tt\\#}Z[a{\mapsto}x]$ and
$a\text{\tt\\#}z[a{\mapsto}x]$.

######  Proof 4.2.

By induction on

$\mathit{age}(Z)\quad\text{and}\quad\mathit{age}(z).$

We consider the possibilities for $Z{\in}\mathsf{Pred}$:

  * •

_The case of ${{\text{\tt and}}}(\mathcal{X})$ for
$\mathcal{X}\mathbin{\subseteq_{\text{\it fin}}}\mathsf{Pred}$._ By Lemma 19
$a\text{\tt\\#}X^{\prime}$ for every $X^{\prime}{\in}\mathcal{X}$, so by the
inductive hypothesis $X^{\prime}[a{\mapsto}x]=((a^{\prime}\
a){\cdot}X^{\prime})[a^{\prime}{\mapsto}x]$. We use Figure 2
${\mathrm{\bf(\sigma{\text{\tt and}})}}$ and Theorem 27.

  * •

_The case of ${\text{\tt neg}}(X)$ for $X{\in}\mathsf{Pred}$._ By Figure 2
${\mathrm{\bf(\sigma{\text{\tt neg}})}}$ and the inductive hypothesis for $X$.

  * •

_The case of ${\text{\tt all}}([b]X)$ for $X{\in}\mathsf{Pred}$ and
$b{\in}\mathbb{A}^{{j}}$ for some $j{\in}{\mathbb{Z}}$._ Using Lemma 33(33) we
may assume without loss of generality that $b\text{\tt\\#}x$. We use Figure 2
${\mathrm{\bf(\sigma{\text{\tt all}})}}$ and the inductive hypothesis.

  * •

_The case of ${\text{\tt elt}}(y,a)$ for some
$y{\in}\mathsf{Set}^{i{\text{-}}1}$._ There are two sub-cases:

    * –

_Suppose $x{=}\text{\tt atm}(n)$ for some $n{\in}\mathbb{A}^{{i}}$._ We reason
as follows:

$\begin{array}[]{r@{\ }l@{\quad}l}({\text{\tt elt}}(y,a))[a{\mapsto}\text{\tt
atm}(n)]=&{\text{\tt elt}}(y[a{\mapsto}\text{\tt
atm}(n)],n)&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&{\text{\tt elt}}(((a^{\prime}\
a){\cdot}y)[a^{\prime}{\mapsto}\text{\tt atm}(n)],n)&\text{Ind hyp for $y$}\\\
=&({\text{\tt elt}}(((a^{\prime}\
a){\cdot}y),a^{\prime}))[a^{\prime}{\mapsto}\text{\tt
atm}(n)]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&((a^{\prime}\ a){\cdot}({\text{\tt
elt}}(y,a)))[a^{\prime}{\mapsto}\text{\tt
atm}(n)]&\text{Theorem~{}\ref{thrm.equivar}}\end{array}$

    * –

_Suppose $x{=}\text{\tt st}([b^{\prime}]X^{\prime})$ where
$X^{\prime}=x\text{@}b^{\prime}$ for some fresh
$b^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$ (so
$b^{\prime}\text{\tt\\#}x,y,z$)._
We reason as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(y,a))[a{\mapsto}x]=&X^{\prime}[b^{\prime}{\mapsto}y[a{\mapsto}x]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\\\ =&X^{\prime}[b^{\prime}{\mapsto}((a^{\prime}\
a){\cdot}y)[a^{\prime}{\mapsto}x]]&\text{Ind hyp for $y$}\\\ =&({\text{\tt
elt}}((a^{\prime}\
a){\cdot}y,a^{\prime}))[a^{\prime}{\mapsto}x]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\end{array}$

  * •

_The case ${\text{\tt elt}}(y,b)$ for $j{\in}{\mathbb{Z}}$ and
$b{\in}\mathbb{A}^{{j}}$ and $y{\in}\mathsf{Set}^{j{\text{-}}1}$._ We reason
as follows:

$\begin{array}[]{r@{\ }l@{\quad}l}({\text{\tt
elt}}(y,b))[a{\mapsto}x]=&{\text{\tt
elt}}(y[a{\mapsto}x],b)&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&{\text{\tt elt}}(((a^{\prime}\
a){\cdot}y)[a^{\prime}{\mapsto}x],b)&\text{Ind hyp for $y$}\\\ =&({\text{\tt
elt}}(((a^{\prime}\
a){\cdot}y),b))[a^{\prime}{\mapsto}x]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&((a^{\prime}\ a){\cdot}({\text{\tt
elt}}(y,b)))[a^{\prime}{\mapsto}x]&\text{Theorem~{}\ref{thrm.equivar}}\end{array}$

We consider the possibilities for $z{\in}\mathsf{Set}^{k}$:

  * •

_The case that $z$ is an internal atom._ We use ${\mathrm{\bf(\sigma a)}}$ or
${\mathrm{\bf(\sigma b)}}$ of Figure 2.

  * •

_The case that $z$ is an internal comprehension._ We use Lemma 35(2&3) for a
fresh $c{\in}\mathbb{A}^{{k{\text{-}}1}}$ (so $c\text{\tt\\#}z$),
${\mathrm{\bf(\sigma{\text{\tt st}})}}$, and the inductive hypothesis.

For part 2, we note that by Theorem 27 and Proposition 29

$\begin{array}[]{r@{\
}l}\mathit{supp}(Z[a{\mapsto}x])\subseteq&\mathit{supp}(Z)\cup\\{a\\}\cup\mathit{supp}(x)\quad\text{and}\\\
\mathit{supp}(((a^{\prime}\
a){\cdot}Z)[a^{\prime}{\mapsto}x])\subseteq&(a^{\prime}\
a){\cdot}\mathit{supp}(Z)\cup\\{a^{\prime}\\}\cup\mathit{supp}(x).\end{array}$

We take a sets intersection. The case of $z$ is similar.

Part 3 follows, recalling from Notation 2.1.4 that $a\text{\tt\\#}x$ means
$a{\not\in}\mathit{supp}(x)$.

######  Remark 45.

_Note for experts:_ We could set Definition 38 up differently: we could have
$\sigma_{i}$ and $\sigma_{ij}$ input abstractions

$\sigma_{i}:([\mathbb{A}^{{i}}]\mathsf{Pred})\times\mathsf{Set}^{i}\to\mathsf{Pred}\quad\text{and}\quad\sigma_{ij}:([\mathbb{A}^{{i}}]\mathsf{Set}^{j})\times\mathsf{Set}^{i}\to\mathsf{Set}^{j}.$

Then Lemma 44 would become immediate from Lemmas 21 and 22 and Theorem 27.
This is nice but note that we incur a well-definedness proof-obligation that
the choice of name for the abstracted atom does not matter. There is probably
still a net gain but it is not quite as great as it might first seem. For this
reason, we use the more elementary set-up in Definition 38.

####  4.2.2. Property ${\mathrm{\bf(\sigma\text{\tt\\#})}}$ (garbage
collection)

######  Lemma 46 (${\mathrm{\bf(\sigma\text{\tt\\#})}}$).

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i}}$ and
$x{\in}\mathsf{Set}^{i}$ and $Z{\in}\mathsf{Pred}$ and
$z{\in}\mathsf{Set}^{k}$ for $k{\in}{\mathbb{Z}}$. Then

$\begin{array}[]{l@{\ }r@{\ }l}a\text{\tt\\#}Z\Rightarrow&Z[a{\mapsto}x]=&Z\\\
a\text{\tt\\#}z\Rightarrow&z[a{\mapsto}x]=&z.\end{array}$

######  Proof 4.3.

By induction on

$\mathit{age}(Z)\quad\text{and}\quad\mathit{age}(z).$

We consider the possibilities for $Z{\in}\mathsf{Pred}$:

_The case of ${{\text{\tt and}}}(\mathcal{X})$ for
$\mathcal{X}\mathbin{\subseteq_{\text{\it fin}}}\mathsf{Pred}$._

By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt and}})}}$ $({{\text{\tt
and}}}(\mathcal{X}))[a{\mapsto}x]={{\text{\tt and}}}(\\{X[a{\mapsto}x]\mid
X{\in}\mathcal{X}\\})$. By Lemma 19(19) $a\text{\tt\\#}X$ for every
$X{\in}\mathcal{X}$. We use the inductive hypothesis on each $X$.

_The case of ${\text{\tt neg}}(X)$ for $X{\in}\mathsf{Pred}$._

By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt neg}})}}$ ${\text{\tt
neg}}(X)[a{\mapsto}x]={\text{\tt neg}}(X[a{\mapsto}x])$. We use the inductive
hypothesis on $X$.

_The case of ${\text{\tt all}}([b]X)$ for $X{\in}\mathsf{Pred}$ and
$b{\in}\mathbb{A}^{{j}}$ for some $j{\in}{\mathbb{Z}}$._

Using Lemma 33(33) we may assume without loss of generality that
$b\text{\tt\\#}x$. By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt all}})}}$
$({\text{\tt all}}([b]X))[a{\mapsto}x]={\text{\tt all}}([b](X[a{\mapsto}x]))$.
We use the inductive hypothesis on $X$.

_The case of ${\text{\tt elt}}(y,a)$ for $i{\in}{\mathbb{Z}}$ and
$y{\in}\mathsf{Set}^{i{\text{-}}1}$._

This is impossible because we assumed $a\text{\tt\\#}Z$.

_The case of ${\text{\tt elt}}(y,b)$ for $j{\in}{\mathbb{Z}}$ and
$b{\in}\mathbb{A}^{{j}}$ and $y{\in}\mathsf{Set}^{j{\text{-}}1}$._

By Figure 2 ${\mathrm{\bf(\sigma{\text{\tt elt}}b)}}$ $({\text{\tt
elt}}(y,b))[a{\mapsto}x]={\text{\tt elt}}(y[a{\mapsto}x],b)$. We use the
inductive hypothesis on $y$. We consider the possibilities for
$z{\in}\mathsf{Set}^{k}$:

  * •

If $z$ is an internal atom then we reason using ${\mathrm{\bf(\sigma a)}}$ or
${\mathrm{\bf(\sigma b)}}$ of Figure 2.

  * •

If $z$ is an internal comprehension then we use Lemma 35(2&3) for a fresh
$c{\in}\mathbb{A}^{{k{\text{-}}1}}$ (so $c\text{\tt\\#}z$),
${\mathrm{\bf(\sigma{\text{\tt st}})}}$, and the inductive hypothesis.

Recall ${\text{\tt F}}{=}{{\text{\tt or}}}(\varnothing)$ and ${\text{\tt
T}}{=}{{\text{\tt and}}}(\varnothing)$ from Example 3.2. Corollary 47 is an
easy consequence of Lemma 46 and will be useful later:

######  Corollary 47.

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i}}$ and
$x{\in}\mathsf{Set}^{i}$. Then

${\text{\tt F}}[a{\mapsto}x]={\text{\tt F}}\quad\text{and}\quad{\text{\tt
T}}[a{\mapsto}x]={\text{\tt T}}.$

######  Proof 4.4.

By Theorem 27 $\mathit{supp}({\text{\tt F}}){=}\varnothing$ so that
$a\text{\tt\\#}x$. We use Lemma 46. Similarly for T.

####  4.2.3. $\sigma$ commutes with atoms-concretion

Lemma 48 will be useful later, starting with Proposition 49:

######  Lemma 48 (${\mathrm{\bf(\sigma\text{@})}}$).

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i}}$ and
$x{\in}\mathsf{Set}^{i}$. Suppose $k{\in}{\mathbb{Z}}$ and
$z\in\mathsf{Set}^{k}$ is an internal comprehension and
$c{\in}\mathbb{A}^{{k{\text{-}}1}}$ and $c\text{\tt\\#}z,x$. Then

$(z\text{<EMAIL_ADDRESS>
($z\text{@}c$ is from Notation 3.2.)

######  Proof 4.5.

By Lemma 35(2) we may write $z=\text{\tt st}([c]Z)$ where $Z=z\text{@}c$. We
reason as follows:

$\displaystyle\begin{array}[b]{r@{\
}l@{\qquad}l}(z\text{@}c)[a{\mapsto}x]=&Z[a{\mapsto}x]&Z=z\text{@}c\\\
=&\text{\tt
st}([c](Z[a{\mapsto}x]))\text{@}c&\text{Lemma~{}\ref{lemm.conc.set}(2)}\\\
=&(\text{\tt
st}([c]Z)[a{\mapsto}x])\text{@}c&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
st}})}},c\text{\tt\\#}x\\\ =&(z[a{\mapsto}x])\text{@}c&z=\text{\tt
st}([c]Z)\end{array}$

####  4.2.4. $\sigma$ commutes with itself: the ‘substitution lemma’

######  Proposition 49.

Suppose $Z{\in}\mathsf{Pred}$ and $k{\in}{\mathbb{Z}}$ and
$z{\in}\mathsf{Set}^{k}$. Suppose $i{\in}{\mathbb{Z}}$ and
$a{\in}\mathbb{A}^{{i}}$ and $x{\in}\mathsf{Set}^{i}$ and suppose
$j{\in}{\mathbb{Z}}$ and $b{\in}\mathbb{A}^{{j}}$ and $y{\in}\mathsf{Set}^{j}$
and $a\text{\tt\\#}y$. Then

$\begin{array}[]{r@{\
}l}Z[a{\mapsto}x][b{\mapsto}y]=&Z[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]]\\\
z[a{\mapsto}x][b{\mapsto}y]=&z[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]].\end{array}$

######  Proof 4.6.

For brevity we may write

$\sigma\text{ for
}[a{\mapsto}x][b{\mapsto}y]\quad\text{and}\quad\sigma^{\prime}\text{ for
}[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]].$

Fix some $k{\in}{\mathbb{Z}}$. We prove the Lemma for all $Z,a,x,b,y$ and
$z,a,x,b,y$ with $\mathit{minlevel}(Z,a,x,b,y){\geq}k$ and
$\mathit{minlevel}(z,a,x,b,y){\geq}k$ (Definition 41), reasoning by induction
on

$(\mathit{level}(a){+}\mathit{level}(b),\mathit{age}(Z))\quad\text{and}\quad(\mathit{level}(a){+}\mathit{level}(b),\mathit{age}(z))$

lexicographically ordered. Since $k$ was arbitrary, this suffices to prove it
for all $Z,a,x,b,y$ and $z,a,x,b,y$.

We consider the possibilities for $Z{\in}\mathsf{Pred}$:

  * •

_The case of ${{\text{\tt and}}}(\mathcal{X})$ for
$\mathcal{X}\mathbin{\subseteq_{\text{\it fin}}}\mathsf{Pred}$._ We use rule
${\mathrm{\bf(\sigma{\text{\tt and}})}}$ of Figure 2 and the inductive
hypothesis.

  * •

_The case of ${\text{\tt neg}}(X)$ for $X{\in}\mathsf{Pred}$._ We use
${\mathrm{\bf(\sigma{\text{\tt neg}})}}$ of Figure 2 and the inductive
hypothesis.

  * •

_The case of ${\text{\tt all}}([a^{\prime}]X)$ for $X{\in}\mathsf{Pred}$ and
$a^{\prime}{\in}\mathbb{A}^{{i^{\prime}}}$ for some
$i^{\prime}{\in}{\mathbb{Z}}$._ We use Lemma 33(33) to assume without loss of
generality that $a^{\prime}\text{\tt\\#}x,y$, and then we use
${\mathrm{\bf(\sigma{\text{\tt all}})}}$ of Figure 2 and the inductive
hypothesis.

  * •

_The case of ${\text{\tt elt}}(z,b)$ for $z{\in}\mathsf{Set}^{j{\text{-}}1}$
where $j{\in}{\mathbb{Z}}$._ There are two sub-cases:

    * –

_Suppose $y{=}\text{\tt atm}(n)$ for some $n{\in}\mathbb{A}^{{i}}$ other than
$a$_ (we assumed $a\text{\tt\\#}y$ so $n{=}a$ is impossible).

We reason as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,b))&[a{\mapsto}x][b{\mapsto}\text{\tt atm}(n)]\\\ =&({\text{\tt
elt}}(z[a{\mapsto}x],b))[b{\mapsto}\text{\tt
atm}(n)]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&{\text{\tt
elt}}(z\sigma,n)&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&{\text{\tt elt}}(z\sigma^{\prime},n)&\text{IH
}\mathit{age}(z){<}\mathit{age}({\text{\tt elt}}(z,b)),\ a\text{\tt\\#}y\\\
=&({\text{\tt elt}}(z[b{\mapsto}\text{\tt
atm}(n)],n))[a{\mapsto}x[b{\mapsto}\text{\tt
atm}(n)]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&({\text{\tt elt}}(z,b))[b{\mapsto}\text{\tt
atm}(n)][a{\mapsto}x[b{\mapsto}\text{\tt
atm}(n)]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\end{array}$

    * –

_Suppose $y{=}\text{\tt st}([b^{\prime}]Y^{\prime})$ where
$Y^{\prime}=y\text{@}b^{\prime}$ for some fresh
$b^{\prime}{\in}\mathbb{A}^{{j{\text{-}}1}}$ (so
$b^{\prime}\text{\tt\\#}z,x,y$ and $k{\leq}\mathit{level}(b^{\prime})$)._

Note by Theorem 27 that $a\text{\tt\\#}Y^{\prime}$ and
$b^{\prime}\text{\tt\\#}x[b{\mapsto}y]$. We reason as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,b))&[a{\mapsto}x][b{\mapsto}y]\\\ =&({\text{\tt
elt}}(z[a{\mapsto}x],b))[b{\mapsto}y]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\
=&Y^{\prime}[b^{\prime}{\mapsto}z\sigma]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\\\ =&Y^{\prime}[b^{\prime}{\mapsto}z\sigma^{\prime}]&\text{IH
}\mathit{age}(z){<}\mathit{age}({\text{\tt elt}}(z,b)),\ a\text{\tt\\#}y\\\
=&Y^{\prime}[a{\mapsto}x[b{\mapsto}y]][b^{\prime}{\mapsto}z\sigma^{\prime}]&\text{Lemma~{}\ref{lemm.sigma.hash.always}},\
a\text{\tt\\#}Y^{\prime}\\\
=&Y^{\prime}[b^{\prime}{\mapsto}z[b{\mapsto}y]]\,[a{\mapsto}x[b{\mapsto}y]]&\text{IH
}\mathit{level}(b^{\prime}){<}\mathit{level}(b),\
b^{\prime}\text{\tt\\#}x[b{\mapsto}y]\\\ =&({\text{\tt
elt}}(z,b))[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\end{array}$

  * •

_The case of ${\text{\tt elt}}(z,a)$ for $z{\in}\mathsf{Set}^{i{\text{-}}1}$
where $i{\in}{\mathbb{Z}}$._ There are two sub-cases:

    * –

_Suppose $x{=}\text{\tt atm}(n)$ for some $n{\in}\mathbb{A}^{{i}}$._

If $n{\neq}b$ then we reason as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,a))&[a{\mapsto}\text{\tt atm}(n)][b{\mapsto}y]\\\ =&({\text{\tt
elt}}(z[a{\mapsto}\text{\tt
atm}(n)],n))[b{\mapsto}y]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&{\text{\tt
elt}}(z\sigma,n)&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&{\text{\tt elt}}(z\sigma^{\prime},n)&\text{IH
}\mathit{age}(z){<}\mathit{age}({\text{\tt elt}}(z,a)),\ a\text{\tt\\#}y\\\
=&{\text{\tt elt}}(z[b{\mapsto}y][a{\mapsto}\text{\tt
atm}(n)],n)&{\mathrm{\bf(\sigma b)}}\ n{\neq}b\\\ =&({\text{\tt
elt}}(z[b{\mapsto}y],a))[a{\mapsto}\text{\tt
atm}(n)]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&({\text{\tt
elt}}(z[b{\mapsto}y],a))[a{\mapsto}\text{\tt
atm}(n)[b{\mapsto}y]]&{\mathrm{\bf(\sigma b)}}\ n{\neq}b\\\ =&({\text{\tt
elt}}(z,a))[b{\mapsto}y][a{\mapsto}\text{\tt
atm}(n)[b{\mapsto}y]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\end{array}$

If $n{=}b$ so that $x{=}\text{\tt atm}(b)$, and $y{=}\text{\tt atm}(m)$ for
some $m{\in}\mathbb{A}^{{j}}$ other than $a$, then we reason as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,a))&[a{\mapsto}\text{\tt atm}(b)][b{\mapsto}\text{\tt atm}(m)]\\\
=&({\text{\tt elt}}(z[a{\mapsto}\text{\tt atm}(b)],b))[b{\mapsto}\text{\tt
atm}(m)]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&{\text{\tt elt}}(z[a{\mapsto}\text{\tt
atm}(b)][b{\mapsto}\text{\tt
atm}(m)],m)&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&{\text{\tt elt}}(z[b{\mapsto}\text{\tt
atm}(m)][a{\mapsto}\text{\tt atm}(b)[b{\mapsto}\text{\tt atm}(m)]],m)&\text{IH
}\mathit{age}(z){<}\mathit{age}({\text{\tt elt}}(z,a)),\ a\text{\tt\\#}m\\\
=&({\text{\tt elt}}(z[b{\mapsto}\text{\tt atm}(m)],m))[a{\mapsto}\text{\tt
atm}(b)[b{\mapsto}\text{\tt
atm}(m)]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&({\text{\tt elt}}(z,b))[b{\mapsto}\text{\tt
atm}(m)][a{\mapsto}\text{\tt atm}(b)[b{\mapsto}\text{\tt
atm}(m)]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\end{array}$

If $n{=}b$ so that $x{=}\text{\tt atm}(b)$, and $y{=}\text{\tt
st}([b^{\prime}]Y^{\prime})$ where $Y^{\prime}=y\text{@}b^{\prime}$ for some
fresh $b^{\prime}{\in}\mathbb{A}^{{j{\text{-}}1}}$ (so
$b^{\prime}\text{\tt\\#}z,n,y$ and $k{\leq}\mathit{level}(b^{\prime})$) then
we reason as follows (note by Theorem 27 that $a\text{\tt\\#}Y^{\prime}$ and
$b^{\prime}\text{\tt\\#}x[b{\mapsto}y]$):

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,a))&[a{\mapsto}\text{\tt atm}(b)][b{\mapsto}y]\\\ =&({\text{\tt
elt}}(z[a{\mapsto}\text{\tt
atm}(b)],b))[b{\mapsto}y]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\
=&Y^{\prime}[b^{\prime}{\mapsto}z\sigma]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\\\ =&Y^{\prime}[b^{\prime}{\mapsto}z\sigma^{\prime}]&\text{IH
}\mathit{age}(z){<}\mathit{age}({\text{\tt elt}}(z,a)),\ a\text{\tt\\#}y\\\
=&Y^{\prime}[a{\mapsto}\text{\tt
atm}(b)[b{\mapsto}y]][b^{\prime}{\mapsto}z\sigma^{\prime}]&\text{Lemma~{}\ref{lemm.sigma.hash.always}},\
a\text{\tt\\#}Y^{\prime}\\\
=&Y^{\prime}[b^{\prime}{\mapsto}z[b{\mapsto}y]][a{\mapsto}\text{\tt
atm}(b)[b{\mapsto}y]]&\text{IH
}\mathit{level}(b^{\prime}){<}\mathit{level}(b),\
b^{\prime}\text{\tt\\#}x[b{\mapsto}y]\\\ =&({\text{\tt
elt}}(z,a))[b{\mapsto}y][a{\mapsto}\text{\tt
atm}(b)[b{\mapsto}y]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\end{array}$

    * –

_Suppose $x{=}\text{\tt st}([a^{\prime}]X^{\prime})$ where
$X^{\prime}=x\text{@}a^{\prime}$ for some fresh
$a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$ (so
$a^{\prime}\text{\tt\\#}z,x,y$ and $k{\leq}\mathit{level}(a^{\prime})$)._

We reason as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,a))[a{\mapsto}x][b{\mapsto}y]=&X^{\prime}[a^{\prime}{\mapsto}z[a{\mapsto}x]]\,[b{\mapsto}y]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\\\ =&X^{\prime}[b{\mapsto}y][a^{\prime}{\mapsto}z\sigma]&\text{IH
}k{\leq}\mathit{level}(a^{\prime}){=}\mathit{level}(a){\text{-}}1,\
a^{\prime}\text{\tt\\#}y\\\
=&X^{\prime}[b{\mapsto}y][a^{\prime}{\mapsto}z\sigma^{\prime}]&\text{IH
}\mathit{age}(z){<}\mathit{age}({\text{\tt elt}}(z,a)),\ a\text{\tt\\#}y\\\
=&(x[b{\mapsto}y]\text{@}a^{\prime})[a^{\prime}{\mapsto}z\sigma^{\prime}]&\text{Lemma~{}\ref{lemm.sigma.at.b}},\
a^{\prime}\text{\tt\\#}y\\\ =&({\text{\tt
elt}}(z[b{\mapsto}y],a))[a{\mapsto}x[b{\mapsto}y]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\\\ =&({\text{\tt
elt}}(z,a))[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}},\ a\text{\tt\\#}y\end{array}$

  * •

_The case of ${\text{\tt elt}}(z,c)$ for $k{\in}{\mathbb{Z}}$ and
$c{\in}\mathbb{A}^{{k}}$ and $z{\in}\mathsf{Set}^{k{\text{-}}1}$._ We reason
as follows:

$\begin{array}[]{@{\hspace{-2em}}r@{\ }l@{\quad}l}({\text{\tt
elt}}(z,c))[a{\mapsto}x][b{\mapsto}y]=&{\text{\tt
elt}}(z\sigma,c)&\text{\text{Figure~{}\ref{fig.sub}}
${\mathrm{\bf(\sigma{\text{\tt elt}}b)}}$, twice}\\\ =&{\text{\tt
elt}}(z\sigma^{\prime},c)&\text{IH }\mathit{age}(z){<}\mathit{age}({\text{\tt
elt}}(z,a)),\ a\text{\tt\\#}y\\\ =&({\text{\tt
elt}}(z,c))[b{\mapsto}y][a{\mapsto}x[b{\mapsto}y]]&\text{\text{Figure~{}\ref{fig.sub}}
${\mathrm{\bf(\sigma{\text{\tt elt}}b)}}$, twice}\end{array}$

We consider the possibilities for $z{\in}\mathsf{Set}^{k}$:

  * •

If $z$ is an internal atom then we reason using ${\mathrm{\bf(\sigma a)}}$ and
${\mathrm{\bf(\sigma b)}}$ of Figure 2.

  * •

If $z$ is an internal comprehension then we use Lemma 35(2&3) for a fresh
$c{\in}\mathbb{A}^{{k{\text{-}}1}}$ (so $c\text{\tt\\#}z$),
${\mathrm{\bf(\sigma{\text{\tt st}})}}$, and the inductive hypothesis.

######  Remark 50.

Were Proposition 49 about the syntax of first-order logic or the
$\lambda$-calculus, then it could be called _the substitution lemma_ , and the
proof would be a routine induction on syntax.

In fact, even in the case of first-order logic or the $\lambda$-calculus, the
proof is not routine. Issues with binders (Figure 2
${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$, and one explicit in
${\mathrm{\bf(\sigma{\text{\tt st}})}}$) were the original motivation for my
thesis [Gab01] and for nominal techniques in general.

For a standard non-rigorous non-nominal proof of the substitution lemma see
[Bar84]; for a detailed discussion of the lemma in the context of Nominal
Isabelle, see [Bar14] which includes many further references.

But the proof of Proposition 49 is not just a replay of the proofs; neither in
the ‘classic’ sense of [Bar84] nor in the ‘nominal’ sense of [Gab01, Bar14].
This is because of the interaction of elt with the $\sigma$-action, mostly
because of ${\mathrm{\bf(\sigma{\text{\tt elt}}a)}}$ (to a lesser extent also
because of the nominal binder ${\mathrm{\bf(\sigma{\text{\tt st}})}}$).

######  Corollary 51 (${\mathrm{\bf(\sigma swp)}}$).

Suppose $Z{\in}\mathsf{Pred}$ and $k{\in}{\mathbb{Z}}$ and
$z{\in}\mathsf{Set}^{k}$. Suppose $i{\in}{\mathbb{Z}}$ and
$a{\in}\mathbb{A}^{{i}}$ and $x{\in}\mathsf{Set}^{i}$ and suppose
$j{\in}{\mathbb{Z}}$ and $b{\in}\mathbb{A}^{{j}}$ and
$y{\in}\mathsf{Set}^{j}$. Suppose $a\text{\tt\\#}y$ and $b\text{\tt\\#}x$.
Then

$\begin{array}[]{r@{\
}l}Z[a{\mapsto}x][b{\mapsto}y]=&Z[b{\mapsto}y][a{\mapsto}x]\\\
z[a{\mapsto}x][b{\mapsto}y]=&z[b{\mapsto}y][a{\mapsto}x].\end{array}$

######  Proof 4.7.

From Proposition 49 and Lemma 46.

######  Corollary 52 (${\mathrm{\bf(\sigma asc)}}$).

Suppose $Z{\in}\mathsf{Pred}$ and $k{\in}{\mathbb{Z}}$ and
$z{\in}\mathsf{Set}^{k}$. Suppose $i{\in}{\mathbb{Z}}$ and
$a{\in}\mathbb{A}^{{i}}$ and $x{\in}\mathsf{Set}^{i}$ and suppose
$j{\in}{\mathbb{Z}}$ and $b{\in}\mathbb{A}^{{j}}$ and
$y{\in}\mathsf{Set}^{j}$. Suppose $a\text{\tt\\#}y$ and
$b\text{\tt\\#}Z,z$.141414We expect a stronger version of Corollary 52 to be
possible in which we do not assume $a\text{\tt\\#}y$. However, the proof would
require an induction resembling the proof of Proposition 49 — the proof
assuming $a\text{\tt\\#}y$ can piggyback on the induction already given in
Proposition 49. We will not need this stronger version, so we do not bother.
Then

$\begin{array}[]{r@{\
}l}Z[a{\mapsto}x[b{\mapsto}y]]=&Z[a{\mapsto}x][b{\mapsto}y]\\\
z[a{\mapsto}x[b{\mapsto}y]]=&z[a{\mapsto}x][b{\mapsto}y].\end{array}$

######  Proof 4.8.

From Proposition 49 and Lemma 46.

####  4.2.5. ${\mathrm{\bf(\sigma id)}}$: substitution for atoms and its
corollaries

We called $\text{\tt atm}(a)$ in Definition 31 an _internal atom_. Atoms in
nominal techniques interpet variables, so if we call $\text{\tt atm}(a)$ an
internal atom this should suggest that $\text{\tt atm}(a)$ should behave like
a variable (or a variable symbol). Rules ${\mathrm{\bf(\sigma a)}}$ and
${\mathrm{\bf(\sigma b)}}$ from Figure 2 are consistent with that, and Lemma
53 makes formal more of this intuition:

######  Lemma 53 (${\mathrm{\bf(\sigma id)}}$).

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i}}$. Then:

If $Z{\in}\mathsf{Pred}$ then $Z[a{\mapsto}\text{\tt atm}(a)]=Z$.

If $k{\in}{\mathbb{Z}}$ and $z{\in}\mathsf{Set}^{k}$ then
$z[a{\mapsto}\text{\tt atm}(a)]=z$.

######  Proof 4.9.

We reason by induction on

$\mathit{age}(Z)\quad\text{and}\quad\mathit{age}(z).$

We consider the possibilities for $Z{\in}\mathsf{Pred}$:

  * •

If $Z={{\text{\tt and}}}(\mathcal{Z})$ for
$\mathcal{Z}\mathbin{\subseteq_{\text{\it fin}}}\mathsf{Pred}$ or
$Z={\text{\tt neg}}(Z^{\prime})$ for $Z^{\prime}{\in}\mathsf{Pred}$ then we
use rules ${\mathrm{\bf(\sigma{\text{\tt and}})}}$ and
${\mathrm{\bf(\sigma{\text{\tt neg}})}}$ of Figure 2 and the inductive
hypothesis.

  * •

If $Z={\text{\tt all}}([a^{\prime}]Z^{\prime})$ for
$Z^{\prime}{\in}\mathsf{Pred}$ and $a^{\prime}{\in}\mathbb{A}^{{i^{\prime}}}$
for some $i^{\prime}{\in}{\mathbb{Z}}$ then we use
${\mathrm{\bf(\sigma{\text{\tt all}})}}$ of Figure 2 and the inductive
hypothesis.

  * •

If $Z=({\text{\tt elt}}(z,b))$ for $j{\in}{\mathbb{Z}}$ and
$b{\in}\mathbb{A}^{{j}}$ and $z{\in}\mathsf{Set}^{j{\text{-}}1}$ then we use
rule ${\mathrm{\bf(\sigma{\text{\tt elt}}b)}}$ of Figure 2 and the inductive
hypothesis.

  * •

If $Z=({\text{\tt elt}}(z,a))$ for $z{\in}\mathsf{Set}^{i{\text{-}}1}$ then we
use ${\mathrm{\bf(\sigma{\text{\tt elt}}\text{\tt atm})}}$ of Figure 2 and the
inductive hypothesis for $z$.

We consider the possibilities for $z{\in}\mathsf{Set}^{k}$:

  * •

If $z$ is an atom then we reason using ${\mathrm{\bf(\sigma a)}}$ or
${\mathrm{\bf(\sigma b)}}$ of Figure 2.

  * •

If $z$ is an internal comprehension then we use Lemma 35(2&3) for a fresh
$c{\in}\mathbb{A}^{{k{\text{-}}1}}$ (so $c\text{\tt\\#}z$),
${\mathrm{\bf(\sigma{\text{\tt st}})}}$, and the inductive hypothesis.

Given what we have so far, Lemma 54 is not hard to prove.

######  Lemma 54 (${\mathrm{\bf(\sigma ren)}}$).

Suppose $i{\in}{\mathbb{Z}}$ and $a,a^{\prime}{\in}\mathbb{A}^{{i}}$. Then:

If $Z{\in}\mathsf{Pred}$ and $a^{\prime}\text{\tt\\#}Z$ then
$Z[a{\mapsto}\text{\tt atm}(a^{\prime})]=(a^{\prime}\ a){\cdot}Z$.

If $k{\in}{\mathbb{Z}}$ and $z{\in}\mathsf{Set}^{k}$ and
$a^{\prime}\text{\tt\\#}z$ then $z[a{\mapsto}\text{\tt
atm}(a^{\prime})]=(a^{\prime}\ a){\cdot}z$.

######  Proof 4.10.

Suppose $Z{\in}\mathsf{Pred}$ and $a^{\prime}\text{\tt\\#}Z$. We note by Lemma
44(1) (since $a^{\prime}\text{\tt\\#}Z$) that $Z[a{\mapsto}\text{\tt
atm}(a^{\prime})]=((a^{\prime}\ a){\cdot}Z)[a^{\prime}{\mapsto}\text{\tt
atm}(a^{\prime})]$ and use Lemma 53(1). The case of $z{\in}\mathsf{Set}^{k}$
is exactly similar.

###  4.3. Sigma-algebras and $\mathsf{SUB}$

We can now observe that our sigma-action is consistent with the nominal
algebra literature in the following sense:

######  Theorem 55.

The syntaxes of internal predicates and internal terms, with the sigma-action
from Definition 38, are _sigma-algebras_ in the sense of [Gab16, GG17], and
models of $\mathsf{SUB}$ in the sense of [GM08].

Concretely, this means that the sigma-action from Definition 38 and Figure 2
should

distribute through and, neg, and

distribute in a capture-avoiding manner through all, and st, and

should act on atm by direct substitution (see ${\mathrm{\bf(\sigma a)}}$ and
${\mathrm{\bf(\sigma b)}}$ in Figure 2), and

should satisfy the equalities in Figure 3.

######  Proof 4.11.

Immediate from the definitions and lemmas thus far, which were designed to
verify these properties.

######  Remark 56.

There is redundancy in Figure 3. For instance, a nominal algebra that
satisfies ${\mathrm{\bf(\sigma\alpha)}}$ satisfies ${\mathrm{\bf(\sigma id)}}$
if and only if it satisfies ${\mathrm{\bf(\sigma ren)}}$. One half of this
implication is implicit in the proof of Lemma 54, which derives
${\mathrm{\bf(\sigma ren)}}$ from (the lemmas corresponding to)
${\mathrm{\bf(\sigma\alpha)}}$ and ${\mathrm{\bf(\sigma id)}}$; going in the
other direction is no harder.

Likewise ${\mathrm{\bf(\sigma swp)}}$ can be derived from
${\mathrm{\bf(\sigma\sigma)}}$ and ${\mathrm{\bf(\sigma\text{\tt\\#})}}$. This
does no harm: in this paper we are interested in exploring the good properties
of Definition 38, rather than studying minimal sets of axioms for their own
sake (for which see [GM08]).

######  Remark 57.

We do not demand that the sigma-action should distribute through elt but this
is because this is syntactically impossible: ${\text{\tt
elt}}(y,a)[a{\mapsto}x]$ cannot be equal to ${\text{\tt
elt}}(y[a{\mapsto}x],x)$ because ${\text{\tt elt}}(y[a{\mapsto}x],x)$ is not
syntax according to Figure 1.

We shall see in Subsection 4.4, however, that this all works after all, in a
suitable sense, and this will become an important observation when
interpreting TST in internal syntax in Section 5.

######  Remark 58.

Another way to approach the proofs in this paper would be to admit ${\text{\tt
elt}}(y,x)$ and an explicit substitution term-former, and orient Figure 2 as
rewrite rules. We would obtain a _nominal rewrite system_ [FG07]. Essentially
this would amount to converting Figure 2 (and the proofs that use it) to a
‘small-step’ presentation, from the current ‘big-step’ form.

###  4.4. The sugar $y{\boldsymbol{\in}}x$ and its properties

Figure 1 only permits the syntax ${\text{\tt elt}}(y,a)$, not the syntax
${\text{\tt elt}}(y,x)$. We can obtain the power of ${\text{\tt elt}}(y,x)$
via a more sophisticated operation which we construct out of components
already available:

  * •

Suppose $i{\in}{\mathbb{Z}}$ and $x{\in}\mathsf{Set}^{i}$ is an internal
comprehension151515Terminology from Notation 3.1. So $x$ has the form
$\text{\tt st}([b]x\text{@}b)$ for some $b{\in}\mathbb{A}^{{i{\text{-}}1}}$
with $b\text{\tt\\#}x$, and $x$ does not have the form $\text{\tt atm}(a)$ for
any $a{\in}\mathbb{A}^{{i1}}$. and $y{\in}\mathsf{Set}^{i{\text{-}}1}$. Then
define $y{\boldsymbol{\in}}x$ by

$y{\boldsymbol{\in}}x=(x\text{@}b)[b{\mapsto}y]$

where we choose $b{\in}\mathbb{A}^{{i{\text{-}}1}}$ fresh (so
$b\text{\tt\\#}x,y$).

  * •

Suppose $i{\in}{\mathbb{Z}}$ and $a{\in}\mathbb{A}^{{i}}$ and
$y{\in}\mathsf{Set}^{i{\text{-}}1}$. Then define $y{\boldsymbol{\in}}\text{\tt
atm}(a)$ and $y{\boldsymbol{\in}}a$ by

$y{\boldsymbol{\in}}\text{\tt atm}(a)={\text{\tt
elt}}(y,a)=y{\boldsymbol{\in}}a.$

######  Remark 59.

Two natural sanity properties for Notation 4.4 are that

it should interact well with sets comprehension on the right-hand side, and

it should interact well with the sigma-action substituting variables for
terms. This is Lemmas 60 and 61.

######  Lemma 60.

Suppose $X{\in}\mathsf{Pred}$ and $i{\in}{\mathbb{Z}}$ and
$a{\in}\mathbb{A}^{{i}}$ and $x{\in}\mathsf{Set}^{i}$ and $a\text{\tt\\#}x$.
Then (using Notation 4.4)

$x{\boldsymbol{\in}}\text{\tt st}([a]X)=X[a{\mapsto}x].$

######  Proof 4.12.

Note by Lemma 21 that $a\text{\tt\\#}\text{\tt st}([a]X)$. By Notation 4.4
(since $a\text{\tt\\#}x,\text{\tt st}([a]X)$) $x{\boldsymbol{\in}}\text{\tt
st}([a]X)$ is equal to $((\text{\tt st}([a]X))\text{@}a)[a{\mapsto}x]$ and by
Lemma 35(4) this is equal to $X[a{\mapsto}x]$.

######  Lemma 61.

Suppose $i,j{\in}{\mathbb{Z}}$ and $x{\in}\mathsf{Set}^{i{+}1}$ and
$y{\in}\mathsf{Set}^{i}$ and $a{\in}\mathbb{A}^{{j}}$ and
$u{\in}\mathsf{Set}^{j}$. Then:

  1. (1)

$(y{\boldsymbol{\in}}x)[a{\mapsto}u]=y[a{\mapsto}u]{\boldsymbol{\in}}x[a{\mapsto}u]$.

  2. (2)

$(y{\boldsymbol{\in}}a)[a{\mapsto}u]=y[a{\mapsto}u]{\boldsymbol{\in}}u$, where
$j=i{\text{+}}1$.

  3. (3)

$(y{\boldsymbol{\in}}b)[a{\mapsto}u]=y[a{\mapsto}u]{\boldsymbol{\in}}b$, where
$b{\in}\mathbb{A}^{{i{\text{+}}1}}$.

######  Proof 4.13.

First, suppose we have proved part 1 of this result. Then part 2 follows using
Figure 2 ${\mathrm{\bf(\sigma a)}}$ and part 3 follows using Figure 2
${\mathrm{\bf(\sigma b)}}$.

To prove part 1 there are three cases:

  * •

_Suppose $x{=}\text{\tt atm}(a^{\prime})$ for some
$a^{\prime}{\in}\mathbb{A}^{{i{\text{+}}1}}$ not equal to $a$._

We reason as follows:

$\begin{array}[b]{r@{\ }l@{\qquad}l}(y{\boldsymbol{\in}}\text{\tt
atm}(a^{\prime}))[a{\mapsto}u]=&({\text{\tt
elt}}(y,a^{\prime}))[a{\mapsto}u]&\text{Notation~{}\ref{nttn.tin}}\\\
=&{\text{\tt
elt}}(y[a{\mapsto}u],a^{\prime})&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}b)}}\\\ =&y[a{\mapsto}u]{\boldsymbol{\in}}\text{\tt
atm}(a^{\prime})&\text{Notation~{}\ref{nttn.tin}}\\\
=&y[a{\mapsto}u]{\boldsymbol{\in}}(\text{\tt
atm}(a^{\prime})[a{\mapsto}u])&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma
b)}}\end{array}$

  * •

_Suppose $x{=}\text{\tt atm}(a)$ (so that $j{=}i{\text{+}}1$)._

There are two sub-cases:

    * –

_Suppose $u{=}\text{\tt atm}(n)$ for some $n{\in}\mathbb{A}^{{i}}$._ We reason
as follows:

$\begin{array}[]{r@{\ }l@{\qquad}l}(y{\boldsymbol{\in}}\text{\tt
atm}(a))[a{\mapsto}\text{\tt atm}(n)]=&({\text{\tt
elt}}(y,a))[a{\mapsto}\text{\tt atm}(n)]&\text{Notation~{}\ref{nttn.tin}}\\\
=&{\text{\tt elt}}(y[a{\mapsto}\text{\tt
atm}(n)],n)&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}\text{\tt atm})}}\\\ =&y[a{\mapsto}\text{\tt
atm}(n)]{\boldsymbol{\in}}\text{\tt
atm}(n)&\text{Notation~{}\ref{nttn.tin}}\end{array}$

    * –

_Suppose $u{=}\text{\tt st}([a^{\prime}]U^{\prime})$ where
$U^{\prime}=u\text{@}a^{\prime}$ for some fresh
$a^{\prime}{\in}\mathbb{A}^{{i{\text{-}}1}}$ (so
$a^{\prime}\text{\tt\\#}u,y$)._ We reason as follows:

$\begin{array}[]{r@{\ }l@{\qquad}l}(y{\boldsymbol{\in}}\text{\tt
atm}(a))[a{\mapsto}u]=&({\text{\tt
elt}}(y,a))[a{\mapsto}u]&\text{Notation~{}\ref{nttn.tin}}\\\
=&U^{\prime}[a^{\prime}{\mapsto}y[a{\mapsto}u]]&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
elt}}a)}}\\\
=&y[a{\mapsto}u]{\boldsymbol{\in}}u&\text{Notation~{}\ref{nttn.tin}}\end{array}$

  * •

_Suppose $x$ is an internal comprehension (not an internal atom)._

Choose $b{\in}\mathbb{A}^{{i}}$ fresh (so $b\text{\tt\\#}x,y,u$). We reason as
follows:

$\displaystyle\begin{array}[b]{r@{\
}l@{\qquad}l}(y{\boldsymbol{\in}}x)[a{\mapsto}u]=&(x\text{@}b)[b{\mapsto}y][a{\mapsto}u]&\text{Notation~{}\ref{nttn.tin}}\\\
=&(x\text{@}b)[a{\mapsto}u][b{\mapsto}y[a{\mapsto}u]]&\text{Proposition~{}\ref{prop.sigma.sigma}}\
b\text{\tt\\#}u\\\
=&(x[a{\mapsto}u]\text{@}b)[b{\mapsto}y[a{\mapsto}u]]&\text{Lemma~{}\ref{lemm.sigma.at.b}}\
b\text{\tt\\#}x,u\\\
=&y[a{\mapsto}u]{\boldsymbol{\in}}x[a{\mapsto}u]&\text{Notation~{}\ref{nttn.tin}}\end{array}$

######  Corollary 62.

Suppose $k{\in}{\mathbb{Z}}$ and $c{\in}\mathbb{A}^{{k}}$ and
$x{\in}\mathsf{Set}^{k}$ and $y{\in}\mathsf{Set}^{k{\text{-}}1}$ and
$c\text{\tt\\#}y$. Then

$\text{if}\ \ z{=}\text{\tt
st}([c](y{\boldsymbol{\in}}c)){\in}\mathsf{Set}^{k{+}1}\ \ \text{then}\ \
x{\boldsymbol{\in}}z=y{\boldsymbol{\in}}x.$

######  Proof 4.14.

We reason as follows:

$\displaystyle\begin{array}[b]{r@{\
}l@{\qquad}l}x{\boldsymbol{\in}}z=&x{\boldsymbol{\in}}\text{\tt
st}([c]y{\boldsymbol{\in}}c)&\text{Assumption}\\\
=&(y{\boldsymbol{\in}}c)[c{\mapsto}x]&\text{Lemma~{}\ref{lemm.Xax.tin}}\\\
=&y[c{\mapsto}x]{\boldsymbol{\in}}x&\text{Lemma~{}\ref{lemm.tin.sigma}(\ref{tin.distrib})}\\\
=&y{\boldsymbol{\in}}x&\text{Lemma~{}\ref{lemm.sigma.hash.always}}\,c\text{\tt\\#}y\end{array}$

######  Remark 63.

It is quite interesting to reflect on the inductive measures used in the
proofs above. Collecting them a list, they are:

$\mathit{age}(Z)$ and $\mathit{age}(z)$ in Lemmas 44, 46, and 53.

$(\mathit{level}(a),\mathit{age}(Z))$ and
$(\mathit{level}(a),\mathit{age}(z))$ in Proposition 42.

$(\mathit{level}(a){+}\mathit{level}(b),\mathit{age}(Z))$ and
$(\mathit{level}(a){+}\mathit{level}(b),\mathit{age}(z))$ in Proposition 49.
So we see that the inductive proofs fall into two categories:

those inductive proofs that are by a direct induction on structure and are
‘fairly simple’, and

those inductive proofs that depend on the hierarchy of levels and are
‘slightly harder’. Looking deeper at the slightly harder results, the
inductive quantities seem to follow a slogan of

> _take the sum of the levels of relevant atoms, and the age of the relevant
> terms, lexicographically ordered._

These inductive quantities are simple, though a certain amount of thinking was
required to develop them in the first place. For future work, if e.g. a
package for handling stratified syntax is implemented in a theorem-prover,
then the slogan above might form the basis of a generic automated proof-
method.

Though the proofs above are probably susceptible to automation by a
sufficiently advanced tactic, they are not all the same.

##  5\. The language of Typed Sets

We now have everything we need to develop the syntax of Typed Set Theory.

###  5.1. Syntax of Stratified Sets

######  Definition 64.

Let formulae and terms be inductively defined as in Figure 4. In that figure,
$a$ ranges over atoms (Definition 7) and  $\forall$ is taken to bind $a$ and
we quotient by $\alpha$-equivalence. We write $\phi[a{{:}\text{=}}s]$ and
$r[a{{:}\text{=}}s]$ for the usual capture-avoiding substitution on syntax.

######  Remark 65.

Quotienting by $\alpha$-equivalence means that a formula $\phi$ is actually an
$\alpha$-equivalence class of syntax-trees and similarly for a term $r$. This
is a typical treatment but we could just as easily set things up differently,
e.g. using nominal abstract syntax or de Bruijn indexes. Definition 64 as
written is designed to be close to what one might find in a typical paper on
TST+ or NF if the syntax were specified.161616…which it typically is not. For
instance [For95] does not formally define its syntax e.g. via an inductive
definition in the style of Definition 64, and this is not unusual.

$\begin{array}[]{r@{\
}l}\phi,\psi::=&{\boldsymbol{\bot}}\mid{\boldsymbol{\neg}}\phi\mid\phi{\boldsymbol{\wedge}}\phi\mid{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip 0.2pt}}a.\phi\mid
s{\boldsymbol{\in}}s\\\ s,t,r::=&a\mid\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\end{array}$ Figure
4. The syntax of Stratified Sets

Definition 66 is standard:

######  Definition 66.

Suppose $t$ is a term (Definition 64). Then extend $\mathit{level}(a)$ from
Definition 7 from atoms to all terms by:

$\begin{array}[]{r@{\ }l}\mathit{level}(\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt})=&\mathit{level}(a){+}1\end{array}$

Call a formula $\phi$ or term $t$ stratified when:

> if $s^{\prime}{\boldsymbol{\in}}s$ is a subterm of $\phi$ or $t$ then
> $\mathit{level}(s)=\mathit{level}(s^{\prime}){+}1$.

Suppose $a{\in}\mathbb{A}^{{2}}$, $b{\in}\mathbb{A}^{{3}}$, and
$c{\in}\mathbb{A}^{{4}}$. Then $a{\boldsymbol{\in}}b$ and
$b{\boldsymbol{\in}}c$ are stratified, and $a{\boldsymbol{\in}}c$,
$b{\boldsymbol{\in}}a$, and $a{\boldsymbol{\in}}a$ are not stratified.

######  Definition 67.

The language of Stratified Sets consists of stratified formulae and terms.

######  Remark 68.

We only care about _stratified_ formulae and terms henceforth — that is, we
restrict attention to those formulae and terms that are stratified.

So for all terms and formulae considered from now on, the reader should assume
they are stratified, where:

${\boldsymbol{\in}}$ polymorphically takes two terms of type $i$ and $i{+}1$
to a formula for each $i\in{\mathbb{Z}}$, and

sets comprehension $\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ takes an atom of
type $i\in{\mathbb{Z}}$ and a formula $\phi$ to a term of type $i{+}1$. We
further assume that levels are arranged to respect stratification where this
is required, so for example when we write $[a{{:}\text{=}}s]$ it is understood
that we assume $a{\in}\mathbb{A}^{{\mathit{level}(s)}}$.

######  Remark 69.

We could add equality $s{\boldsymbol{\text{=}}}t$ to our syntax in Figure 4,
at some modest cost in extra cases in inductive arguments. The pertinent
stratification condition would be that if $s{\boldsymbol{\text{=}}}t$ is a
subterm then $\mathit{level}(s)=\mathit{level}(t)$. Our results extend without
issues to the syntax with equality.

###  5.2. Interpretation for formulae and terms

######  Definition 70.

Define an interpretation of stratified formulae $\phi$ and terms $s$ as in
Figure 5, mapping $\phi$ to ${\langle\phi\rangle}\in\mathsf{Pred}$ and $s$ of
level $i{\in}{\mathbb{Z}}$ to ${\langle s\rangle}\in\mathsf{Set}^{i}$.

######  Remark 71.

For the reader’s convenience we give pointers for the notation used in the
right-hand sides of the equalities in Figure 5:

F is from Example 3.2.

neg is from Definition 31.

${\langle t\rangle}{\boldsymbol{\in}}{\langle s\rangle}$ is from Notation 4.4.

$\text{\tt st}([a]{\langle\phi\rangle})$ is from Definitions 20 and 31.

atm is from Definition 31. Note that the translation in Figure 5 from the
syntax of formulae $\phi$ and terms $s$ from Figure 4 to the syntax of
internal predicates and internal sets from Definition 31 is not entirely
direct: $t{\boldsymbol{\in}}s$ is primitive in formulae but only primitive in
internal predicates if $s$ is an atom.

$\begin{array}[t]{r@{\ }l}{\langle{\boldsymbol{\bot}}\rangle}=&{\text{\tt
F}}\\\ {\langle{\boldsymbol{\neg}}\phi\rangle}=&{\text{\tt
neg}}({\langle\phi\rangle})\\\
{\langle\phi{\boldsymbol{\wedge}}\psi\rangle}=&{{\text{\tt
and}}}(\\{{\langle\phi\rangle},{\langle\psi\rangle}\\})\\\
{\langle{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi\rangle}=&{\text{\tt
all}}([a]{\langle\phi\rangle})\end{array}\qquad\begin{array}[t]{r@{\
}l}{\langle t{\boldsymbol{\in}}s\rangle}=&{\langle
t\rangle}{\boldsymbol{\in}}{\langle s\rangle}\\\ {\langle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\rangle}=&\text{\tt
st}([a]{\langle\phi\rangle})\\\ {\langle a\rangle}=&\text{\tt
atm}(a)\end{array}$ Figure 5. Interpretation of formulae and terms

######  Definition 72.

Define the size of a stratified formula $\phi$ and stratified term $t$
inductively as follows:

$\begin{array}[]{r@{\ }l@{\quad}r@{\
}l}\mathit{size}(a)=&1&\mathit{size}(\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt})=&\mathit{size}(\phi){+}1\\\
\mathit{size}({\boldsymbol{\bot}})=&1&\mathit{size}(\phi{\boldsymbol{\wedge}}\psi)=&\mathit{size}(\phi)+\mathit{size}(\psi)+1\\\
\mathit{size}({\boldsymbol{\neg}}\phi)=&\mathit{size}(\phi){+}1&\mathit{size}({\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi)=&\mathit{size}(\phi){+}1\\\
\mathit{size}(t{\boldsymbol{\in}}s)=&\mathit{size}(t){+}\mathit{size}(s)+1\end{array}$

######  Lemma 73.

Suppose $\phi$ is a stratified formula and $s$ is a stratified term with
$\mathit{level}(s)=i\in{\mathbb{Z}}$. Then

${\langle\phi\rangle}\in\mathsf{Pred}\quad\text{and}\quad{\langle
s\rangle}\in\mathsf{Set}^{i}.$

######  Proof 5.1.

By induction on $\mathit{size}(\phi)$ and $\mathit{size}(s)$:171717A
structural induction on nominal abstract syntax [GP01] would also work, and in
a nominal mechanised proof might be preferable. Similarly for Proposition 74.

_The case of $a$._ By Figure 5 ${\langle a\rangle}{=}\text{\tt atm}(a)$. By
Definition 31 $\text{\tt atm}(a){\in}\mathsf{Set}^{i}$.

_The case of $\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}b\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ for $j{\geq}1$ and
$b{\in}\mathbb{A}^{{j}}$._ By Figure 5 ${\langle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}b\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\rangle}{=}\text{\tt
st}([b]{\langle\phi\rangle})$. By Definition 66
$\mathit{level}{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}b\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}}=j{+}1$. By
inductive hypothesis ${\langle\phi\rangle}{\in}\mathsf{Pred}$ and by
Definition 31 $\text{\tt st}([b]{\langle\phi\rangle})\in\mathsf{Set}^{j{+}1}$.

_The case of ${\boldsymbol{\bot}}$._ By Figure 5
${\langle{\boldsymbol{\bot}}\rangle}{=}{\text{\tt F}}\in\mathsf{Pred}$.

_The case of ${\boldsymbol{\neg}}\phi$._ From Figure 5 and Definition 31 using
the inductive hypothesis.

_The case of $\phi{\boldsymbol{\wedge}}\psi$._ From Figure 5 and Definition 31
using the inductive hypothesis.

_The case of ${\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip 0.2pt}}a.\phi$._ From
Figure 5 and Definition 31 using the inductive hypothesis.

_The case of $t{\boldsymbol{\in}}s$._ We refer to Notation 4.4 and use Lemma
35 and Proposition 42.

###  5.3. Properties of the interpretation

######  Proposition 74.

Suppose $\phi$ is a stratified formula and $t$, and $r$ are stratified terms
and $b{\in}\mathbb{A}^{{\mathit{level}(t)}}$. Then:

$\begin{array}[]{r@{\ }l}{\langle\phi\rangle}[b{\mapsto}{\langle
t\rangle}]=&{\langle\phi[b{{:}\text{=}}t]\rangle}\\\ {\langle
r\rangle}[b{\mapsto}{\langle t\rangle}]=&{\langle
r[b{{:}\text{=}}t]\rangle}\end{array}$

Note by Lemma 73 that ${\langle
t\rangle}{\in}\mathsf{Set}^{\mathit{level}(t)}$ so that the $\sigma$-action
$[b{\mapsto}{\langle t\rangle}]$ above is well-defined (Definition 38).

######  Proof 5.2.

By induction on $\mathit{size}(\phi)$ and $\mathit{size}(r)$. We consider each
case in turn; the interesting case is for ${\boldsymbol{\in}}$, where we use
Lemma 61:

_The case of ${\boldsymbol{\bot}}$._ We reason as follows:

$\begin{array}[]{r@{\
}l@{\qquad}l}{\langle{\boldsymbol{\bot}}\rangle}[b{\mapsto}{\langle
t\rangle}]=&{\text{\tt F}}[b{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.interp}}\\\ =&{\text{\tt
F}}&\text{Corollary~{}\ref{corr.credemp.sigma}}\\\
{\langle{\boldsymbol{\bot}}[b{{:}\text{=}}t]\rangle}=&{\langle{\boldsymbol{\bot}}\rangle}&\text{Fact
of syntax}\\\ =&{\text{\tt F}}&\text{Figure~{}\ref{fig.interp}}\end{array}$

_The case of ${\boldsymbol{\neg}}\phi$._ We reason as follows:

$\begin{array}[]{r@{\
}l@{\quad}l}{\langle{\boldsymbol{\neg}}\phi\rangle}[b{\mapsto}{\langle
t\rangle}]=&({\text{\tt neg}}({\langle\phi\rangle}))[b{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.interp}}\\\ =&{\text{\tt
neg}}({\langle\phi\rangle}[b{\mapsto}{\langle
t\rangle}])&\text{Figure~{}\ref{fig.sub}}\\\ =&{\text{\tt
neg}}({\langle\phi[b{{:}\text{=}}t]\rangle})&\text{IH}\
\mathit{size}(\phi){<}\mathit{size}({\boldsymbol{\neg}}\phi)\\\
=&{\langle{\boldsymbol{\neg}}(\phi[b{{:}\text{=}}t])\rangle}&\text{Figure~{}\ref{fig.sub}}\\\
=&{\langle({\boldsymbol{\neg}}\phi)[b{{:}\text{=}}t]\rangle}&\text{Fact of
syntax}\end{array}$

_The case of $\phi{\boldsymbol{\wedge}}\psi$._ We reason as follows:

$\begin{array}[]{r@{\
}l@{\quad}l}{\langle\phi{\boldsymbol{\wedge}}\psi\rangle}[b{\mapsto}{\langle
t\rangle}]=&({{\text{\tt
and}}}(\\{{\langle\phi\rangle},{\langle\psi\rangle}\\}))[b{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.interp}}\\\ =&{{\text{\tt
and}}}(\\{({\langle\phi\rangle}[b{\mapsto}{\langle
t\rangle}]),({\langle\psi\rangle}[b{\mapsto}{\langle
t\rangle}])\\})&\text{Figure~{}\ref{fig.sub}}\\\ =&{{\text{\tt
and}}}(\\{{\langle\phi[b{{:}\text{=}}t]\rangle},{\langle\psi[b{{:}\text{=}}t]\rangle}\\})&\text{IH}\
\mathit{size}(\phi),\mathit{size}(\psi){<}\mathit{size}(\phi{\boldsymbol{\wedge}}\psi)\\\
=&{\langle\phi[b{{:}\text{=}}t]{\boldsymbol{\wedge}}(\psi[b{{:}\text{=}}t])\rangle}&\text{Figure~{}\ref{fig.sub}}\\\
=&{\langle(\phi{\boldsymbol{\wedge}}\psi)[b{{:}\text{=}}t]\rangle}&\text{Fact
of syntax}\end{array}$

_The case of ${\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip 0.2pt}}a.\phi$._ We
reason as follows, where we $\alpha$-rename if necessary to assume
$a\text{\tt\\#}t$ (from which it follows by Theorem 27 that
$a\text{\tt\\#}{\langle t\rangle}$):

$\begin{array}[]{r@{\ }l@{\qquad}l}{\langle{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi\rangle}[b{\mapsto}{\langle t\rangle}]=&{\text{\tt
all}}([a]{\langle\phi\rangle})[b{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.interp}}\\\ =&{\text{\tt
all}}([a]({\langle\phi\rangle}[b{\mapsto}{\langle
t\rangle}]))&\text{Figure~{}\ref{fig.sub}}\ a\text{\tt\\#}{\langle
t\rangle}\\\ =&{\text{\tt
all}}([a]{\langle\phi[b{{:}\text{=}}t]\rangle})&\text{IH}\
\mathit{size}(\phi){<}\mathit{size}({\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip 0.2pt}}a.\phi)\\\
=&{\langle{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.(\phi[b{{:}\text{=}}t])\rangle}&\text{Figure~{}\ref{fig.interp}}\\\
=&{\langle({\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi)[b{{:}\text{=}}t]\rangle}&\text{Fact of syntax},\
a\text{\tt\\#}t\end{array}$

_The case of $b$._ By Figure 5 ${\langle b\rangle}{=}\text{\tt atm}(b)$. By
assumption ${\langle t\rangle}{\in}\mathsf{Set}^{\mathit{level}(b)}$ so by
Figure 2 ${\mathrm{\bf(\sigma a)}}$

$\text{\tt atm}(b)[b{\mapsto}{\langle t\rangle}]={\langle t\rangle}.$

_The case of $a$ (any atom other than $b$)._ By Figure 5 ${\langle
a\rangle}{=}\text{\tt atm}(a)$. We use rule ${\mathrm{\bf(\sigma b)}}$ of
Figure 2.

_The case of $\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$._
$\alpha$-converting if necessary assume $a$ is fresh (so $a\text{\tt\\#}t$,
and by Theorem 27 also $a\text{\tt\\#}{\langle t\rangle}$). We reason as
follows:

$\begin{array}[]{r@{\ }l@{\qquad}l}{\langle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}[b{\mapsto}{\langle t\rangle}]=&(\text{\tt
st}([a]{\langle\phi\rangle}))[b{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.interp}}\\\ =&\text{\tt
st}([a]{\langle\phi\rangle}[b{\mapsto}{\langle
t\rangle}])&\text{Figure~{}\ref{fig.sub}}{\mathrm{\bf(\sigma{\text{\tt
st}})}},\ a\text{\tt\\#}{\langle t\rangle}\\\ =&\text{\tt
st}([a]{\langle\phi[b{{:}\text{=}}t]\rangle})&\text{IH}\
\mathit{size}(\phi){<}\mathit{size}(\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt})\\\
=&{\langle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi[b{{:}\text{=}}t]\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}&\text{Figure~{}\ref{fig.interp}},\ a\text{\tt\\#}t\\\
=&{\langle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}[b{{:}\text{=}}t]\rangle}&\text{Fact of syntax}\end{array}$

_The case of $t^{\prime}{\boldsymbol{\in}}s^{\prime}$._ We reason as follows:

$\displaystyle\begin{array}[b]{r@{\ }l@{\quad}l}{\langle
t^{\prime}{\boldsymbol{\in}}s^{\prime}\rangle}[b{\mapsto}{\langle
t\rangle}]=&({\langle t^{\prime}\rangle}{\boldsymbol{\in}}{\langle
s^{\prime}\rangle})[b{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.interp}}\\\ =&({\langle
t^{\prime}\rangle}[b{\mapsto}{\langle t\rangle}]){\boldsymbol{\in}}({\langle
s^{\prime}\rangle}[b{\mapsto}{\langle
t\rangle}])&\text{Lemma~{}\ref{lemm.tin.sigma}}\\\ =&({\langle
t^{\prime}[b{{:}\text{=}}t]\rangle}){\boldsymbol{\in}}({\langle
s^{\prime}[b{{:}\text{=}}t]\rangle})&\text{IH}\
\mathit{size}(t^{\prime}),\mathit{size}(s^{\prime}){<}\mathit{size}(t^{\prime}{\boldsymbol{\in}}s^{\prime})\\\
=&{\langle(t^{\prime}[b{{:}\text{=}}t]){\boldsymbol{\in}}(s^{\prime}[b{{:}\text{=}}t])\rangle}&\text{Figure~{}\ref{fig.interp}}\end{array}$

######  Lemma 75.

Suppose $\phi$ is a stratified formula and $s$ is a stratified term. Suppose
$a\in\mathbb{A}^{{i{+}1}}$ and $\mathit{level}(s)=i$. Then:

  1. (1)

${\langle s{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}={\langle\phi[a{{:}\text{=}}s]\rangle}$.

  2. (2)

${\langle s{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}={\langle\phi\rangle}[a{\mapsto}{\langle s\rangle}]$.

######  Proof 5.3.

We reason as follows:

$\displaystyle\begin{array}[b]{r@{\ }l@{\qquad}l}{\langle
s{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\rangle}=&{\langle
s\rangle}{\boldsymbol{\in}}{\langle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}&\text{Figure~{}\ref{fig.interp}}\\\ =&{\langle
s\rangle}{\boldsymbol{\in}}\text{\tt
st}([a]{\langle\phi\rangle})&\text{Figure~{}\ref{fig.interp}}\\\ =&(\text{\tt
st}([a]{\langle\phi\rangle})\text{@}a)[a{\mapsto}{\langle
s\rangle}]&\text{Notation~{}\ref{nttn.tin}}\\\
=&{\langle\phi\rangle}[a{\mapsto}{\langle
s\rangle}]&\text{Lemma~{}\ref{lemm.conc.set}(4)}\\\
=&{\langle\phi[a{{:}\text{=}}s]\rangle}&\text{Proposition~{}\ref{prop.interp.sub}}\end{array}$

###  5.4. Confluence

######  Definition 76.

  1. (1)

Let $\to$ be a rewrite relation on the language of Stratified Sets (Definition
67) defined by the rules in Figure 6.

  2. (2)

Write $\to^{*}$ for the transitive reflexive closure of $\to$ (so the least
transitive reflexive relation containing $\to$).

$\begin{array}[]{c@{\qquad}c@{\qquad}c@{\qquad}c}{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
34.27179pt\hbox{$\displaystyle\penalty 1\phantom{h}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=74.30516pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\to\phi[a{{:}\text{=}}t]$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 5.27783pt\hbox{$\displaystyle\penalty
1\phi\to\phi^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=34.56778pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\boldsymbol{\neg}}\phi\to{\boldsymbol{\neg}}\phi^{\prime}$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.70502pt\hbox{$\displaystyle\penalty 1\phi\to\phi^{\prime}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=52.64444pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\phi{\boldsymbol{\wedge}}\phi^{\prime\prime}\to\phi^{\prime}{\boldsymbol{\wedge}}\phi^{\prime\prime}$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.70502pt\hbox{$\displaystyle\penalty 1\phi\to\phi^{\prime}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.42215pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\phi^{\prime\prime}{\boldsymbol{\wedge}}\phi\to\phi^{\prime\prime}{\boldsymbol{\wedge}}\phi^{\prime}$}}}}\\\\[17.22217pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
16.54706pt\hbox{$\displaystyle\penalty 1\phi\to\phi^{\prime}$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.10623pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\to\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi^{\prime}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.06367pt\hbox{$\displaystyle\penalty
1\phi\to\phi^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=52.13947pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi\to{\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi^{\prime}$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 10.2778pt\hbox{$\displaystyle\penalty 1s\to
s^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.02603pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle t{\boldsymbol{\in}}s\to
t{\boldsymbol{\in}}s^{\prime}$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 11.35419pt\hbox{$\displaystyle\penalty 1t\to
t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=42.02603pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle t{\boldsymbol{\in}}s\to
t^{\prime}{\boldsymbol{\in}}s$}}}}\end{array}$ Figure 6. Rewrite system on
formulae and terms

The natural injection of internal predicates and internal terms into
stratified formulae and terms is clear; to save notation we elide it, thus
effectively treating the syntax of internal predicates and terms from
Definition 31 as a direct subset of the syntax of stratified formulae and
terms from Figure 4. The reader who dislikes this abuse of notation can fill
in an explicit injection function $\iota$ as required, to map the former
injectively into the latter. Either way, the meaning will be the same.

Call a formula of the form $t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ a reduct.

######  Lemma 77.

${\langle\phi\rangle}$ considered as a formula, is a $\to$-normal form, and
similarly for ${\langle s\rangle}$.

######  Proof 5.4.

Reducts are impossible because the internal syntax from Figure 1 only allows
us to form $y{\boldsymbol{\in}}x$ (written ${\text{\tt elt}}(y,x)$ in that
figure) when $x$ is an atom and not a comprehension.

We can now state a kind of converse to Lemma 77:

######  Theorem 78.

$\phi\to^{*}{\langle\phi\rangle}$ and $s\to^{*}{\langle s\rangle}$.

Here we use Notation 5.4 to treat ${\langle\phi\rangle}$ and ${\langle
s\rangle}$ directly as stratified syntax.

If $\phi\to\phi^{\prime}$ then
${\langle\phi\rangle}={\langle\phi^{\prime}\rangle}$. If $s\to s^{\prime}$
then ${\langle s\rangle}={\langle s^{\prime}\rangle}$.

$\phi\to^{*}\phi^{\prime}$ then $\phi^{\prime}\to^{*}{\langle\phi\rangle}$,
and if $s\to^{*}s^{\prime}$ then $s^{\prime}\to^{*}{\langle
s^{\prime}\rangle}$. As a corollary, the rewrite relation $\to$ from Figure 6
is confluent.

######  Proof 5.5.

  1. (1)

By induction on syntax. The interesting case is for
$t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$. Suppose
$\phi\to^{*}{\langle\phi\rangle}$. Then

$\begin{array}[]{r@{\ }l@{\qquad}l}t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\to^{*}&{\langle
t\rangle}{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}&\text{IH,
Figure~{}\ref{fig.rewrite}}\\\ \to&{\langle\phi\rangle}[a{\mapsto}{\langle
t\rangle}]&\text{Figure~{}\ref{fig.rewrite}}\\\ =&{\langle
t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}&\text{Lemma~{}\ref{lemm.finte.to.sm}}\end{array}$

  2. (2)

By induction on the derivation of the rewrite (that is, on the term-context in
which the rewrite takes place). We consider three cases:

     * •

Suppose $t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\to\phi[a{{:}\text{=}}t]$. By Lemma 75 ${\langle
t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}={\langle\phi[a{{:}\text{=}}t]\rangle}$.

     * •

Suppose $t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\to
t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi^{\prime}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ because
$\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip
0.2pt}a\hskip 0.25pt\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip 0.2pt}\hskip
0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\to\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi^{\prime}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ because
$\phi\to\phi^{\prime}$. By induction hypothesis
${\langle\phi\rangle}={\langle\phi^{\prime}\rangle}$. Then using Lemma 75 we
have

${\langle t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}\stackrel{{\scriptstyle
L\ref{lemm.finte.to.sm}}}{{=}}{\langle\phi\rangle}[a{\mapsto}{\langle
t\rangle}]={\langle\phi^{\prime}\rangle}[a{\mapsto}{\langle
t\rangle}]\stackrel{{\scriptstyle L\ref{lemm.finte.to.sm}}}{{=}}{\langle
t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\rangle}.$

     * •

Suppose $t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\to
t^{\prime}{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ because $t\to
t^{\prime}$. By induction hypothesis ${\langle t\rangle}={\langle
t^{\prime}\rangle}$. We have

${\langle t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt}\rangle}\stackrel{{\scriptstyle
L\ref{lemm.finte.to.sm}}}{{=}}{\langle\phi\rangle}[a{\mapsto}{\langle
t\rangle}]={\langle\phi\rangle}[a{\mapsto}{\langle
t^{\prime}\rangle}]\stackrel{{\scriptstyle
L\ref{lemm.finte.to.sm}}}{{=}}{\langle
t^{\prime}{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}\rangle}.$

  3. (3)

We combine parts 1 and 2 of this result.

###  5.5. Strong normalisation

Call a comprehension $\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ ternary when $a$
occurs in $\phi$ _at least_ three times.181818This is arguably an abuse of
notation; ‘ternary’ might suggest _exactly_ three times. But we need a name.

If $a$ occurs in $\phi$ zero, one, or two times then we call
$\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip
0.2pt}a\hskip 0.25pt\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip 0.2pt}\hskip
0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ non-ternary.

Call a formula $\phi$ ternary if every comprehension in it is ternary.

Call a term $t$ ternary if every comprehension in it is ternary.

######  Definition 79.

Suppose $\phi$ is a formula and $t$ is a term. Write $\mathit{na}(\phi)$ and
$\mathit{na}(t)$ for the predicate or term obtained by padding every non-
ternary comprehension $\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a^{\prime}\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi^{\prime}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ in $\phi$ or $t$
to

$\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip
0.2pt}a^{\prime}\hskip 0.25pt\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip 0.2pt}\hskip
0.4pt\phi^{\prime}{\boldsymbol{\wedge}}{\boldsymbol{\exists}}c.(a^{\prime}{\boldsymbol{\in}}c{\boldsymbol{\wedge}}a^{\prime}{\boldsymbol{\in}}c{\boldsymbol{\wedge}}a^{\prime}{\boldsymbol{\in}}c)\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$

where $c\in\mathbb{A}^{{\mathit{level}(a^{\prime}){\text{+}}1}}$.191919The
precise choice of $c$ does not matter since we bind it with
${\boldsymbol{\exists}}$. The level matters, so the result is stratified.

######  Lemma 80.

Suppose $\phi$ is a formula and $t$ is a term. Then:

$\mathit{na}(\phi)$ and $\mathit{na}(t)$ are ternary.

If $\phi$ and $s$ are ternary then $\phi[a{{:}\text{=}}s]$ is ternary.
Similarly for $t[a{{:}\text{=}}s]$.

If $\phi$ is ternary and $\phi\to\phi^{\prime}$ then $\phi^{\prime}$ is
ternary. Similarly for $t\to t^{\prime}$.

######  Proof 5.6.

  1. (1)

By construction.

  2. (2)

By an easy calculation.

  3. (3)

By an easy calculation from Figure 6 and part 2 of this result.

######  Definition 81.

Define the complexity of a stratified formula $\phi$ and stratified term $t$
as follows:

$\begin{array}[]{r@{\ }l@{\quad}l}\mathit{cplx}(a)=&1\\\
\mathit{cplx}(\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt})=&1+\mathit{cplx}(\phi)\\\ \mathit{cplx}({\boldsymbol{\bot}})=&3\\\
\mathit{cplx}(\phi{\boldsymbol{\wedge}}\psi)=&\mathit{cplx}(\phi)+1+\mathit{cplx}(\psi)\\\
\mathit{cplx}({\boldsymbol{\neg}}\phi)=&1+\mathit{cplx}(\phi)\\\
\mathit{cplx}({\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi)=&1+\mathit{cplx}(\phi)\\\
\mathit{cplx}(b{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt})=&\mathit{cplx}(\phi)\\\
\mathit{cplx}(t{\boldsymbol{\in}}s)=&\mathit{cplx}(t)+1+\mathit{cplx}(s)&\begin{array}[t]{l}\text{$t$
not an atom, or}\\\ \text{$s$ not a comprehension}\end{array}\end{array}$

Define the number of atomic reducts of $\phi$ and $t$ as follows:

$\begin{array}[]{r@{\ }l@{\quad}l}\mathit{atomic}(a)=&0\\\
\mathit{atomic}(\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt})=&\mathit{atomic}(\phi)\\\ \mathit{atomic}({\boldsymbol{\bot}})=&0\\\
\mathit{atomic}(\phi{\boldsymbol{\wedge}}\psi)=&\mathit{atomic}(\phi)+\mathit{atomic}(\psi)\\\
\mathit{atomic}({\boldsymbol{\neg}}\phi)=&\mathit{atomic}(\phi)\\\
\mathit{atomic}({\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\forall$}}\hskip
0.2pt}}a.\phi)=&\mathit{atomic}(\phi)\\\
\mathit{atomic}(t{\boldsymbol{\in}}b)=&\mathit{atomic}(t)\\\
\mathit{atomic}(t{\boldsymbol{\in}}\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip
0.2pt})=&\mathit{atomic}(\phi)+1&t\text{ an atom}\\\
\mathit{atomic}(t{\boldsymbol{\in}}s)=&\mathit{atomic}(t)+\mathit{atomic}(s)&t\text{
not an atom}\end{array}$

######  Remark 82.

  1. (1)

If we view $\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\{$}}\hskip 0.2pt}a\hskip
0.25pt\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\mid$}}\hskip
0.2pt}\hskip 0.4pt\phi\boldsymbol{\hskip
0.8pt\raisebox{0.5pt}{\scalebox{0.85}{$\\}$}}\hskip 0.2pt}$ as $\lambda
a.\phi$ and $t{\boldsymbol{\in}}s$ as $s\,t$ then an _atomic reduct_ is just a
term of the form $(\lambda a.\phi)b$. Then $\mathit{atomic}$ counts the number
of atomic reducts in formulae $\phi$ and terms $t$, and $\mathit{cplx}$ is a
measure of size in which atomic reducts are skipped. Indeed, though we never
use this directly, from Definition 72 we see that

$\mathit{size}(\phi)=\mathit{cplx}(\phi)+2*\mathit{atomic}(\phi),$

and similarly for $t$.

  2. (2)

Intuitively, $\mathit{cplx}({\boldsymbol{\bot}})=3$ means
“${\boldsymbol{\bot}}$ has the same complexity as $b{\boldsymbol{\in}}a$”.
Technically, $\mathit{cplx}({\boldsymbol{\bot}})=3$ makes Lemma 83(2) hold,
and allows the arithmetic in Lemma 85 to go through.

######  Lemma 83.

Suppose $s$ is a term and $\phi$ is a predicate. Then:

$\mathit{cplx}(s)\geq 1$.

$\mathit{cplx}(\phi)\geq 3$.

If $s$ is not an atom (so it is a comprehension) then $\mathit{cplx}(s)\geq
4$.

######  Proof 5.7.

By calculations and induction using Definition 81; the base cases are
${\boldsymbol{\bot}}$ and $t{\boldsymbol{\in}}s$ (in particular,
$b{\boldsymbol{\in}}a$).

######  Lemma 84.

Suppose $\phi$ is a predicate and $t$ is a term. Suppose $a$ is an atom and
$s$ is a term and $\mathit{level}(a)=\mathit{level}(s)$ (so the substitution
$[a{{:}\text{=}}s]$ is well-defined). Then:

If $s$ is an atom then

$\mathit{cplx}(\phi[a{{:}\text{=}}s])=\mathit{cplx}(\phi)\quad\text{and}\quad\mathit{cplx}(t[a{{:}\text{=}}s])=\mathit{cplx}(t).$

If $s$ is not an atom (so is a comprehension) then

$\begin{array}[]{r@{\
}l}\mathit{cplx}(\phi[a{{:}\text{=}}s])\geq&\mathit{cplx}(\phi)+n*(\mathit{cplx}(s){\text{-}}1)\quad\text{and}\\\
\mathit{cplx}(t[a{{:}\text{=}}s])\geq&\mathit{cplx}(t)+n*(\mathit{cplx}(s){\text{-}}1)\end{array}$

where $n$ is the number of instances of $a$ in $\phi$ or $t$.

######  Proof 5.8.

  1. (1)

By a routine induction on $\phi$ and $t$ using Definition 81.

  2. (2)

Essentially this is clear because we replace $n$ instances of $a$ each with
complexity $1$, with $n$ instances of $s$ each with complexity
$\mathit{cplx}(s)$. The proof is by induction on syntax using Definition 81.
Interesting cases of the induction are $\phi$ or $t$ that do not mention $a$