The language of Stratified Sets is confluent and strongly normalising
Murdoch J. Gabbay
TL;DR
This paper proves that the language of Stratified Sets, used in various set theories, is confluent and strongly normalising, ensuring consistent and predictable rewriting behavior.
Contribution
It establishes that stratification conditions lead to confluence and strong normalisation in the syntax of Stratified Sets, connecting logic with rewriting properties.
Findings
Syntax forms a nominal algebra for substitution
Stratification implies confluence
Stratifiability implies strong normalisation
Abstract
We study the properties of the language of Stratified Sets (first-order logic with 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 -conversion.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\lmcsheading
1–LABEL:LastPageMay 23, 2017May 22, 2018
\makecompactlistenumeratei*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 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 -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 then if and only if . One way to avoid the term is to restrict to the language of Stratified Sets. This is first-order logic with a binary relation whose intuition is ‘ is an element of ’ and:
- •
Variable symbols (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 if the level of is one plus the level of . .
See Definition 66 for full details. Then cannot be stratified, since whatever level we assign to in we cannot make .
Stratified Sets are one of a family of syntaxes designed to exclude Russell’s paradox: {itemize*}
The language of ZF set theory restricts sets comprehension to bounded comprehension .
Type Theories (such as Higher-Order Logic) impose more or less elaborate type systems. The canonical example of this is simple types .
Stratified Sets stratifies terms as described.
One feature of Stratified Sets is that we can write a term representing the universal set:
[TABLE]
is easily stratified by giving any level we like. Likewise we can write definitions such as ‘the number 2’ to be ‘the set of all two-element sets’:
[TABLE]
(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 ‘’.
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)
The stratification condition implies that the syntax is confluent and strongly normalising under the natural rewrite
[TABLE]
We can write:
Stratification 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: {itemize*}
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 -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 -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)
TST (which stands for Typed Set Theory) is typically taken to be first-order logic with and variables stratified as , 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 . 3. (3)
Quine’s New Foundations (NF) uses the language of first-order logic with , and reasonable axioms, and a stratifiability condition that variables could be stratified.
So in TST we would have to write (say) (choosing a level 1 variable symbol and a level 2 variable symbol ), whereas in NF we could write just and say “we could assign level 1 and 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: {itemize}*
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 -calculus).**
One way to see that something like this paper should work, fingers crossed, is by an analogy: {itemize}*
The rewrite can be rewritten as .
*Extensionality is , and we can rewrite this as .
These are of course familiar as -reduction and -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 whose elements may ‘contain’ finitely many names ”. 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 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: {itemize*}
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**.**
{itemize*}
For each fix a disjoint countably infinite set of atoms.444These will serve as variable symbols in Definition 31.
Write .
If (so is an atom) write for the unique number such that .
We use a permutative convention that range over distinct atoms.
If we do not wish to use the permutative convention then we will refer to the atom using (see for instance of Figure 2).
2.1.2. Permutation actions on sets
Definition 8**.**
Suppose is a bijection on atoms.
- (1)
If is finite then we call finite. 2. (2)
If then call sort-respecting. 3. (3)
A permutation is a finite sort-respecting bijection on atoms.
Henceforth will range over permutations.
We will use the following notations in the rest of this paper: {nota} {enumerate*}
Write for the identity permutation such that for all .
Write for composition, so that .
If and then write for the swapping (terminology from [GP01]) mapping to , to , and all other to themselves, and take .
Write for the inverse of , so that .
2.1.3. Sets with a permutation action
{nota}
If write
[TABLE]
Definition 9**.**
A set with a permutation action is a pair of an underlying set and a permutation action written which is a group action on , so that and for all and permutations and .
Definition 10**.**
{enumerate*}
Say that supports when .
If a finite supporting exists, call finitely supported (by ) and say that has finite support.
{nota}
If is a set with a permutation action then we may write {itemize*}
as shorthand for , and
as shorthand for .
2.1.4. Nominal sets
[TABLE]
Definition 12**.**
Call a function equivariant when for all permutations and . In this case write .
The category of nominal sets and equivariant functions between them is usually called the category of nominal sets.
Definition 13**.**
Suppose is a nominal set and . Define the support of by
[TABLE]
{nota}{itemize*}
Write as shorthand for and read this as is fresh for .
If write as shorthand for .
Given atoms and elements write as shorthand for . That is: for every and .
Theorem 14**.**
Suppose is a nominal set and . Then is the unique least finite set of atoms that supports .
Proof 2.1**.**
See [Gab11, Theorem 2.21(1)].
Corollary 15**.**
{enumerate*}
If for all then . Equivalently: {enumerate}*
If then .
If then (see Notation 2.1.4).
If for every then .
* if and only if .*
Proof 2.2**.**
By routine calculations from the definitions and from Theorem 14 (see also [Gab11, Theorem 2.21(2)]).
2.2. Examples
Suppose and are nominal sets. We consider some examples, some of which will be useful later.
2.2.1. Atoms
is a nominal set with the natural permutation action .
2.2.2. Cartesian product
is a nominal set with underlying set and the pointwise action .
It is routine to check that .
2.2.3. Full function space
is a set with a permutation action with underlying set all functions from to , and the conjugation permutation action
[TABLE]
2.2.4. Finite-supported function space
is a nominal set with underlying set the functions from to with finite support under the conjugation action, and the conjugation permutation action.
2.2.5. Full powerset
Definition 16**.**
Suppose is a set with a permutation action. Give subsets the pointwise permutation action
[TABLE]
Then (the full powerset of ) is a set with a permutation action with {itemize*}
underlying set (the set of all subsets of ), and
the pointwise action .
A particularly useful instance of the pointwise action is for sets of atoms. As discussed in Subsection 2.2.1 above, if then . Thus if then
[TABLE]
Lemma 17**.**
Even if is a nominal set, need not be a nominal set.
Proof 2.3**.**
Take which we enumerate as and we take to be equal to defined by
[TABLE]
This does not have finite support (see also [Gab11, Remark 2.18]).
2.2.6. Finite powerset
For this subsection, fix a nominal set .
Definition 18**.**
Write for the nominal set with {itemize}*
underlying set the set of all finite subsets of ,
with the pointwise action from Definition 16.
{nota}
We might write for .
Lemma 19**.**
If then: {enumerate}*
* is finite.*
.
* implies .*
Rewriting this using Notation 2.1.4: if is finite and then implies .555This is not necessarily true if is infinite. For instance if we take then the reader can verify that for every , but does not hold for any . 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 that bounds for all . 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 -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 and an .
Definition 20**.**
Let the atoms-abstraction set have {itemize}*
Underlying set where .
Permutation action .
Lemma 21**.**
If and then . In particular (Notation 2.1.4).
Proof 2.5**.**
See [Gab11, Theorem 3.11].
Lemma 22**.**
Suppose and . Then if then .
Proof 2.6**.**
See [Gab11, Lemma 3.12].
Definition 23**.**
Suppose and . Write for the unique such that , if this exists.
Lemma 24**.**
Suppose and . Then implies is well-defined.
Proof 2.7**.**
See [Gab11, Theorem 3.19].
Lemma 25**.**
Suppose and and . Then: {enumerate}*
* and if then .*
If then .
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 -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 is a list . Suppose is a (not necessarily finite) permutation and write for . Suppose is a first-order logic predicate in the language of ZFA666First-order logic with equality , sets membership , and a constant or collection of constants for sets of atoms. with free variables . Suppose is a function specified using a first-order predicate in the language of ZFA with free variables .
Then we have the following principles: {enumerate}*
Equivariance of predicates.* .777It is important to realise here that must contain all the variables mentioned in the predicate. It is not the case that if and only if — but it is the case that if and only if (both are false).*
Equivariance of functions.* .*
Conservation of support.* If denotes elements with finite support
then .*
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 , then {itemize}*
taking we also know and
taking we also know , but
*we do not necessarily know that we can deduce (depending on this may still hold, of course, but not by equivariance since no permutation takes to ).
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 . 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 , given a deduction of , is 1. Without equivariance, the cost of deducing , given a deduction of , is roughly where is the cost of deducing . 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 for each . This is the difference between -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**.**
{enumerate*}
* (which means ).*
* (Notation 2.1.4) if and only if , and if and only if .*
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. {enumerate}*
Parts 33 and 33 of Lemma 33 say “We can alpha-convert”.
*In part 33 of Lemma 33, corresponds exactly to the notion that would normally be written “Free variables of”, and corresponds to “ is not free in ”.
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 -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).
{nota}
Write for the integers, so and for the natural numbers, which we start at [math], so .
Definition 31**.**
{enumerate*}
Define datatypes {itemize}*
* of internal predicates and*
* for of internal (level ) sets
inductively by the rules in Figure 1, where ranges over finite ordinals.*
Define
[TABLE]
Write for the least such that .
Write for the least such that .
{nota}
- •
If we may call an internal atom.
- •
If we may call an internal comprehension.
- •
We may call or an internal set.111111So every internal comprehension or internal atom is an internal set. Another choice of terminology would be to call an internal atom, an internal set, and or internal elements. However, note that is not a set and neither is ; they are both syntax and we can call them what we like.
Remark 32**.**
We read through and comment on Definition 31: {enumerate}*
* 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 and levels and simplify, we can rewrite Definition 31 semi-formally as follows:
[TABLE]
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 . See Example 3.2.*
all* represents universal quantification; read as ‘for all , ’ or in symbols: ‘’. In , is the nominal atoms-abstraction from Definition 20. It implements the binding of the universal quantifier by the standard nominal method.*
* represents a sets membership; read as ‘ is an element of ’. Note here that is an atom; it does not literally have any elements. represents the predicate ‘we believe that is an element of the variable ’, or in symbols: ‘’.*
* represents sets comprehension; read as ‘the set of such that ’ or in symbols: ‘’. Again, as standard in nominal techniques, nominal atoms-abstraction is used to represent the binding.*
If then .
* is a copy of wrapped in some formal syntax atm.*
Lemma 33**.**
Suppose and and and . Then: {enumerate}*
* and .*
* and , and .*
For every finite there exist and such that and .
Proof 3.1**.**
Immediate from Lemma 22, and Lemma 21 with Theorem 27.
Lemma 34**.**
Suppose and and and . Then and .
Proof 3.2**.**
3.2. Some notation
{nota}
Suppose and . Define syntactic sugar , and by
[TABLE]
{exa}
Define and by
[TABLE]
Intuitively, F represents the empty disjunction, and T represents the empty conjunction.
{nota}
Suppose that: {itemize*}
and
is an internal comprehension where and and
(equivalently121212By concrete calculations or by Theorem 27. ).
Then write
[TABLE]
Lemma 35 checks that Notation 3.2 makes sense:
Lemma 35**.**
Suppose and . Suppose is an internal comprehension and and . Then: {enumerate}*
* is well-defined and .*
.
If then (meaning that in an inductive argument using age, taking strictly decreases the inductive measure).
.
Proof 3.3**.**
- (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 from Example 3.2.
Definition 36**.**
Suppose and . Define and by
[TABLE]
We conclude with an easy lemma:
Lemma 37**.**
Suppose and . Then: {enumerate}*
* and , and similarly and .*
* and .*
Definition 36 does not depend on the choice of .
Proof 3.4**.**
{enumerate*}
From Definition 36 and Lemma 25(1).
From part 1 of this result, since and 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 of Figure 2, so it gets a fancy name (‘-action’) and we need to make formal and verify that it behaves as a substitution action should; see Remark 43.
Definition 38**.**
Define a -action* (sigma-action) to be a family of functions*
[TABLE]
where , inductively by the rules in Figure 2. For readability we write
[TABLE]
Furthermore in Figure 2: {itemize}*
In rule , .
In rule , .
In rule , and for some .
In rule , .
In rule , ranges over all atoms in (not just those distinct from ).
In rule , for some .
In rule , and for some .
Remark 39**.**
Figure 2 slips in no fewer than three abuses of the mathematics:
- (1)
We do not know that implies , so we should not write on the right-hand side of , or indeed on the right-hand side of , and so on.
In fact, all right-hand sides of Figure 2 are suspect except those of and . 2. (2)
We do not know whether the choice of fresh in matters, so we do not know that is well-defined. 3. (3)
The definition looks inductive at first glance, however in the case of there is no guarantee that (on the right-hand side) is smaller than (on the left-hand side). The level of is strictly lower than the level of , however levels are taken from which is totally ordered but not well-ordered by .
In fact:
- •
* does indeed imply .*
- •
The choice of fresh in is immaterial.
- •
The levels of atoms involved are bounded below (see Definition 41) so we only ever work on a well-founded fragment of .
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 and are totally ordered by 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 and the minimum level of or , inductively on and for as follows:
[TABLE]
Above, is the least element of . We add [math] 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 over a fixed but arbitrary choice. The proofs to follow will not care.
It will be convenient to apply to a mixed list of internal predicates, atoms, and internal sets: {nota}
- •
Define .
- •
If is a list of elements from then we write for the least element of .
Proposition 42**.**
Suppose and and .
- (1)
If then {itemize}* 2. (2)
* is well-defined,* 3. (3)
, and 4. (4)
. 5. (5)
If and then {itemize}* 6. (6)
* is well-defined,* 7. (7)
, and 8. (8)
.
Proof 4.1**.**
Fix some . We prove the Proposition for all and with and , by induction on
[TABLE]
lexicographically ordered. Since was arbitrary, this suffices to prove it for all and .
We consider the possibilities for : {itemize}*
The case of for .**
By Figure 2 We use the inductive hypothesis on each and some easy arithmetic calculations.
The case of for .**
By Figure 2 We use the inductive hypothesis on .
The case of for and for some .**
Using Lemma 33(33) we may assume without loss of generality that . By Figure 2 We use the inductive hypothesis on .
The case of for .* There are two sub-cases:*
- •
Suppose for some .* *
By Figure 2 We use the inductive hypothesis on .
- •
Suppose where for some fresh (so ).* *
By Figure 2 We have the inductive hypothesis on . We also have the inductive hypothesis (since )131313 was chosen no greater than the minimum level of , , and . Now , and it follows from Definition 41 that . on , and this suffices.
The case of where and and .**
*By Figure 2 and the inductive hypothesis.
We consider the possibilities for :*
- •
The case that is an internal atom.**
We use or of Figure 2.
- •
The case that is an internal comprehension.**
Choose fresh (so ), so that by Lemma 35(2) . We use the first part of this result and Figure 2 .
4.2. Nominal algebraic properties of the sigma-action
Remark 43**.**
Several useful properties of the -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: {itemize}*
* is Lemma 44.*
* is Lemma 46.*
* is Proposition 49.*
* and are Corollaries 51 and 52.*
* is Lemma 53.*
* is Lemma 54.*
* is Lemma 48.
These are familiar properties of substitution on syntax: for instance {itemize*}*
* looks like an -equivalence property — and indeed it is — and*
* (Lemma 46) is sometimes called garbage collection and corresponds to the property “if is not free in then ”, and*
* (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 -action on is not a simple ‘tree-grafting’ operation — not even a capture-avoiding one — because of in Figure 2. The proofs work, but we cannot take this for granted, and they require checking.
4.2.1. Alpha-equivalence of the sigma-action
Lemma 44** ().**
Suppose and and . Suppose and and and . Then: {enumerate}*
* and .*
* and .*
If then and .
Proof 4.2**.**
By induction on
[TABLE]
We consider the possibilities for :
- •
The case of for .* By Lemma 19 for every , so by the inductive hypothesis . We use Figure 2 and Theorem 27.*
- •
The case of for .* By Figure 2 and the inductive hypothesis for .*
- •
The case of for and for some .* Using Lemma 33(33) we may assume without loss of generality that . We use Figure 2 and the inductive hypothesis.*
- •
The case of for some .* There are two sub-cases:*
- –
Suppose for some .* We reason as follows:*
[TABLE]
- –
Suppose where for some fresh (so ).* *
We reason as follows:
[TABLE]
- •
The case for and and .* We reason as follows:*
[TABLE]
We consider the possibilities for :
- •
The case that is an internal atom.* We use or of Figure 2.*
- •
The case that is an internal comprehension.* We use Lemma 35(2&3) for a fresh (so ), , and the inductive hypothesis.*
For part 2, we note that by Theorem 27 and Proposition 29
[TABLE]
We take a sets intersection. The case of is similar.
Part 3 follows, recalling from Notation 2.1.4 that means .
Remark 45**.**
Note for experts:* We could set Definition 38 up differently: we could have and input abstractions*
[TABLE]
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 (garbage collection)
Lemma 46** ().**
Suppose and and and and for . Then
[TABLE]
Proof 4.3**.**
By induction on
[TABLE]
We consider the possibilities for : {itemize}*
The case of for .**
By Figure 2 . By Lemma 19(19) for every . We use the inductive hypothesis on each .
The case of for .**
By Figure 2 . We use the inductive hypothesis on .
The case of for and for some .**
Using Lemma 33(33) we may assume without loss of generality that . By Figure 2 . We use the inductive hypothesis on .
The case of for and .**
This is impossible because we assumed .
The case of for and and .**
*By Figure 2 . We use the inductive hypothesis on .
We consider the possibilities for :*
- •
If is an internal atom then we reason using or of Figure 2.
- •
If is an internal comprehension then we use Lemma 35(2&3) for a fresh (so ), , and the inductive hypothesis.
Recall and from Example 3.2. Corollary 47 is an easy consequence of Lemma 46 and will be useful later:
Corollary 47**.**
Suppose and and . Then
[TABLE]
Proof 4.4**.**
By Theorem 27 so that . We use Lemma 46. Similarly for T.
4.2.3. commutes with atoms-concretion
Lemma 48 will be useful later, starting with Proposition 49:
Lemma 48** ().**
Suppose and and . Suppose and is an internal comprehension and and . Then
[TABLE]
( is from Notation 3.2.)
Proof 4.5**.**
By Lemma 35(2) we may write where . We reason as follows:
[TABLE]
4.2.4. commutes with itself: the ‘substitution lemma’
Proposition 49**.**
Suppose and and . Suppose and and and suppose and and and . Then
[TABLE]
Proof 4.6**.**
For brevity we may write
[TABLE]
Fix some . We prove the Lemma for all and with and (Definition 41), reasoning by induction on
[TABLE]
lexicographically ordered. Since was arbitrary, this suffices to prove it for all and .
We consider the possibilities for :
- •
The case of for .* We use rule of Figure 2 and the inductive hypothesis.*
- •
The case of for .* We use of Figure 2 and the inductive hypothesis.*
- •
The case of for and for some .* We use Lemma 33(33) to assume without loss of generality that , and then we use of Figure 2 and the inductive hypothesis.*
- •
The case of for where .* There are two sub-cases:*
- –
Suppose for some other than * (we assumed so is impossible).*
We reason as follows:
[TABLE]
- –
Suppose where for some fresh (so and ).**
Note by Theorem 27 that and . We reason as follows:
[TABLE]
- •
The case of for where .* There are two sub-cases:*
- –
Suppose for some .**
If then we reason as follows:
[TABLE]
If so that , and for some other than , then we reason as follows:
[TABLE]
If so that , and where for some fresh (so and ) then we reason as follows (note by Theorem 27 that and ):
[TABLE]
- –
Suppose where for some fresh (so and ).**
We reason as follows:
[TABLE]
- •
The case of for and and .* We reason as follows:*
[TABLE]
We consider the possibilities for :
- •
If is an internal atom then we reason using and of Figure 2.
- •
If is an internal comprehension then we use Lemma 35(2&3) for a fresh (so ), , and the inductive hypothesis.
Remark 50**.**
Were Proposition 49 about the syntax of first-order logic or the -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 -calculus, the proof is not routine. Issues with binders (Figure 2 , and one explicit in ) 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 -action, mostly because of (to a lesser extent also because of the nominal binder ).
Corollary 51** ().**
Suppose and and . Suppose and and and suppose and and . Suppose and . Then
[TABLE]
Proof 4.7**.**
From Proposition 49 and Lemma 46.
Corollary 52** ().**
Suppose and and . Suppose and and and suppose and and . Suppose and .141414We expect a stronger version of Corollary 52 to be possible in which we do not assume . However, the proof would require an induction resembling the proof of Proposition 49 — the proof assuming can piggyback on the induction already given in Proposition 49. We will not need this stronger version, so we do not bother. Then
[TABLE]
Proof 4.8**.**
From Proposition 49 and Lemma 46.
4.2.5. : substitution for atoms and its corollaries
We called in Definition 31 an internal atom. Atoms in nominal techniques interpet variables, so if we call an internal atom this should suggest that should behave like a variable (or a variable symbol). Rules and from Figure 2 are consistent with that, and Lemma 53 makes formal more of this intuition:
Lemma 53** ().**
Suppose and . Then: {enumerate}*
If then .
If and then .
Proof 4.9**.**
We reason by induction on
[TABLE]
We consider the possibilities for :
- •
If for or for then we use rules and of Figure 2 and the inductive hypothesis.
- •
If for and for some then we use of Figure 2 and the inductive hypothesis.
- •
If for and and then we use rule of Figure 2 and the inductive hypothesis.
- •
If for then we use of Figure 2 and the inductive hypothesis for .
We consider the possibilities for :
- •
If is an atom then we reason using or of Figure 2.
- •
If is an internal comprehension then we use Lemma 35(2&3) for a fresh (so ), , and the inductive hypothesis.
Given what we have so far, Lemma 54 is not hard to prove.
Lemma 54** ().**
Suppose and . Then: {itemize}*
If and then .
If and and then .
Proof 4.10**.**
Suppose and . We note by Lemma 44(1) (since ) that and use Lemma 53(1). The case of is exactly similar.
4.3. Sigma-algebras and
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 in the sense of [GM08].
Concretely, this means that the sigma-action from Definition 38 and Figure 2 should {itemize}*
distribute through and, neg, and
distribute in a capture-avoiding manner through all, and st, and
should act on atm by direct substitution (see and 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 satisfies if and only if it satisfies . One half of this implication is implicit in the proof of Lemma 54, which derives from (the lemmas corresponding to) and ; going in the other direction is no harder.
Likewise can be derived from and . 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: cannot be equal to because 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 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 and its properties
Figure 1 only permits the syntax , not the syntax . We can obtain the power of via a more sophisticated operation which we construct out of components already available: {nota}
- •
Suppose and is an internal comprehension151515Terminology from Notation 3.1. So has the form for some with , and does not have the form for any . and . Then define by
[TABLE]
where we choose fresh (so ).
- •
Suppose and and . Then define and by
[TABLE]
Remark 59**.**
Two natural sanity properties for Notation 4.4 are that {enumerate}*
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.
Lemma 60**.**
Suppose and and and and . Then (using Notation 4.4)
[TABLE]
Proof 4.12**.**
Note by Lemma 21 that . By Notation 4.4 (since ) is equal to and by Lemma 35(4) this is equal to .
Lemma 61**.**
Suppose and and and and . Then:
- (1)
. 2. (2)
, where . 3. (3)
, where .
Proof 4.13**.**
First, suppose we have proved part 1 of this result. Then part 2 follows using Figure 2 and part 3 follows using Figure 2 .
To prove part 1 there are three cases:
- •
Suppose for some not equal to .**
We reason as follows:
[TABLE]
- •
Suppose (so that ).**
There are two sub-cases:
- –
Suppose for some .* We reason as follows:*
[TABLE]
- –
Suppose where for some fresh (so ).* We reason as follows:*
[TABLE]
- •
Suppose is an internal comprehension (not an internal atom).**
Choose fresh (so ). We reason as follows:
[TABLE]
Corollary 62**.**
Suppose and and and and . Then
[TABLE]
Proof 4.14**.**
We reason as follows:
[TABLE]
Remark 63**.**
It is quite interesting to reflect on the inductive measures used in the proofs above. Collecting them a list, they are: {itemize}*
* and in Lemmas 44, 46, and 53.*
* and in Proposition 42.*
* and in Proposition 49.
So we see that the inductive proofs fall into two categories: {enumerate*}*
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, ranges over atoms (Definition 7) and
is taken to bind and we quotient by -equivalence. We write and for the usual capture-avoiding substitution on syntax.*
Remark 65**.**
Quotienting by -equivalence means that a formula is actually an -equivalence class of syntax-trees and similarly for a term . 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.
Definition 66 is standard:
Definition 66**.**
Suppose is a term (Definition 64). Then extend from Definition 7 from atoms to all terms by:
[TABLE]
Call a formula or term stratified when:
if is a subterm of or then .
{exa}
Suppose , , and . Then and are stratified, and , , and 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: {itemize}*
* polymorphically takes two terms of type and to a formula for each , 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 and a formula to a term of type .
We further assume that levels are arranged to respect stratification where this is required, so for example when we write it is understood that we assume .*
Remark 69**.**
We could add equality to our syntax in Figure 4, at some modest cost in extra cases in inductive arguments. The pertinent stratification condition would be that if is a subterm then . 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 and terms as in Figure 5, mapping to and of level to .
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: {itemize}*
F* is from Example 3.2.*
neg* is from Definition 31.*
* is from Notation 4.4.*
* is from Definitions 20 and 31.*
atm* is from Definition 31.
Note that the translation in Figure 5 from the syntax of formulae and terms from Figure 4 to the syntax of internal predicates and internal sets from Definition 31 is not entirely direct: is primitive in formulae but only primitive in internal predicates if is an atom.*
Definition 72**.**
Define the size of a stratified formula and stratified term inductively as follows:
[TABLE]
Lemma 73**.**
Suppose is a stratified formula and is a stratified term with . Then
[TABLE]
Proof 5.1**.**
By induction on and :171717A structural induction on nominal abstract syntax [GP01] would also work, and in a nominal mechanised proof might be preferable. Similarly for Proposition 74. {itemize}*
The case of .* By Figure 5 . By Definition 31 .*
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 and .* 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 and by Definition 31 .*
The case of .* By Figure 5 .*
The case of .* From Figure 5 and Definition 31 using the inductive hypothesis.*
The case of .* 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 .* We refer to Notation 4.4 and use Lemma 35 and Proposition 42.*
5.3. Properties of the interpretation
Proposition 74**.**
Suppose is a stratified formula and , and are stratified terms and . Then:
[TABLE]
Note by Lemma 73 that so that the -action above is well-defined (Definition 38).
Proof 5.2**.**
By induction on and . We consider each case in turn; the interesting case is for , where we use Lemma 61: {itemize}*
The case of .* We reason as follows:*
[TABLE]
The case of .* We reason as follows:*
[TABLE]
The case of .* We reason as follows:*
[TABLE]
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 -rename if necessary to assume (from which it follows by Theorem 27 that ):*
[TABLE]
The case of .* By Figure 5 . By assumption so by Figure 2 *
[TABLE]
The case of (any atom other than ).* By Figure 5 . We use rule 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}.* -converting if necessary assume is fresh (so , and by Theorem 27 also ). We reason as follows:*
[TABLE]
The case of .* We reason as follows:*
[TABLE]
Lemma 75**.**
Suppose is a stratified formula and is a stratified term. Suppose and . Then:
- (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:
[TABLE]
5.4. Confluence
Definition 76**.**
- (1)
Let be a rewrite relation on the language of Stratified Sets (Definition 67) defined by the rules in Figure 6. 2. (2)
Write for the transitive reflexive closure of (so the least transitive reflexive relation containing ).
{nota}
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 as required, to map the former injectively into the latter. Either way, the meaning will be the same.
{nota}
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**.**
* considered as a formula, is a -normal form, and similarly for .*
Proof 5.4**.**
Reducts are impossible because the internal syntax from Figure 1 only allows us to form (written in that figure) when is an atom and not a comprehension.
We can now state a kind of converse to Lemma 77:
Theorem 78**.**
{enumerate*}
* and .*
Here we use Notation 5.4 to treat and directly as stratified syntax.
If then . If then .
* then , and if then . As a corollary, the rewrite relation from Figure 6 is confluent.*
Proof 5.5**.**
- (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 . Then
[TABLE] 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 . By induction hypothesis . Then using Lemma 75 we have
[TABLE]
- •
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 . By induction hypothesis . We have
[TABLE] 3. (3)
We combine parts 1 and 2 of this result.
5.5. Strong normalisation
{nota}{itemize*}
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 occurs in at least three times.181818This is arguably an abuse of notation; ‘ternary’ might suggest exactly three times. But we need a name.
If occurs in 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 ternary if every comprehension in it is ternary.
Call a term ternary if every comprehension in it is ternary.
Definition 79**.**
Suppose is a formula and is a term. Write and 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 or to
[TABLE]
where .191919The precise choice of does not matter since we bind it with . The level matters, so the result is stratified.
Lemma 80**.**
Suppose is a formula and is a term. Then: {enumerate}*
* and are ternary.*
If and are ternary then is ternary. Similarly for .
If is ternary and then is ternary. Similarly for .
Proof 5.6**.**
- (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 and stratified term as follows:
[TABLE]
Define the number of atomic reducts of and as follows:
[TABLE]
Remark 82**.**
- (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 and as then an atomic reduct is just a term of the form . Then counts the number of atomic reducts in formulae and terms , and is a measure of size in which atomic reducts are skipped. Indeed, though we never use this directly, from Definition 72 we see that
[TABLE]
and similarly for . 2. (2)
Intuitively, means “* has the same complexity as ”. Technically, makes Lemma 83(2) hold, and allows the arithmetic in Lemma 85 to go through.*
Lemma 83**.**
Suppose is a term and is a predicate. Then: {enumerate}*
.
.
If is not an atom (so it is a comprehension) then .
Proof 5.7**.**
By calculations and induction using Definition 81; the base cases are and (in particular, ).
Lemma 84**.**
Suppose is a predicate and is a term. Suppose is an atom and is a term and (so the substitution is well-defined). Then: {enumerate}*
If is an atom then
[TABLE]
If is not an atom (so is a comprehension) then
[TABLE]
where is the number of instances of in or .
Proof 5.8**.**
- (1)
By a routine induction on and using Definition 81. 2. (2)
Essentially this is clear because we replace instances of each with complexity , with instances of each with complexity . The proof is by induction on syntax using Definition 81. Interesting cases of the induction are or that do not mention (so ), , , and a{\boldsymbol{\in}}\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}. We consider each in turn: {itemize}* 3. (3)
If or do not mention then and and the result follows. 4. (4)
It is a fact that , and we calculate as follows:
[TABLE] 5. (5)
It is a fact that , and we calculate as follows:
[TABLE] 6. (6)
It is a fact that \mathit{cplx}(a{\boldsymbol{\in}}\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})=\mathit{cplx}(\phi^{\prime}), and we calculate as follows:
[TABLE]
Lemma 85**.**
Suppose \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} is ternary (so mentions free at least three times) and is a term and . Then: {enumerate}*
If is an atom then
[TABLE]
If is not an atom then
[TABLE]
Proof 5.9**.**
- (1)
From Lemma 84(1). 2. (2)
Using Definition 81 and Lemma 84(2) we have the following facts: {itemize}* 3. (3)
\mathit{cplx}(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})=\mathit{cplx}(\phi)+3+(\mathit{cplx}(s){\text{-}}1). 4. (4)
*.
We can drop the on both sides and do some arithmetic:*
[TABLE]
We assumed is ternary, which means precisely that , so this is true.
Corollary 86**.**
If is ternary and then precisely one of the following must hold: {itemize}*
* (in words: complexity increases).*
* and (in words: atomic reducts decrease).
Similarly for .*
Proof 5.10**.**
Consider a reduct 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^{\prime}\boldsymbol{\hskip 0.8pt\raisebox{0.5pt}{\scalebox{0.85}{}}}\hskip 0.2pt}. {itemize}*
If is not an atom then we use Lemma 85(2).
If is an atom then using Lemma 85(1) complexity is unchanged; however the number of atomic reducts decrements.
Proposition 87**.**
The rewrite system from Figure 6 is terminating (no infinite chain of rewrites).
Proof 5.11**.**
We consider just the case of reducing formulae; reducing terms is no harder.
* is just an annotated copy of , so if has an infinite chain of rewrites then so must .202020In a machine implementation we would probably want to refine Definition 79 to annotate with for a fresh constant-symbol or variable symbol (one for each level), instead of . This would make it easier to automatically track the annotations. We see that it would suffice to prove that reductions from are terminating.*
So suppose , and is ternary (apply if required).
Consider and suppose . From Theorem 78 , and by Corollary 86(1)
[TABLE]
Thus the set is bounded above by . It follows using Corollary 86(1&2) and considering the measure
[TABLE]
lexicographically ordered, that any chain of reductions from must terminate.
Remark 88**.**
The proof of Proposition 87 is not difficult.212121…but not trivial. Thanks to an anonymous referee for spotting my errors. This is in itself interesting:
We noticed in Remark 6 how stratified syntax can be viewed as a fragment of the simply-typed -calculus, where corresponds to a -reduct and extensionality corresponds to an -expansion. Yet, the direct proof of strong normalisation for the simply-typed -calculus is quite different and seems harder than the proof of Proposition 87 (a concise but clear presentation is in Chapter 6 of [GTL89]).
Theorem 89**.**
Formulae and terms of Stratified Sets, with the rewrites from Figure 6, are confluent and strongly normalising.
Proof 5.12**.**
Confluence and weak normalisation (every formula/term has some rewrite to a normal form) are from Theorem 78.
Strong normalisation* follows from weak normalisation and termination (Proposition 87).*
Remark 90**.**
So from Theorems 89 and 55 we see that: {enumerate}*
the syntax of formulae and terms has normal forms, and furthermore
normal forms with the natural substitution action given by substitute-then-renormalise, corresponds precisely to the theory of internal predicates and terms from Definition 31 and 38, and furthermore
this theory of normal forms is an instance of the notion of nominal algebras for substitution, also called sigma-algebras, as used in the previous literature studying -calculus, first-order logic, and pure substitution [GG17, Gab16, GM08].
Recall from Remarks 1 and 2 that in stratifiable syntax, as used in Quine’s NF, variables do not have predefined levels but we insist on a stratifiability condition that and are only legal if we could assign levels to their variables to stratify them. We obtain as an easy corollary:
Theorem 91**.**
Formulae and terms of stratifiable syntax, with the rewrites from Figure 6, are confluent and strongly normalising.
Proof 5.13**.**
The result follows from Theorem 89 by taking a stratifiable , and stratifying it so that we now have in the language of Typed Sets. Rewrites on clearly correspond 1-1 with rewrites on , since Figure 6 makes no reference to the levels of variables.
6. Conclusions and future work
Stratified Sets occupy a nice middle ground between ZF sets and simple types. They typically appear used as a foundational syntax. However, we have seen in this paper that Typed-Sets-the-syntax in and of itself forms a well-behaved rewrite system, and a well-behaved nominal algebra. This had not previously been noted, and this paper gives a reasonably full and detailed account of how rewriting and nominal algebra apply. This account is intended to be suitable for {itemize*}
readers familiar with rewriting who are unfamiliar with stratified sets syntax222222Stratified sets syntax is not hard to define — but it requires experience to learn what kinds of predicates are and are not stratifiable. In use, stratifiability is a subtle and powerful condition.
readers familiar with stratified sets syntax but unfamiliar with techniques from rewriting and nominal algebra.
We have also tried to smooth a path to implementing these proofs in a machine, hopefully in a nominal context. We have designed the proofs to be friendly to such an implementation as future work, yet without compromising readability for humans. Where we have cut corners (relative to a machine implementation), we tried to signpost this fact (see for instance Remark 39 and Notation 5.4).
Concerning other applications, it is often possible to use normal forms to build denotations. In some contexts, the normal form is the denotation of the terms that reduce to it. That will not work for Stratified Sets because we are usually interested in imposing additional axioms. But there are standard things that can be done about that, and this has been investigated in a nominal context in papers like [Gab16, GG17]. These papers build denotations for first-order logic and the -calculus using maximally consistent sets, and using nominal techniques to manage binding in denotations (extending how we used nominal techniques in this paper to manage binding in syntax). Having normal forms is useful here and the ideas in this paper can be used to give a denotational analysis of theories in the languages of Stratified and Stratifiable Sets. This is future work.
We can ask about a converse to Theorems 89 and 91. We have shown that a stratifiable formula rewrites to a normal form. Now if a formula (without levels) rewrites to normal form, is it stratifiable? We see that we cannot hope for a perfect converse by the following easy example: if we write then is not stratifiable but it rewrites to , which is stratifiable for instance as , which we could also write just as . However there may be special cases in which stratification information can be recovered from normalisation, and this is future work.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[Bar 84] Henk P. Barendregt. The Lambda Calculus: its Syntax and Semantics (revised ed.) . North-Holland, 1984.
- 2[Bar 14] Barendregt’s substitution lemma, June 2014. http://isabelle.in.tum.de/nominal/example.html, retrieved 2014/June/8.
- 3[DG 12a] Gilles Dowek and Murdoch J. Gabbay. Permissive Nominal Logic (journal version). Transactions on Computational Logic , 13(3), 2012.
- 4[DG 12b] Gilles Dowek and Murdoch J. Gabbay. PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. Theoretical Computer Science , 451:38–69, 2012.
- 5[FG 07] Maribel Fernández and Murdoch J. Gabbay. Nominal rewriting (journal version). Information and Computation , 205(6):917–965, June 2007.
- 6[For 95] Thomas E. Forster. Set theory with a universal set: exploring an untyped universe . Clarendon Press, 1995.
- 7[For 97] Thomas E. Forster. Quine’s NF, 60 years on. American Mathematical Monthly , 104(9):838–845, 1997.
- 8[Gab 01] Murdoch J. Gabbay. A Theory of Inductive Definitions with alpha-Equivalence . Ph D thesis, University of Cambridge, UK, March 2001.