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.Comment: arXiv admin note: text overlap with arXiv:1406.4060

@article{paperbot402,
  title = {The language of Stratified Sets is confluent and strongly normalising},
  author = {Murdoch J. Gabbay},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 2},
  year = {2018},
  doi = {10.23638/lmcs-14(2:12)2018}
}